Search

The theorem proving system Tps provides support for constructing proofs using a mix of automation and user interaction, and for manipulating and inspecting proofs. Its library facilities allow the user to store and organize work. Mathematical theorems can be expressed very naturally in Tps using higher-order logic. A number of proof representations are available in Tps , so proofs can be inspected from various perspectives.

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 problems involved in proving theorems, and it automatically checks the proofs.

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 contribution.

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 logic, and searching for proofs of such wffs interactively or automatically, or in a combination of these modes. An important feature of TPS is the ability to translate between expansion proofs and natural deduction proofs. Examples of theorems that TPS can prove completely automatically are given to illustrate certain aspects of TPS's behavior and problems of theorem proving in higher-order logic.

Certain aspects of the theorem proving system TPS are described. Type theory with λ-abstraction has been chosen as the logical language of TPS so that statements from many fields of mathematics and other disciplines can be expressed in terms accessible to the system.

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 under consideration (provided, of course, that it actually is a theorem). As a practical matter, however, one usually wishes to find a proof as quickly and easily as possible, so various methods have been devised to facilitate efficient searches for proofs. We shall discuss some of these methods in this chapter, along with various results related to them.

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 4.1. They soon realized that the figures on the tablet were truth tables, and they set about translating them into more familiar notations. (Before proceeding further, the reader is advised to do this for himself for at least a few of the tables.) Oren produced the translation in Figure 4.2, and Nero produced that in Figure 4.3. As they started to show their translations to the archaeologist, Nero modestly remarked “That was really quite easy, as soon as I realized that ⊕ denoted conjunction”. “But you’re wrong!” exclaimed Oren. “⊕ denoted disjunction!” They argued for some time, and neither was able to persuade the other that he was wrong. All they could agree on was that ⊖ denoted negation.

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 the natural numbers as the finite cardinals, and derive Peano’s Postulates from an Axiom of Infinity. We then establish those results about natural numbers and recursive functions which we need in order to establish the incompleteness results in Chapter 7.

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 in §26.

Logical systems such as Q 0 ∞ have infinitely many theorems—indeed, infinitely many essentially different theorems—but these theorems are finitely generated. There may be infinitely many axioms, but a finite description in the meta-language suffices to specify them. Wffs are finite, and proofs are finite. Such features seem to be inescapable characteristics of logical systems which can actually be used by finite, mortal men.

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.html.

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 feature of TPS is the ability to translate between expansion proofs and natural deduction proofs.

A small block (8.4 km2) of Upper Triassic Torlesse Supergroup rocks is mapped and described. Three sedimentary facies and one probably volcanogenic facies are recognised. They are interstratified and grade laterally into one another. Very thick-bedded sandstone occurs in wedging units up to 450 m thick. It consists mostly of massive, moderately sorted, medium-fine sandstone with scattered zones of parallel lamination, gently inclined lamination, and ripple cross-lamination. Penecontemporaneous black mudstone clasts occur widely. The facies is unfossiliferous. Thin-bedded siltstone forms units up to 95 m thick. It consists of very thin and thin beds of parallel-laminated, small-scale ripple cross-laminated, and deformed cross-laminated, moderately to well sorted coarse siltstone or silty very fine sandstone, alternating with homogeneous or mottled black mudstone. The worm tubes Titahia and Torlessia and feeding trails are widespread. Black mudstone occurs in units up to 150 m thick. It is characte...

Modern sand and silty sand cover the inner shelf, with silty sand accumulating off the mouth of the Clutha River. Palimpsest sediment dominated by shell debris and polymodal detrital gravel and sand covers the outer shelf. The detrital sediment is largely or wholly of Clutha River origin.

Many Deep Sea Drilling Project drillholes in circum-Antarctic regions penetrated a basal euxinic claystone facies. The facies is dark-coloured, organic carbon and pyrite-rich, very sparsely fossiliferous, massive to burrow-mottled detrital claystone and silty claystone. At some sites redeposited silt and sand is intercalated with the facies. The facies accumulated relatively rapidly, under stagnant or restricted circulation bottom conditions. On subsided fragments of continental crust (Falkland Plateau, Campbell Plateau) the euxinic claystone facies succeeds transgressive non-marine to marine sequences; in near-continent positions it overlies the oldest oceanic crust. The former relationship appears to mark the rifting phase and the latter the early spreading phase of ocean basin development in circum-Antarctic and other Southern Hemisphere regions. Persistent oceanic biogenic sediment eventually succeeds the claystone facies at each drillsite. In the younger parts of an ocean basin biogenic sediment lies directly on oceanic crust. The change from claystone to biogenic sediment occurs earliest in first-formed oceanic basins and latest in young basins. The change appears to mark the moment when each basin had grown to sufficient size through sea-floor spreading for a thermohaline circulation to develop.