Peter B. Andrews

According to our database, Peter B. Andrews authored at least 29 papers between 1968 and 2006.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2006

TPS: A hybrid automatic-interactive system for developing proofs.

Peter B. Andrews, Chad E. Brown

J. Appl. Log., 2006

2005

Some Reflections on Proof Transformations.

Peter B. Andrews

Proceedings of the Mechanizing Mathematical Reasoning, 2005

Proving Theorems of Type Theory Automatically with TPS.

Peter B. Andrews

Proceedings of the Proceedings, 2005

2004

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

2003

Herbrand Award Acceptance Speech.

Peter B. Andrews

J. Autom. Reason., 2003

2001

Classical Type Theory.

Peter B. Andrews

Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

2000

System Description: TPS: A Theorem Proving System for Type Theory.

Peter B. Andrews, Matthew Bishop, Chad E. Brown

Proceedings of the Automated Deduction, 2000

Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic.

Peter B. Andrews, Chad E. Brown

Proceedings of the Automated Deduction, 2000

1998

Selectively Instantiating Definitions.

Matthew Bishop, Peter B. Andrews

Proceedings of the Automated Deduction, 1998

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

On Sets, Types, Fixed Points, and Checkerboards.

Peter B. Andrews, Matthew Bishop

Proceedings of the Theorem Proving with Analytic Tableaux and Related Methods, 1996

1993

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

Proceedings of the Higher Order Logic Theorem Proving and its Applications, 1993

1991

More on the Problem of Finding a Mapping between Clause Representation and Natural Deduction Representation.

Peter B. Andrews

J. Autom. Reason., 1991

1990

The TPS Theorem Proving System.

Peter B. Andrews, Sunil Issar, Dan Nesmith, Frank Pfenning

Proceedings of the 10th International Conference on Automated Deduction, 1990

1986

The TPS Theorem Proving System.

Peter B. Andrews, Frank Pfenning, Sunil Issar, Carl P. Klapper

Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 27, 1986

Connections and Higher-Order Logic.

Peter B. Andrews

Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 27, 1986

An introduction to mathematical logic and type theory - to truth through proof.

Peter B. Andrews

Computer science and applied mathematics, Academic Press, ISBN: 978-0-12-058535-9, 1986

1982

A Look at TPS.

Dale A. Miller, Eve Longini Cohen, Peter B. Andrews

Proceedings of the 6th Conference on Automated Deduction, 1982

1981

Theorem Proving via General Matings.

Peter B. Andrews

J. ACM, 1981

1980

Transforming Matings into Natural Deduction Proofs.

Peter B. Andrews

Proceedings of the 5th Conference on Automated Deduction, 1980

1977

Theorem Proving in Type Theory.

Peter B. Andrews, Eve Longini Cohen

Proceedings of the 5th International Joint Conference on Artificial Intelligence. Cambridge, 1977

1976

Refutations by Matings.

Peter B. Andrews

IEEE Trans. Computers, 1976

1974

Resolution and the consistency of analysis.

Peter B. Andrews

Notre Dame J. Formal Log., 1974

1972

General Models and Extensionality.

Peter B. Andrews

J. Symb. Log., 1972

General Models, Descriptions, and Choice in Type Theory.

Peter B. Andrews

J. Symb. Log., 1972

1971

Resolution in Type Theory.

Peter B. Andrews

J. Symb. Log., 1971

1968

On Simplifying the Matrix of a WFF.

Peter B. Andrews

J. Symb. Log., 1968

A Correction Concerning Resolution.

Peter B. Andrews

J. ACM, 1968

Resolution With Merging.

Peter B. Andrews

J. ACM, 1968