Search

We have formalized material from an introductory real analysis textbook in the proof assistant Scunak. Scunak is a system based on set theory encoded in a dependent type theory. We use the formalized material to illustrate some interesting aspects of the relationship between informal presentations of mathematics and their formal representation. We focus especially on a representative example proved using the system. [ABSTRACT FROM AUTHOR]

Many textbook proofs are essentially human-readable representations of natural deduction proofs. Terms in dependent type theory provide formally checkable representations of natural deduction proofs. We show how the new mathematical assistant system Scunak can be used to verify a textbook proof by translating the version into a proof term in a dependent type theory. We also show how Scunak can give interesting output upon failure. [ABSTRACT FROM AUTHOR]

We investigate cut-elimination and cut-simulation in impredicative (higher-order) logics. We illustrate that adding simple axioms such as Leibniz equations to a calculus for an impredicative logic — in our case a sequent calculus for classical type theory — is like adding cut. The phenomenon equally applies to prominent axioms like Boolean- and functional extensionality, induction, choice, and description. This calls for the development of calculi where these principles are built-in instead of being treated axiomatically. [ABSTRACT FROM AUTHOR]

We describe a dependent type theory with proof irrelevance. Within this framework, we give a representation of a form of Mac Lane set theory and discuss automated support for constructing proofs within this set theory. One of the novel aspects of the representation is that one is allowed to use any class (in the set theory) as a type (in the type theory). Such class types allow a natural way of representing partial functions (e.g., the first and second operators on the class of Kuratowski ordered pairs). We also discuss how automated search can be used to construct proofs. In particular, the first-order prover Vampire can be called to solve a challenge problem (the injective Cantor Theorem) which is notoriously difficult for higher-order automated provers. [ABSTRACT FROM AUTHOR]

We describe methods for automated theorem proving in extensional type theory with primitive equality. We discuss a complete, cut-free sequent calculus as well as a compact representation of cut-free (ground) proofs as extensional expansion dags. Automated proof search can be realized using a few operations to manipulate extensional expansion dags with variables. These search operations form a basis for complete search procedures. Procedures based on these ideas are implemented in the higher-order theorem prover Tps. [ABSTRACT FROM AUTHOR]

We present a set of problems that may support the development of calculi and theorem provers for classical higher-order logic. We propose to employ these test problems as quick and easy criteria preceding the formal soundness and completeness analysis of proof systems under development. Our set of problems is structured according to different technical issues and along different notions of semantics (including Henkin semantics) for higher-order logic. Many examples are either theorems or non-theorems depending on the choice of semantics. The examples can thus indicate the deductive strength of a proof system. [ABSTRACT FROM AUTHOR]

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. In Section 2 we discuss some examples of theorems which Tps can now prove automatically, and in Section 3 we discuss an example which illustrates one of the many challenges of theorem proving in higher-order logic. We first provide a brief summary of the key features of Tps. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]