Narrow Results

We embed a first order theory with equality in the Pure Type System λMON2 that is a subsystem of the well-known type system λPRED2. The embedding is based on the Curry-Howard isomorphism, i.e. → and ∀ coincide with → and Π. Formulas of the form are treated as Leibniz equalities. That is, is identified with the second order formula ∀ P. P(t₁)→ P(t₂), which contains only →'s and ∀'s and can hence be embedded straightforwardly. We give a syntactic proof — based on enriching typed λ-calculus with extra reduction steps — for the equivalence between derivability in the logic and inhabitance in λMNO2. Familiarity with Pure Type Systems is assumed.

Automated theorem provers use search strategies. Unfortunately, there is no unique strategy which is uniformly successful on all problems. This motivates us to apply different strategies in parallel, in a competitive manner. In this paper, we discuss properties, problems, and perspectives of strategy parallelism in theorem proving. We develop basic concepts like the complementarity and the overlap value of strategy sets. Some of the problems such as initial strategy selection and run-time strategy exchange are discussed in more detail. The paper also contains the description of an implementation of a strategy parallel theorem prover (p-SETHEO) and an experimental evaluation.

Automated theorem proving with connection tableau calculi imposes search problems in tremendous search spaces. In this paper, we present a new approach to search space reduction in connection tableau calculi. In our approach structurally similar parts of the search space are compressed by means of disjunctive constraints. We describe the necessary changes of the calculus, and we develop elaborate techniques for an efficient constraint processing. Moreover, we present an experimental evaluation of our approach.

Darwin is the first implementation of the Model Evolution Calculus by Baumgartner and Tinelli. The Model Evolution Calculus lifts the DPLL procedure to first-order logic. Darwin is meant to be a fast and clean implementation of the calculus, showing its effectiveness and providing a base for further improvements and extensions.

Based on a brief summary of the Model Evolution Calculus, we describe in the main part of the paper Darwin's proof procedure and its data structures and algorithms, discussing the main design decisions and features that influence Darwin's performance. We also report on practical experiments carried out with problems from the CASC-J2 system competition and parts of the TPTP Problem Library, and compare the results with those of other state-of-the-art theorem provers.

We describe a system for the automated certification of safety properties of NASA software. The system uses Hoare-style program verification technology to generate proof obligations which are then processed by an automated first-order theorem prover (ATP). We discuss the unique requirements this application places on the ATPs, focusing on automation, proof checking, traceability, and usability, and describe the resulting system architecture, including a certification browser that maintains and displays links between obligations and source code locations. For full automation, the obligations must be aggressively preprocessed and simplified, and we demonstrate how the individual simplification stages, which are implemented by rewriting, influence the ability of the ATPs to solve the proof tasks. Our results are based on 13 comprehensive certification experiments that lead to 366 top-level safety obligations and ultimately to more than 25,000 proof tasks which have been used to determine the suitability of the high-performance provers DCTP, E-Setheo, E, Gandalf, Otter, Setheo, Spass, and Vampire, and our associated infrastructure. The proofs found by Otter have been checked by Ivy.

Automated Theorem Proving (ATP) systems are complex pieces of software, and thus may have bugs that make them unsound. In order to guard against unsoundness, the derivations output by an ATP system may be semantically verified by trusted ATP systems that check the required semantic properties of each inference step. Such verification needs to be augmented by structural verification that checks that inferences have been used correctly in the context of the overall derivation. This paper describes techniques for semantic verification of derivations, and reports on their implementation and testing in the GDV verifier.

CREACOMP provides an electronic environment for learning and teaching mathematics that aims at inspiring the creative potential of students. During their learning process, students are encouraged to engage themselves in various kinds of interactive experiments, both of visual and purely formal mathematical nature. The computer-algebra system Mathematica powers the visualization of mathematical concepts and the tools provided by the theorem proving system Theorema are used for the formal counterparts. We present a case study on the concept of equivalence relations and set partitions, in which we demonstrate the entire bandwidth of computer-support that we envision for modern learning environments for mathematics.

In this paper we present a set of clauses for set theory, thus developing a foundation for the expression of most theorems of mathematics in a form acceptable to a resolution-based automated theorem prover. Because Gödel's formulation of set theory permits presentation in a finite number of first-order formulas, we employ it rather than that of Zermelo-Fraenkel. We illustrate the expressive power of this formulation by providing statements of some well-known open questions in number theory, and give some intuition about how the axioms are used by including some sample proofs. A small set of challenge problems is also given.

We present in this article an application of automated theorem proving to a study of a theorem in combinatory logic. The theorem states: the strong fixed point property is satisfied in a system that contains the B and W fR combinators. The theorem can be stated in terms of Smullyan's forests of birds: a sage exists in a forest that contains a bluebird and a warbler. Proofs of the theorem construct sages from B and W. Prior to the study, one sage, discovered by Statman, was known to exist. During the study, with much assistance from two automated theorem-proving programs, four new sages were discovered. The study was conducted from a syntactic point of view because the authors know very little about combinatory logic. The uses of the automated theorem-proving programs are described in detail.

This article discusses the two incarnations of Otter entered in the CADE-13 Automated Theorem Proving Competition. Also presented are some historical background, a summary of applications that have led to new results in mathematics and logic, and a general discussion of Otter.