Peter B. Andrews

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