Automatic theorem proving. I

Cybernetics and Systems Analysis -     

Automatic theorem proving in set theory

This paper describes a program which proves theorems in set theory by the use of heuristics. The use of methods which are analogous to human methods is its main characteristics. By splitting, a different theorem is first brokes into more easily proud parts. The heuristics for the following steps, which are the resuse of observation and imitation of the mathematics' methods, emphasize the use of many selections methods and the choice of suitable representations. In particular, a graph is constructed to represent binary relations. The program has been used to prove about 150 theorems in more and axiomatic set theory, sampling with functions, orderings, congruence relations and ordinal numbers.     

Refutational theorem proving using term-rewriting systems

In this paper we propose a new approach to theorem proving in first-order logic based on the term-rewriting method. First for propositional calculus, we introduce a canonical term-rewriting system for Boolean algebra. This system enables us to transform the first-order predicate calculus into a form of equational logic, and to develop several complete strategies (both clausal and nonclausal) for first-order theories based on the Knuth-Bendix Completion Procedure. More importantly, our strategies can deal with predicate logic and built-in (equational) theories in a uniform and effective way. We also describe an implementation and comparisons with some other first-order theorem-proving methods.     

Plane geometry theorem proving using forward chaining

A computer program is described which operates on a subset of plane geometry. Its performance not only compares favorably with previous computer programs, but within its limited problem domain (e.g., no curved lines nor introduction of new points), it also invites comparison with the best human theorem provers. The program employs a combination of forward and backward chaining with the forward component playing the more important role. This, together with a deeper use of diagrammatic information, allows the program to dispense with the diagram filter in contrast with its central role in previous programs. An important aspect of human problem solving may be the ability to structure a problem space so that forward chaining techniques can be used effectively.     

Completely non-clausal theorem proving

The proof procedure we describe operates on quantifier-free formulas of the predicate calculus which are not truth-functionally normalized in any way. The procedure involves a single inference rule called NC-resolution, and is shown to be complete. Completeness is also obtained for a simple restriction on the rule's application.Examples are given using NC-resolution to derive a logic program from its specification, and to ‘execute’ a program specification in its original form.     

A prolog technology theorem prover: Implementation by an extended prolog compiler

A Prolog technology theorem prover (PTTP) is an extension of Prolog that is complete for the full first-order predicate calculus. It differs from Prolog in its use of unification with the occurs check for soundness, the model-elimination reduction rule that is added to Prolog inferences to make the inference system complete, and depth-first iterative-deepening search instead of unbounded depthfirst search to make the search strategy complete. A Prolog technology theorem prover has been implemented by an extended Prolog-to-LISP compiler that supports these additional features. It is capable of proving theorems in the full first-order predicate calculus at a rate of thousands of inferences per second.This is a revised and expanded version of a paper presented at the 8th International Conference on Automated Deduction, Oxford, England, July 1986.This research was supported by the Defense Advanced Research Projects Agency under Contract N00039-84-K-0078 with the Naval Electronic Systems Command and by the National Science Foundation under Grant CCR-8611116. The views and conclusions contained herein are those of the author and should not be interpreted as necessarily representing the official policies, either expressed or implied, of the Defense Advanced Research Projects Agency, the National Science Foundation, or the United States government. Approved for public release. Distribution unlimited.     

An approach for lifetime reliability analysis using theorem proving

Recently proposed formal reliability analysis techniques have overcome the inaccuracies of traditional simulation based techniques but can only handle problems involving discrete random variables. In this paper, we extend the capabilities of existing theorem proving based reliability analysis by formalizing several important statistical properties of continuous random variables like the second moment and the variance. We also formalize commonly used concepts about the reliability theory such as survival, hazard, cumulative hazard and fractile functions. With these extensions, it is now possible to formally reason about important measures of reliability (the probabilities of failure, the failure risks and the mean-time-to failure) associated with the life of a system that operates in an uncertain and harsh environment and is usually continuous in nature. We illustrate the modeling and verification process with the help of examples involving the reliability analysis of essential electronic and electrical system components.     

An autonomous multistrategy theorem proving system using knowledge-based techniques

Most general-purpose theorem-proving systems have weak search control. There is no alternative to the use of a large number of heuristics or strategies for search guidance. Choosing appropriate strategies for solving a given problem may require the knowledge of different strategies and may involve a lot of painstaking trial-and-error. To encourage the widespread use of computer reasoning systems, it is important that a theorem prover be usable by those with little knowledge of problem-solving strategies, and that a theorem prover be able to select good strategies for the user. An autonomous multistrategy theorem-proving system is developed, using knowledge-based techniques, to entirely free the user from the necessity of understanding the system or the merits of different strategies. All the user has to do is input his or her problem in first-order logic, and the system solves the problem efficiently for him or her without any manual intervention. The system embodies much of expert knowledge about how to solve problems. The knowledge is represented as metarules in knowledge base which guide a hyperlinking theorem prover to solve problems automatically and efficiently.     

Composition of Semantic Web services using Linear Logic theorem proving

This paper introduces a method for automatic composition of Semantic Web services using Linear Logic (LL) theorem proving. The method uses a Semantic Web service language (DAML-S) for external presentation of Web services, while, internally, the services are presented by extralogical axioms and proofs in LL. LL, as a resource conscious logic, enables us to capture the concurrent features of Web services formally (including parameters, states and non-functional attributes). We use a process calculus to present the process model of the composite service. The process calculus is attached to the LL inference rules in the style of type theory. Thus, the process model for a composite service can be generated directly from the complete proof. We introduce a set of subtyping rules that defines a valid dataflow for composite services. The subtyping rules that are used for semantic reasoning are presented with LL inference figures. We propose a system architecture where the DAML-S Translator, LL Theorem Prover and Semantic Reasoner can operate together. This architecture has been implemented in Java.     

Analytic resolution in theorem proving

Analytic resolution is a proof procedure for predicate calculus based on the ideas of semantic trees and analytic tableaux. It is related to the unit preference with set-of-support strategy, and incorporates some features of model elimination. The philosophy is to expect and compensate for “blind alleys” by a stack discipline. This eliminates pollution of the search space by a bad choice of the next step in a proof. Experimental results included compare favourably with others from the literature.     

Automated theorem proving in mathematics

TheMuscadet theorem prover is a knowledge-based system able to prove theorems in some non-trivial mathematical domains. The knowledge bases contain some general deduction strategies based onnatural deduction, mathematical knowledge and metaknowledge. Metarules build new rules, easily usable by the inference engine, from formal definitions. Mathematical knowledge may be general or specific to some particular field.Muscadet proved many theorems in set theory, mappings, relations, topology, geometry, and topological linear spaces. Some of the theorems were rather difficult.Muscadet is now intended to become an assistant for mathematicians in discrete geometry for cellular automata. In order to evaluate the difficulty of such a work, researchers were observed while proving some lemmas, andMuscadet was tested on easy ones. New methods have to be added to the knowledge base, such as reasoning by induction, but also new heuristics for splitting and reasoning by cases. It is also necessary to find good representations for some mathematical objects.     

Parallel cooperative propositional theorem proving

A parallel satisfiability testing algorithm called Parallel Modoc is presented. Parallel Modoc is based on Modoc, which is based on propositional Model Elimination with an added capability to prune away certain branches that cannot lead to a successful subrefutation. The pruning information is encoded in a partial truth assignment called an autarky. Parallel Modoc executes multiple instances of Modoc as separate processes and allows processes to cooperate by sharing lemmas and autarkies as they are found. When a Modoc process finds a new autarky or a new lemma, it makes the information available to other Modoc processes via a “blackboard”. Combining autarkies generally is not straightforward because two autarkies found by two separate processes may have conflicting assignments. The paper presents an algorithm to combine two arbitrary autarkies to form a larger autarky. Experimental results show that for many of the formulas, Parallel Modoc achieves speedup greater than the number of processors. Formulas that could not be solved in an hour by Modoc were often solved by Parallel Modoc in the order of minutes and, in some cases, in seconds. This revised version was published online in June 2006 with corrections to the Cover Date.     

Mechanical theorem proving in projective geometry

We present an algorithm that is able to confirm projective incidence statements by carrying out calculations in the ring of all formal determinants (brackets) of a configuration. We will describe an implementation of this prover and present a series of examples treated by the prover, includingPappus' andDesargues' theorems, thesixteen point theorem, Saam's theorem, thebundle condition, theuniqueness of a harmonic point andPascal's theorem.     

Bounded-overhead caching for definite-clause theorem proving

In this paper we describe the design of an effective caching mechanism for resource-limited, definite-clause theorem-proving systems. Previous work in adapting caches for theorem proving relies on the use of unlimited-size caches. We show how unlimited-size caches are unsuitable in application contexts where resource-limited theorem provers are used to solve multiple problems from a single problem distribution. We introduce bounded-overhead caches, that is, those caches that contain at most a fixed number of entries and entail a fixed amount of overhead per lookup, and we examine cache design issues for bounded-overhead caches. Finally, we present an empirical evaluation of bounded-overhead cache performance, relying on a specially designed experimental methodology that separates hardware-dependent, implementation-dependent, and domain-dependent effects.     

Hybridizing nonmonotonic inheritance with theorem proving

Theorem proving techniques and inheritance are often thought of as quite different reasoning styles. This paper concentrates on similarities between the two. It suggests a criterion for when an inheritance consequence relation can be integrated coherently with a stronger logical consequence relation, and develops in some detail one way in which a nonmonotonic inheritance network could be integrated with a Gentzen-style theorem prover for the Boolean connectives.