| 2006 |
|---|
| 29 | EE | 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 | EE | Peter B. Andrews:
Some Reflections on Proof Transformations.
Mechanizing Mathematical Reasoning 2005: 14-29 |
| 2004 |
|---|
| 26 | EE | 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 | EE | 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 | EE | 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 | EE | 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 | EE | Peter B. Andrews:
Resolution With Merging.
J. ACM 15(3): 367-381 (1968) |
| 2 | EE | 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) |
