Peter B. Andrews

Peter B. Andrews, Chad E. Brown: TPS: A hybrid automatic-interactive system for developing proofs. J. Applied Logic 4(4): 367-395 (2006)

Peter B. Andrews: Proving Theorems of Type Theory Automatically with TPS. AAAI 2005: 1676-1677

Peter B. Andrews: Some Reflections on Proof Transformations. Mechanizing Mathematical Reasoning 2005: 14-29

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. Reasoning 32(1): 75-92 (2004)

Peter B. Andrews: Herbrand Award Acceptance Speech. J. Autom. Reasoning 31(2): 169-187 (2003)

Peter B. Andrews: Classical Type Theory. Handbook of Automated Reasoning 2001: 965-1007

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

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

Matthew Bishop, Peter B. Andrews: Selectively Instantiating Definitions. CADE 1998: 365-380

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

Peter B. Andrews, Matthew Bishop: On Sets, Types, Fixed Points, and Checkerboards. TABLEAUX 1996: 1-15

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: 366-370

Peter B. Andrews: More on the Problem of Finding a Mapping between Clause Representation and Natural Deduction Representation. J. Autom. Reasoning 7(2): 285-286 (1991)

Peter B. Andrews, Sunil Issar, Dan Nesmith, Frank Pfenning: The TPS Theorem Proving System. CADE 1990: 641-642

Peter B. Andrews: On Connections and Higher-Order Logic. J. Autom. Reasoning 5(3): 257-291 (1989)

Peter B. Andrews, Sunil Issar, Daniel Nesmith, Frank Pfenning: The TPS Theorem Proving System. CADE 1988: 760-761

Peter B. Andrews: An introduction to mathematical logic and type theory - to truth through proof. Computer science and applied mathematics, Academic Press 1986, isbn 978-0-12-058535-9, pp. I-XV, 1-304

Peter B. Andrews: Connections and Higher-Order Logic. CADE 1986: 1-4

Peter B. Andrews, Frank Pfenning, Sunil Issar, C. P. Klapper: The TPS Theorem Proving System. CADE 1986: 663-664

Dale Miller, Eve Longini Cohen, Peter B. Andrews: A Look at TPS. CADE 1982: 50-69

Peter B. Andrews: Theorem Proving via General Matings. J. ACM 28(2): 193-214 (1981)

Peter B. Andrews: Transforming Matings into Natural Deduction Proofs. CADE 1980: 281-292

Peter B. Andrews, Eve Longini Cohen: Theorem Proving in Type Theory. IJCAI 1977: 566-566

Peter B. Andrews: Refutations by Matings. IEEE Trans. Computers 25(8): 801-807 (1976)

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

Peter B. Andrews: General Models and Extensionality. J. Symb. Log. 37(2): 395-397 (1972)

Peter B. Andrews: Resolution in Type Theory. J. Symb. Log. 36(3): 414-432 (1971)

Peter B. Andrews: Resolution With Merging. J. ACM 15(3): 367-381 (1968)

Peter B. Andrews: A Correction Concerning Resolution. J. ACM 15(4): 720 (1968)

Peter B. Andrews: On Simplifying the Matrix of a WFF. J. Symb. Log. 33(2): 180-192 (1968)