Peter B. Andrews

	2006
29		Peter B. Andrews, Chad E. Brown: TPS: A hybrid automatic-interactive system for developing proofs. J. Applied Logic 4(4): 367-395 (2006)
	2005
28		Peter B. Andrews: Proving Theorems of Type Theory Automatically with TPS. AAAI 2005: 1676-1677
27		Peter B. Andrews: Some Reflections on Proof Transformations. Mechanizing Mathematical Reasoning 2005: 14-29
	2004
26		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)
	2003
25		Peter B. Andrews: Herbrand Award Acceptance Speech. J. Autom. Reasoning 31(2): 169-187 (2003)
	2001
24		Peter B. Andrews: Classical Type Theory. Handbook of Automated Reasoning 2001: 965-1007
	2000
23		Peter B. Andrews, Matthew Bishop, Chad E. Brown: System Description: TPS: A Theorem Proving System for Type Theory. CADE 2000: 164-169
22		Peter B. Andrews, Chad E. Brown: Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic. CADE 2000: 511-512
	1998
21		Matthew Bishop, Peter B. Andrews: Selectively Instantiating Definitions. CADE 1998: 365-380
	1996
20		Peter B. Andrews, Matthew Bishop: On Sets, Types, Fixed Points, and Checkerboards. TABLEAUX 1996: 1-15
19		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)
	1993
18		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
	1991
17		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)
	1990
16		Peter B. Andrews, Sunil Issar, Dan Nesmith, Frank Pfenning: The TPS Theorem Proving System. CADE 1990: 641-642
	1989
15		Peter B. Andrews: On Connections and Higher-Order Logic. J. Autom. Reasoning 5(3): 257-291 (1989)
	1988
14		Peter B. Andrews, Sunil Issar, Daniel Nesmith, Frank Pfenning: The TPS Theorem Proving System. CADE 1988: 760-761
	1986
13		Peter B. Andrews: Connections and Higher-Order Logic. CADE 1986: 1-4
12		Peter B. Andrews, Frank Pfenning, Sunil Issar, C. P. Klapper: The TPS Theorem Proving System. CADE 1986: 663-664
	1982
11		Dale Miller, Eve Longini Cohen, Peter B. Andrews: A Look at TPS. CADE 1982: 50-69
	1981
10		Peter B. Andrews: Theorem Proving via General Mappings. J. ACM 28(2): 193-214 (1981)
	1980
9		Peter B. Andrews: Transforming Matings into Natural Deduction Proofs. CADE 1980: 281-292
	1977
8		Peter B. Andrews, Eve Longini Cohen: Theorem Proving in Type Theory. IJCAI 1977: 566-566
	1976
7		Peter B. Andrews: Refutations by Matings. IEEE Trans. Computers 25(8): 801-807 (1976)
	1972
6		Peter B. Andrews: General Models, Descriptions, and Choice in Type Theory. J. Symb. Log. 37(2): 385-394 (1972)
5		Peter B. Andrews: General Models and Extensionality. J. Symb. Log. 37(2): 395-397 (1972)
	1971
4		Peter B. Andrews: Resolution in Type Theory. J. Symb. Log. 36(3): 414-432 (1971)
	1968
3		Peter B. Andrews: Resolution With Merging. J. ACM 15(3): 367-381 (1968)
2		Peter B. Andrews: A Correction Concerning Resolution. J. ACM 15(4): 720 (1968)
1		Peter B. Andrews: On Simplifying the Matrix of a WFF. J. Symb. Log. 33(2): 180-192 (1968)

Coauthor Index

1	Matthew Bishop	[18] [19] [20] [21] [23] [26]
2	Chad E. Brown	[22] [23] [26] [29]
3	Eve Longini Cohen	[8] [11]
4	Sunil Issar	[12] [14] [16] [18] [19] [26]
5	C. P. Klapper	[12]
6	Dale Miller	[11]
7	Daniel Nesmith (Dan Nesmith)	[14] [16] [18] [19]
8	Frank Pfenning	[12] [14] [16] [18] [19] [26]
9	Hongwei Xi	[18] [19] [26]