Page
%P
-
Chapter
A Bit of History Related to Logic Based on Equality
This historical note illuminates how Leon Henkin’s work influenced that of the author. It focuses on Henkin’s development of a formulation of type theory based on equality, and the significance of this contrib...
-
Chapter
Some Reflections on Proof Transformations
Some general reflections on proof transformations lead to the abstract concept of a quintessential proof of a theorem. A quintessential proof embodies the essential features of many intertranslatable proofs of...
-
Article
ETPS: A System to Help Students Write Formal Proofs
ETPS (Educational Theorem Proving System) is a program that logic students can use to write formal proofs in first-order logic or higher-order logic. It enables students to concentrate on the essential logical...
-
Article
Herbrand Award Acceptance Speech
This is a slightly enhanced version of the acceptance speech given by the author after receiving the Herbrand Award at the 19th International Conference on Automated Deduction (CADE-19) in Miami, Florida, on A...
-
Book
-
Chapter
Introduction
The ability to reason is one of the marvels of human nature. In many situations it is not easy to think logically, but the benefits of doing so are a familiar fact of human experience. Since at least the time ...
-
Chapter
Further Topics in First-Order Logic
We introduce this subject with a parable about two scholars, named Oren and Nero, who were visiting an archaeologist and were shown a recently discovered tablet, the contents of which are reproduced in Figure ...
-
Chapter
Provability and Refutability
We now turn our attention to the practical problems of proving theorems of first-order logic. If one has unlimited resources and patience, one can simply enumerate proofs until one finds a proof of the wff und...
-
Chapter
Type Theory
So far we have been concerned with first-order logic, and its subsystem propositional calculus, which we might regard as zeroth-order logic. We now wish to discuss higher-order logics.
-
Chapter
Incompleteness and Undecidability
Logical systems such as Q 0 ∞ have infinitely many theorems—indeed, infinitely many essentially different theorems—but these theorems are finitely generated. There m...
-
Chapter
First-Order Logic
We next consider first-order logic, which is also called quantification theory and predicate calculus.1 Initially we discuss first-order logic without equality, and then we discuss first-order logic with equality...
-
Chapter
Formalized Number Theory
In the preface to Principia Mathematica, it is stated that “what were formerly taken, tacitly or explicitly, as axioms, are either unnecessary or demonstrable” .1 In this spirit, we shall in this chapter define t...
-
Chapter
Propositional Calculus
As discussed in the Introduction, we can study the nature of reasoning by studying logistic systems in which reasoning is represented in a precise way. We shall commence our study with a rather simple logistic...
-
Chapter and Conference Paper
Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic
TPS is an automated theorem proving system which can be used to prove theorems of first- or higher-order logic automatically, interactively, or in a combination of these modes of operation. Proofs in TPS are p...
-
Chapter and Conference Paper
System Description: TPS: A Theorem Proving System for Type Theory
This is a brief update on the Tps automated theorem proving system for classical type theory, which was described in [3]. Manuals and information about obtaining Tps can be found at http://gtps.math.cmu.edu/tps.h...
-
Chapter and Conference Paper
Selectively instantiating definitions
When searching for proofs of theorems which contain definitions, it is a significant problem to decide which instances of the definitions to instantiate. We describe a method called dual instantiation, which is a...
-
Article
TPS: A theorem-proving system for classical type theory
This is 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- and higher-order log...
-
Chapter and Conference Paper
On sets, types, fixed points, and checkerboards
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 certain contex...
-
Chapter and Conference Paper
TPS: An interactive and automatic tool for proving theorems of type theory
This is a demonstration of TPS, a theorem proving system for classical type theory (Church's typed λ-calculus). TPS can be used interactively or automatically, or in a combination of these modes. An important ...
-
Article
More on the problem of finding a map** between clause representation and natural-deduction representation
