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 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 August 1, 2003. Historical matters related to Herbrand's theorem, higher-order logic, and the author's work are discussed. Contributions by others that have been helpful to the author are noted.

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.

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 the theorem. While reasonable candidates for quintessential proofs for normal proofs have been developed, more work is needed with regard to non-normal proofs. Work on proof transformations seems likely to lead to important progress in understanding proofs.

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.

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 presented in natural deduction style. ETPS is a program which was obtained from TPS by deleting all the facilities for proving theorems automatically. ETPS can be used by students to learn how to prove theorems interactively. The objective of the tutorial is to teach participants how to make effective use of TPS and ETPS.

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.

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 partial solution to the problem in the context of the connection method; the same solution may also be adaptable to other search procedures. Dual instantiation has been implemented in TPS, a theorem prover for classical type theory, and we provide some examples of theorems that have been proven using this method. Dual instantiation has the desirable properties that the search for a proof cannot possibly fail due to insufficient instantiation of definitions, and that the natural deduction proof which results from a successful search will contain no unnecessary instantiations of definitions. Furthermore, the time taken by a proof search using dual instantiation is in general comparable to the time taken by a search in which exactly the required instances of each definition have been instantiated. We also describe how this technique can be applied to the problem of instantiating set variables.

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.

This is an expository introduction to an approach to theorem proving in higher-order logic based on establishing appropriate connections between subformulas of an expanded form of the theorem to be proved. Expansion trees and expansion proofs play key roles.

The late Cambrian Bowers Group is regressive marine to non-marine. On the basis of associations of textures and sedimentary structures (both primary and biotic), and of palaeocurrent measurements, the sediments of the newly defined Mariner Formation appear to have accumulated on a platform or continental shelf of low gradient and narrow tidal range. Trilobite- and brachiopod-bearing fissile mudstone with sparse channels and scattered stratified sandstone (open marine) is succeeded by wavy-bedded and lenticular-bedded mudstone, muddy sandstone, and rippled sandstone with bands rich in brachiopods (shallow open marine), then mudstone and laminated sandstone with lenticular bodies of oosparite (open marine shoals and protected inner shelf), and red and green, ripple- and parallel-laminated sandstone, interbedded with burrowed muddy sandstone and mudstone, with lenticular bedding (tidal flat). The sharply overlying Camp Ridge Quartzite of cross-bedded sandstone, pebbly sandstone, and sandy pebble conglomerate, is regarded as braided channel alluvium. The detritus appears to have been derived from veined low-grade metamorphic rocks and fine-grained detrital sedimentary rocks that lay south of the area.

The bathymetry, surficial sediments, and benthic assemblages of approximately 1190 km2 of continental shelf and adjoining submarine canyons east of Otago Peninsula are investigated. Pebble and sand fraction composition shows that the detrital sediments have been derived predominantly from the Otago Schists. The sediments are supplied to the continental shelf largely by the Clutha River 72 km south of the area, and are transported north by the combined action of the Southland Current and longshore drift induced by southerly swell. The detrital sediments are polymodal, and by tracing the distribution of five prominent modes it is possible to determine the late Quaternary depositional history in the area. Sandy pebble gravel, which comprises a prominent and continuous band of gravel in mid-shelf position, extends from off the mouth of the Clutha to just north of Otago Peninsula, where it grades into sand. The distribution of sandy pebble gravel off the Clutha shows that it was supplied to the shelf ...

Grain-size distribution and mineralogical composition are independent variables in most detrital sediments. Separate classifications are necessary to describe these sediment attributes. Essential characteristics are given when the following format is used: (sorting term) (size term): (cement) (prominent nondetrital) (detrital composition). This polynomial evokes a clear mental image of the sediment. Descriptive nomenclature and procedure are modified from earlier Folk publications. The resultant classification system is objective and practical. Gravel, sand, silt, and clay are end members of triangular diagrams that are divided into named textural categories in accord with apparent natural groupings. Modal size and sorting terms supplement the names of some categories. Rudite, arenite, and lutite are used in a compositional sense for detrital sediments whose texture is respectively indicated by the terms gravel (conglomerate or breccia), sand (sandstone), and mud (mudstone, siltstone, or clayston...

Summary Reids Rise is a remnant of a marine sand body that accumulated in the inner neritic zone of the continental shelf south‐west of Westport during the Last Interglacial. The sand body is notable for its spectacular sedimentary structures and consists of an upper unit that is characterised by trough cross‐lamination, locally forming mesoscopic ridges, and a lower unit that is characterised by horizontal lamination. The sand body is underlain by gravels of probable alluvial origin. The trough cross‐laminated sets of the upper unit dip off near‐symmetrical ridges that probably formed as subaqueous bars. The dip azimuths of the cross‐laminae have a polymodal distribution with two bimodal maxima, one almost perpendicular to, and the second roughly parallel to the shoreline formed during the Last Interglacial. Magnitude of dip varies from horizontal to over 40°. The sediment is clean, fine sand composed predominantly of angular grains. Sample to sample variation in grain size statistical parameters is smal...

Comparative study of five South Island beaches and a beach on the central Texas coast suggests a short list of features that are diagnostic of the coastal beach. Beach sediments are clean (no mud matrix) and are very well to moderately well sorted. Foreshore strata occur as even, internally laminated, thin beds that dip seaward at low angles. The angle of dip is directly related to the slope of the foreshore surface (especially the beach face), which in turn is largely dependent upon the mean size of the beach sediment, that is, the coarser the grain size the steeper the foreshore. Backshore strata occur as lens- and slightly wedge- shaped, internally laminated thin beds. Scour surfaces and cross-stratified lenses are characteristic. Dip of strata varies from 0° to 15°, and strata dip directly or obliquely landward. A transition zone (foreshore or above high tide level plus outer backshore) is characterised by mixed foreshore and backshore stratification, and some strata dip landward, others dip ...

In [4] Alonzo Church introduced an elegant and expressive formulation of type theory with λ-conversion. In [8] Henkin introduced the concept of a general model for this system, such that a sentence A is a theorem if and only if it is true in all general models. The crucial clause in Henkin's definition of a general model ℳ is that for each assignment φ of values in ℳ to variables and for each wff A, there must be an appropriate value of A in ℳ. Hintikka points out in [10, p. 3] that this constitutes a rather strong requirement concerning the structure of a general model. Henkin draws attention to the problem of constructing nonstandard models for the theory of types in [9, p. 324].We shall use a simple idea of combinatory logic to find a characterization of general models which does not directly refer to wffs, and which is easier to work with in certain contexts. This characterization can be applied, with appropriate minor and obvious modifications, to a variety of formulations of type theory with λ-conversion. We shall be concerned with a language ℒ with extensionality in which there is no description or selection operator, and in which (for convenience) the sole primitive logical constants are the equality symbols Qoαα for each type α.

Results are obtained about special cases of the decision problem for provability in type theory with A-conversion, minus axioms of extensionality, descriptions, choice, and infinity. |&£ . . . ag [A=g] iff there is a substitution 0 such that 9 * A = 0 * B. Hence fA = g iff A conv Jg. This shows the independence of the axioms of extensionality. If £ is quantifier-free, fVjc . . . Vx Q iff r}C is tautologous. Inhere is no decision procedure for the class of wffs of the form 3z [A=B] , or the class of wffs of the form 3g£* where C is quantifier-free. Hence the only solvable classes of wffs in prenex normal form defined solely by the structure of the prefix are those in which no existential quantifiers occur. PROVABILITY IN ELEMENTARY TYPE THEORY by Peter B. Andrews §

In [8] J. A. Robinson introduced a complete refutation procedure called resolution for first order predicate calculus. Resolution is based on ideas in Herbrand's Theorem, and provides a very convenient framework in which to search for a proof of a wff believed to be a theorem. Moreover, it has proved possible to formulate many refinements of resolution which are still complete but are more efficient, at least in many contexts. However, when efficiency is a prime consideration, the restriction to first order logic is unfortunate, since many statements of mathematics (and other disciplines) can be expressed more simply and naturally in higher order logic than in first order logic. Also, the fact that in higher order logic (as in many-sorted first order logic) there is an explicit syntactic distinction between expressions which denote different types of intuitive objects is of great value where matching is involved, since one is automatically prevented from trying to make certain inappropriate matches. (One may contrast this with the situation in which mathematical statements are expressed in the symbolism of axiomatic set theory.).

A refinement of the resolution method for mechanical theorem proving is presented. A resolvent C of clauses A and B is called a merge if literals from A and B merge together to form some literal of C . It is shown that the resolution method remains complete if it is required that two noninitial clauses which are not merges never be resolved with one another. It is also shown that this strategy can be combined with the set-of-support strategy.

The lower part of the Waikari Formation (Otaian) was sampled at 30 localities in North Canterbury. The field relationships, sedimentary structures, textures, and gross compositions of its constituent members are compared with the geographic variation in their grain size parameters (mean size, standard deviation, skewness, and kurtosis). From these data patterns of sedimentation are reconstructed for a basal Otaian depositional surface and for a second depositional surface a little higher in the Otaian stage. At the beginning of Otaian time sediments were accumulating in a single depositional basin, part of a broader continental shelf. The basin was oriented north-north-east and south-south-west, and was bounded by a land ridge on the west and a submarine ridge on the east. Probable tidal flat sediments were deposited in the extreme south-west of the study area and a short distance to the north-east shallowshelf muddy sand, rich in shell fragments was accumulating. Glauconitic sandy silt (mean siz...

In his thesis of 1929 (see [l]) Herbrand showed how to generate effectively from an arbitrary quantificational schema 5 a sequence of quantifier-free expressions Ri(S), Ri(S)t • • • , called reductions (reduites) of 5, and said that S has property C of order p if RP(S), the pth reduction of 5, is truth-functionally valid. (Throughout this paper "effective" will mean "primitive recursive." When reductions are defined below, the reader should observe that a schema has property C of order p only if it has property C for all orders >/>.) Herbrand also gave a set of rules of inference, called rules of passage, the main point of which is to permit an arbitrary schema to be transformed into an equivalent prenex one, and then argued: (I) If, for any given p = 1, 2, 3, • • , a schema S has property C of order p, then any schema T obtained from S solely by the rules of passage also has property C of the same order p. (II) If S and W are any schemata such that S has property C of order p and the schema "15 V W has property C of order g, then the schema W has property C of order max(£, q). (Assertion (I) is Lemma 3 in §3 of Chapter 5 of [l], and assertion (II) is Lemma 3 in §5 of the same chapter.) On the basis of (I) and (II) Herbrand readily established what he called his Fundamental Theorem, varying versions of which are now known as Herbrand's Theorem. More specifically, for a particular axiomatic system 3C of quantification theory which we shall soon describe, Herbrand constructed on the basis of (I) and (II) two effectively computable functions and \f/ such that (1) if D(S) is any derivation in 5C of a quantificational schema 5, then (D(S)) is a truth-functionally valid reduction of S, and (2) if RP(S) is any truth-functionally valid reduction of S, then \l/(Rp(S)) is a derivation of 5 in 3C in which no use is made of modus ponens. But (I) and (II) are false. Indeed, after the necessary background material has been sketched, we shall show that for each p^3 (a) there are schemata 5 and T such that T comes from S by just one application of one rule of passage and S has property C of order 3 but T has property C of no order

It is well known that equality is definable in type theory. Thus, in the language of [2], the equality relation between elements of type α is definable as , i.e., xα = yα iff every set which contains xα also contains yα. However, in a nonstandard model of type theory, the sets may be so sparse that the wff above does not denote the true equality relation. We shall use this observation to construct a general model in the sense of [2] in which the Axiom of Extensionality is not valid. Thus Theorem 2 of [2] is technically incorrect. However, it is easy to remedy the situation by slightly modifying the definition of general model.Our construction will show that the Axiom Schema of Extensionality is independent even if one takes as an axiom schema.We shall assume familiarity with, and use the notation of, [2] and §§2–3 of [1].

A procedure is given for transforming refutation matings into natural deduction proofs. Thus a theorem proving system which establishes the validity of a theorem by the general matings approach can apply this procedure to obtain a comprehensible proof of the theorem without further search. This illuminates the close relationship between matings and proofs, and serves as a step toward a synthesis between apparently quite different approaches to automated theorem proving.

Theorem proving is difficult and deals with complex phenomena. The difficulties seem to be compounded when one works with higher-order logic, but the rich expressive power of Church's formulation [10] [3] of this language makes research on theorem proving in this realm very worthwhile. In order to make significant progress on this problem, we need to try many approaches and ideas, and explore many questions. A highly relevant question is "What makes a logical formula valid?".

When one is seeking an expansion proof for a theorem of higher-order logic, not all necessary substitution terms can be generated by unification of formulas already present, so certain expansion options [5] are applied, and then a search for a p-acceptable mating [2] is made, using Huet's higher-order unification algorithm [8] to generate all remaining substitution terms. The expansion options consist of quantifier duplications and projective and primitive substitutions (such as

It is shown by a purely syntactic argument how the completeness of resolution in type theory implies the consistency of type theory with axioms of extensionality, descriptions, and infinity. In this system the natural numbers are defined, and Peanos Postulates proved; indeed, classical analysis and much more can be formalized here. Nevertheless, Godels results show that the completeness of resolution in type theory cannot be proved in this system. Mathematical Offprint Service classification numbers: O2B15 Higher order predicate calculus O2G99 Methodology of deductive systems 68A40 Theorem proving This research was partially supported by NSF Grant GJ-28457X. Resolution and the Consistency of Analysis Peter B. Andrews §

In [8] J. A. Robinson introduced a complete refutation pro­cedure called resolution for first order predicate calculus. Resolution is based on ideas in Herbrand’s Theorem, and provides a very convenient framework in which to search for a proof of a wff believed to be a theorem. Moreover, it has proved possible to formulate many refinements of resolution which are still complete but are more efficient, at least in many contexts. However, when efficiency is a prime consideration, the restriction to first order logic is unfortunate, since many state­ments of mathematics (and other disciplines) can be expressed more simply and naturally in higher order logic than in first order logic. Also, the fact that in higher order logic (as in many-sorted first order logic) there is an explicit syntactic distinc­tion between expressions which denote different types of intuitive objects is of great value where matching is involved, since one is automatically prevented from trying to make certain inappropriate matches. (One may contrast this with the situation in which mathematical statements are expressed in the symbolism of axiomatic set theory.)

In [3], [4], and [5] Joyce Friedman formulated and investigated certain rules which constitute a semi-decision procedure for wffs of first order predicate calculus in closed prenex normal form with prefixes of the form ∀x1 ...∀xk∃y1 ...∃Ym∀z1 ...∀z n . Given such a wff QM,where Q is the prefix and M is the matrix in conjunctive normal form, Friedman’s rules can be used, in effect, to construct a matrix M* which is obtained from M by deleting certain conjuncts of M. Obviously, ⊢QM⊃QM* Using the Herbrand-Godel theorem for first order predicate calculus, Friedman showed that ⊢QM if and only if ⊢QM*. Clearly if M* is the empty conjunct (i.e., a tautology), ⊢QM* so ⊢QM. Friedman also showed that for certain classes of wffs, such as those in which m ≤ 2 or n = 0 in the prefix above, ⊢QM if and only if M* is the empty conjunct. Hence for such classes of wffs the rules constitute a decision procedure. Computer implementation [4] of the procedure has shown it to be quite efficient by present standards.