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 inflence Darwin's performance. We also report on practical experiments carried out with problems from the CADE-18 and CADE-19 system competitions, as well as on results on parts of the TPTP problem library.
We describe feature vector indexing, a new, non-perfect indexing method for clause subsumption. It is suitable for both forward (i.e. finding a subsuming clause in a set) and backward (finding all subsumed clauses in a set) subsumption. Moreover, it is easy to implement, but still yields excellent performance in practice. As an added benefit, by restricting the selection of features used in the index, our technique immediately adapts to indexing modulo arbitrary AC theories with only minor loss of efficiency. Alternatively, the feature selection can be restricted to result in set subsumption. Feature vector indexing has been implemented in our equational theorem prover E, and has enabled us to integrate new simplification techniques making heavy use of subsumption. We experimentally compare the performance of the prover for a number of strategies using feature vector indexing and conventional sequential subsumption.
The Lexicographic Path Ordering (LPO) poses an interesting problem to the implementor: How to achieve a version that is both efficient (i. e., polynomial) and correct? The method of program transformation helps us to develop an efficient version step-by-step, making clear the essential ideas, while retaining correctness. Detailed measurements show besides theoretical analysis the practical improvements of the different variants. They allow us to assess experimentally various optimizations suggested for LPO.
Perfect Developer is a tool for developing software specifications, refining them to code and performing formal verification. Automated reasoning is key to the verification phase, since software developers generally have neither the time nor the skill needed to participate in proving verification conditions. Thanks to the maturity of automated reasoning technology, Perfect Developer now routinely achieves successful proof rates of 98% to 100% in some commercial application domains. This talk will focus on the requirements for provers used in software verification, the sorts of theorems they are required to prove, problems they face, and techniques we have successfully employed.
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, and usability. For full automation, however, 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 certification experiments that lead to more than 25,000 proof tasks which have each been attempted by Vampire, Spass, e-setheo, and Otter. The proofs found by Otter have been proof-checked by IVY.
MoMM (in the narrower sense) is a tool allowing fast interreduction of a high number of clauses, dumping and fast-loading of the interreduced clause sets, and their use for real-time retrieval of matching clauses in an interactive mode. MoMM's main task is now providing these services for the world's largest body of formalized mathematics - the Mizar Mathematical Library (MML), which uses a richer formalism than just pure predicate logic. This task leads to a number of features (strength, speed, memory e ciency, dealing with the richer Mizar logic, etc.) required from MoMM, and we describe the choices taken in its implementation corresponding to these requirements. An important part of MoMM (in the wider sense) are the tools exporting the richer logic of MML into the clause-like format suitable for fast interreduction, and the tools allowing the use of MoMM as an interactive advisor for the authors of Mizar articles. These tools and choices taken in their implementation are also described here. Finally, the results of the interreduction of MML are described, and some problems and possible future work are discussed.
In the beginning (the early 1960s), the long-term goal of automated deduction was the design and implementation of a program whose use would lead to 'real' and significant contributions to mathematics by offering sufficient power for the discovery of proofs. The realization of that goal appeared to be at least six decades in the future. However, with amazement and satisfaction, we can report that less than four decaides were required. In this article, we present evidence for this claim, thanks to W. McCune's program OTTER. Our focus is on various lanmarks, or milestones, of two types. One type concerns the formulation of new strategies and methodologies whose use greatly enhances the power of a reasoning program. A second type focuses on actual contributions to mathematics and (although not initially envisioned) to logic. We give examples of each type of milestone, and, perhaps of equal importance, demonstrate that advances are far more likely to occur if the two classes are indeed intertwined. We draw heavily on material presented in great detail in the new book Automated Reasoning and the Discovery of Missing and Elegant Proofs, published by Rinton Press.
Support for lambda calculus and an algorithm for untyped lambda-unification has been implemented in the source code of Otter. This is the first time that a resolution-based, clause-language prover (that accumulates deduced clauses and uses strategies to control the deduction and retention of clauses) has been combined with a lambda-unification algorithm to assist in the deductions. The resulting prover combines the advantages of the proof-search algorithm of Otter and the power of higher-order unification. Several example theorems are given to illustrate the capabilities of the modified version of Otter, which we call Otter-λ. We also describe the untyped lambda unification algorithm used by Otter-λ.
The demands of real-time commonsense reasoning - as evidenced for example in the pragmatics of human-computer dialog - put stringent requirements on the underlying logic, including those of (i) perturbation tolerance, (ii) contradiction tolerance and (iii) time situatedness. Active logic is an attempt to meet all of these needs. In this paper we present this work and its application to natural language dialog via time-sensitive meta-reasoning. We illustrate this with a description of ALFRED, a cooperative natural language interface to mulitple task-oriented domains.
ETPS is a program which logic students can use to develop formal proofs in first-order logic or higher-order logic interactively. It displays formulas using notations of symbolic logic, and displays proofs in windows which are automatically updated as the proofs are developed. It enables students to concentrate on the essential logical problems involved in proving theorems, and automatically checks the proofs. It was developed in collaboration with Frank Pfenning, Sunil Issar, Hongwei Xi, Matthew Bishop, and Chad E. Brown. It is the interactive component of the TPS automated Theorem Proving System. ETPS and related information can be obtained from http://gtps.math.cmu.edu/tps.html.