Peter B. Andrews

Publication Activity (10 Years)

Years Active: 1968-2006
Publications (10 Years): 0

Publications

Peter B. Andrews, Chad E. Brown
TPS: A hybrid automatic-interactive system for developing proofs. J. Appl. Log. 4 (4) (2006)
Peter B. Andrews
Proving Theorems of Type Theory Automatically with TPS. AAAI (2005)
Peter B. Andrews
Some Reflections on Proof Transformations. Mechanizing Mathematical Reasoning (2005)
Peter B. Andrews, Chad E. Brown, Frank Pfenning, Matthew Bishop, Sunil Issar, Hongwei Xi
ETPS: A System to Help Students Write Formal Proofs. J. Autom. Reason. 32 (1) (2004)
Peter B. Andrews
Herbrand Award Acceptance Speech. J. Autom. Reason. 31 (2) (2003)
Peter B. Andrews, Matthew Bishop, Chad E. Brown
System Description: TPS: A Theorem Proving System for Type Theory. CADE (2000)
Peter B. Andrews, Chad E. Brown
Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic. CADE (2000)
Matthew Bishop, Peter B. Andrews
Selectively Instantiating Definitions. CADE (1998)
Peter B. Andrews, Matthew Bishop
On Sets, Types, Fixed Points, and Checkerboards. TABLEAUX (1996)
Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi
TPS: A Theorem-Proving System for Classical Type Theory. J. Autom. Reason. 16 (3) (1996)
Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi
TPS: An Interactive and Automatic Tool for Proving Theorems of Type Theory. HUG (1993)
Peter B. Andrews
More on the Problem of Finding a Mapping between Clause Representation and Natural Deduction Representation. J. Autom. Reason. 7 (2) (1991)
Peter B. Andrews, Sunil Issar, Dan Nesmith, Frank Pfenning
The TPS Theorem Proving System. CADE (1990)
Peter B. Andrews
On Connections and Higher-Order Logic. J. Autom. Reason. 5 (3) (1989)
Peter B. Andrews, Sunil Issar, Daniel Nesmith, Frank Pfenning
The TPS Theorem Proving System. CADE (1988)
Peter B. Andrews, Frank Pfenning, Sunil Issar, Carl P. Klapper
The TPS Theorem Proving System. CADE (1986)
Peter B. Andrews
Connections and Higher-Order Logic. CADE (1986)
Dale A. Miller, Eve Longini Cohen, Peter B. Andrews
A Look at TPS. CADE (1982)
Peter B. Andrews
Theorem Proving via General Matings. J. ACM 28 (2) (1981)
Peter B. Andrews
Transforming Matings into Natural Deduction Proofs. CADE (1980)
Peter B. Andrews, Eve Longini Cohen
Theorem Proving in Type Theory. IJCAI (1977)
Peter B. Andrews
Refutations by Matings. IEEE Trans. Computers 25 (8) (1976)
Peter B. Andrews
Resolution and the consistency of analysis. Notre Dame J. Formal Log. 15 (1) (1974)
Peter B. Andrews
General Models, Descriptions, and Choice in Type Theory. J. Symb. Log. 37 (2) (1972)
Peter B. Andrews
General Models and Extensionality. J. Symb. Log. 37 (2) (1972)
Peter B. Andrews
Resolution in Type Theory. J. Symb. Log. 36 (3) (1971)
Peter B. Andrews
On Simplifying the Matrix of a WFF. J. Symb. Log. 33 (2) (1968)
Peter B. Andrews
A Correction Concerning Resolution. J. ACM 15 (4) (1968)
Peter B. Andrews
Resolution With Merging. J. ACM 15 (3) (1968)