Resolution With Merging. - Peter B. Andrews (J. ACM, 1968)

A Correction Concerning Resolution. - Peter B. Andrews (J. ACM, 1968)

On Simplifying the Matrix of a WFF. - Peter B. Andrews (J. Symb. Log., 1968)

Resolution in Type Theory. - Peter B. Andrews (J. Symb. Log., 1971)

General Models, Descriptions, and Choice in Type Theory. - Peter B. Andrews (J. Symb. Log., 1972)

General Models and Extensionality. - Peter B. Andrews (J. Symb. Log., 1972)

Resolution and the consistency of analysis. - Peter B. Andrews (Notre Dame J. Formal Log., 1974)

Refutations by Matings. - Peter B. Andrews (IEEE Trans. Computers, 1976)

Theorem Proving in Type Theory. - Peter B. Andrews; Eve Longini Cohen (IJCAI, 1977)

Transforming Matings into Natural Deduction Proofs. - Peter B. Andrews (CADE, 1980)

Theorem Proving via General Matings. - Peter B. Andrews (J. ACM, 1981)

A Look at TPS. - Dale A. Miller; Eve Longini Cohen; Peter B. Andrews (CADE, 1982)

An introduction to mathematical logic and type theory - to truth through proof. - Peter B. Andrews (Academic Press, 1986)

The TPS Theorem Proving System. - Peter B. Andrews; Frank Pfenning; Sunil Issar; Carl P. Klapper (CADE, 1986)

On Connections and Higher-Order Logic. - Peter B. Andrews (J. Autom. Reason., 1989)

The TPS Theorem Proving System. - Peter B. Andrews; Sunil Issar; Dan Nesmith; Frank Pfenning (CADE, 1990)

More on the Problem of Finding a Mapping between Clause Representation and Natural Deduction Representation. - Peter B. Andrews (J. Autom. Reason., 1991)

TPS: An Interactive and Automatic Tool for Proving Theorems of Type Theory. - Peter B. Andrews; Matthew Bishop; Sunil Issar; Dan Nesmith; Frank Pfenning; Hongwei Xi (HUG, 1993)

On Sets, Types, Fixed Points, and Checkerboards. - Peter B. Andrews; Matthew Bishop (TABLEAUX, 1996)

TPS: A Theorem-Proving System for Classical Type Theory. - Peter B. Andrews; Matthew Bishop; Sunil Issar; Dan Nesmith; Frank Pfenning; Hongwei Xi (J. Autom. Reason., 1996)

Selectively Instantiating Definitions. - Matthew Bishop; Peter B. Andrews (CADE, 1998)

Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic. - Peter B. Andrews; Chad E. Brown (CADE, 2000)

System Description: TPS: A Theorem Proving System for Type Theory. - Peter B. Andrews; Matthew Bishop; Chad E. Brown (CADE, 2000)

Classical Type Theory. - Peter B. Andrews (Handbook of Automated Reasoning, 2001)

Herbrand Award Acceptance Speech. - Peter B. Andrews (J. Autom. Reason., 2003)

ETPS: A System to Help Students Write Formal Proofs. - Peter B. Andrews; Chad E. Brown; Frank Pfenning; Matthew Bishop; Sunil Issar; Hongwei Xi (J. Autom. Reason., 2004)

Proving Theorems of Type Theory Automatically with TPS. - Peter B. Andrews (AAAI, 2005)

Some Reflections on Proof Transformations. - Peter B. Andrews (Mechanizing Mathematical Reasoning, 2005)

TPS: A hybrid automatic-interactive system for developing proofs. - Peter B. Andrews; Chad E. Brown (J. Appl. Log., 2006)