Some Useful Commands in TPS (2008)
Peter B. Andrews, Peter B. Andrews, Eve Longini Cohen, Dale A. Miller, Ph. D, Dan Nesmith, ...
[ ∼ A] means “A is not true”; [A ∧ B] means “A and B”; [A ∨ B] means “A or B”; [A ⊃ B] means “A implies B”; [A ≡ B] means “A if and only if B”; When the relative scopes...
TPS: A Theorem Proving Systemfor Classical Type Theory (2008)
Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi
AbstractThis is a description of T PS, a theorem proving system for classical type theory (Church's typedl-calculus). T PS has been designed to be a general research tool for manipulating wffs...
ETPS: A System to Help Students Write Formal Proofs (2008)
Peter B. Andrews, Matthew Bishop, Chad E. Brown, Sunil Issar, Frank Pfenning, Hongwei Xi
ETPS (Educational Theorem Proving System) is a program which logic students can use to write formal proofs in first-order logic or higher-order logic. It enables students to concentrate on the...
ETPS: A System to Help Students Write Formal Proofs (2007)
Peter B. Andrews, Matthew Bishop, Chad E. Brown, Sunil Issar, Frank Pfenning, Hongwei Xi
ETPS (Educational Theorem Proving System) is a program which logic students can use to write formal proofs in rst-order logic or higher-order logic. It enables students to concentrate on the...
ETPS: A System to Help Students Write Formal Proofs (2003)
Peter B. Andrews, Matthew Bishop, Chad E. Brown, Sunil Issar, Frank Pfenning, Hongwei Xi
ETPS (Educational Theorem Proving System) is a program which logic students can use to write formal proofs in first-order logic or higher-order logic. It enables students to concentrate on the...
Herbrand award acceptance speech (2003)
Peter B. Andrews, Peter B. Andrews\lambda
presented toPeter Andrews theory, mating-based theorem proving, automated deductionin higher-order logic, proof presentation, logic education and his many other contributions to the field of...
ETPS: A System to Help Students Write Formal Proofs (2003)
Chad E. Brown, Peter B. Andrews, Peter B. Andrews, Matthew Bishop, Matthew Bishop, Sunil Issar, ...
ETPS (Educational Theorem Proving System) is a program which logic students can use to write formal proofs in rst-order logic or higher-order logic. It enables students to concentrate on the...
ETPS: A System to Help Students Write Formal Proofs (2003)
Peter Andrews, Peter B. Andrews, Chad E. Brown, Chad E. Brown, Matthew Bishop, Matthew Bishop, ...
ETPS (Educational Theorem Proving System) is a program which logic students can use to write formal proofs in first-order logic or higher-order logic. It enables students to concentrate on the...
Peter B. Andrews, Michael Kohlhase
Contents 1 Introduction to type theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 967 1.1 Early versions of type theory . . . . . . . . . . . . . . . . . . . . . . . . . . . ....
On Sets, Types, Fixed Points, and Checkerboards (1996)
Peter B. Andrews, Matthew Bishop
Most current research on automated theorem proving is concerned with proving theorems of first-order logic. We discuss two examples which illustrate the advantages of using higher-order logic in...
tps: A theorem proving system for classical type theory (1996)
Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi
This is a description of TPS, a theorem proving system for classical type theory (Church’s typed λ-calculus). TPS has been designed to be a general research tool for manipulating wffs of first-...
TPS: An Interactive and Automatic Tool for Proving Theorems of Type Theory (1994)
Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi, ...
This is a demonstration of TPS, a theorem proving system for classical type theory (Church's typed l-calculus). TPS can be used interactively or automatically, or in a combination of these...
TPS: A Theorem Proving System for Classical Type Theory (1994)
Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi
This is a description of TPS, a theorem proving system for classical type theory (Church's typed l-calculus). TPS has been designed to be a general research tool for manipulating wffs of first-...
Theorem proving in type theory (1977)
Peter B. Andrews, Eve Longini Cohen
As one aspect of the endeavor to create new intellectual tools for mankind, we wish to enable computers to prove, and to assist in the proofs of, theorems of mathematics and (eventually) other...
Facies and genesis of a hurricane washover fan, St. Joseph Island, Central Texas Coast. (1967)
Thesis (Ph. D.)--University of Texas, 1967.