In this report we give an overview of the development of our new Waldmeisterprover for equational theories. We elaborate a systematic stepwise design process, startingwith the inference system for unfailing Knuth - Bendix completion and ending up with animplementation which avoids the main diseases today's provers suffer from: overindulgencein time and space.Our design process is based on a logical three - level system model consisting of basicoperations for inference step execution, aggregated inference machine, and overall controlstrategy. Careful analysis of the inference system for unfailing completion has revealed thecrucial points responsible for time and space consumption. For the low level of our model,we introduce specialized data structures and algorithms speeding up the running system andcutting it down in size - both by one order of magnitude compared with standard techniques.Flexible control of the mid - level aggregation inside the resulting prover is made possible by acorresponding set of parameters. Experimental analysis shows that this flexibility is a pointof high importance. We go on with some implementation guidelines we have found valuablein the field of deduction.The resulting new prover shows that our design approach is promising. We compare oursystem's throughput with that of an established system and finally demonstrate how twovery hard problems could be solved by Waldmeister.
We show how to prove ground confluence of term rewrite relations that areinduced by reductive systems of clausal rewrite rules. According to a well-knowncritical pair criterion it suffices for such systems to prove ground joinability ofa suitable set of 'critical clauses'. We outline how the latter can be done in asystematic fashion, using mathematical induction as a key concept of reasoning.
In recent years several computational systems and techniques fortheorem proving by analogy have been developed. The obvious prac-tical question, however, as to whether and when to use analogy hasbeen neglected badly in these developments. This paper addresses thisquestion, identifies situations where analogy is useful, and discussesthe merits of theorem proving by analogy in these situations. Theresults can be generalized to other domains.
We present a way to describe Reason Maintenance Systems using the sameformalism for justification based as well as for assumption based approaches.This formalism uses labelled formulae and thus is a special case of Gabbay'slabelled deductive systems. Since our approach is logic based, we are able toget a semantics oriented description of the systems in question.Instead of restricting ourselves to e.g. propositional Horn formulae, as wasdone in the past, we admit arbitrary logics. This enables us to characterizesystems as a whole, including both the reason maintenance component and theproblem solver, nevertheless maintaining a separation between the basic logicand the part that describes the label propagation. The possibility to freely varythe basic logic enables us to not only describe various existing systems, but canhelp in the design of completely new ones.We also show, that it is possible to implement systems based directly on ourlabelled logic and plead for "incremental calculi" crafted to attack undecidablelogics.Furthermore it is shown that the same approach can be used to handledefault reasoning, if the propositional labels are upgraded to first order.
A lot of the human ability to prove hard mathematical theorems can be ascribedto a problem-specific problem solving know-how. Such knowledge is intrinsicallyincomplete. In order to prove related problems human mathematicians, however,can go beyond the acquired knowledge by adapting their know-how to new relatedproblems. These two aspects, having rich experience and extending it by need, can besimulated in a proof planning framework: the problem-specific reasoning knowledge isrepresented in form of declarative planning operators, called methods; since these aredeclarative, they can be mechanically adapted to new situations by so-called meta-methods. In this contribution we apply this framework to two prominent proofs intheorem proving, first, we present methods for proving the ground completeness ofbinary resolution, which essentially correspond to key lemmata, and then, we showhow these methods can be reused for the proof of the ground completeness of lockresolution.
Mechanised reasoning systems and computer algebra systems have apparentlydifferent objectives. Their integration is, however, highly desirable, since in manyformal proofs both of the two different tasks, proving and calculating, have to beperformed. Even more importantly, proof and computation are often interwoven andnot easily separable. In the context of producing reliable proofs, the question howto ensure correctness when integrating a computer algebra system into a mechanisedreasoning system is crucial. In this contribution, we discuss the correctness prob-lems that arise from such an integration and advocate an approach in which thecalculations of the computer algebra system are checked at the calculus level of themechanised reasoning system. This can be achieved by adding a verbose mode to thecomputer algebra system which produces high-level protocol information that can beprocessed by an interface to derive proof plans. Such a proof plan in turn can beexpanded to proofs at different levels of abstraction, so the approach is well-suited forproducing a high-level verbalised explication as well as for a low-level machine check-able calculus-level proof. We present an implementation of our ideas and exemplifythem using an automatically solved extended example.
We present first steps towards fully automated deduction that merely requiresthe user to submit proof problems and pick up results. Essentially, this necessi-tates the automation of the crucial step in the use of a deduction system, namelychoosing and configuring an appropriate search-guiding heuristic. Furthermore,we motivate why learning capabilities are pivotal for satisfactory performance.The infrastructure for automating both the selection of a heuristic and integra-tion of learning are provided in form of an environment embedding the "core"deduction system.We have conducted a case study in connection with a deduction system basedon condensed detachment. Our experiments with a fully automated deductionsystem 'AutoCoDe' have produced remarkable results. We substantiate Au-toCoDe's encouraging achievements with a comparison with the renowned the-orem prover Otter. AutoCoDe outperforms Otter even when assuming veryfavorable conditions for Otter.
One of the many abilities that distinguish a mathematician from an auto-mated deduction system is to be able to offer appropriate expressions based onintuition and experience that are substituted for existentially quantified variablesso as to simplify the problem at hand substantially. We propose to simulate thisability with a technique called genetic programming for use in automated deduc-tion. We apply this approach to problems of combinatory logic. Our experimen-tal results show that the approach is viable and actually produces very promisingresults. A comparison with the renowned theorem prover Otter underlines theachievements.This work was supported by the Deutsche Forschungsgemeinschaft (DFG).
We present a concept for an automated theorem prover that employs a searchcontrol based on ideas from several areas of artificial intelligence (AI). The combi-nation of case-based reasoning, several similarity concepts, a cooperation conceptof distributed AI and reactive planning enables a system using our concept tolearn form previous successful proof attempts. In a kind of bootstrapping processeasy problems are used to solve more and more complicated ones.We provide case studies from two domains of interest in pure equationaltheorem proving taken from the TPTP library. These case studies show thatan instantiation of our architecture achieves a high grade of automation andoutperforms state-of-the-art conventional theorem provers.
We propose a specification language for the formalization of data types with par-tial or non-terminating operations as part of a rewrite-based logical frameworkfor inductive theorem proving. The language requires constructors for designat-ing data items and admits positive/negative conditional equations as axioms inspecifications. The (total algebra) semantics for such specifications is based onso-called data models. We present admissibility conditions that guarantee theunique existence of a distinguished data model with properties similar to thoseof the initial model of a usual equational specification. Since admissibility of aspecification requires confluence of the induced rewrite relation, we provide aneffectively testable confluence criterion which does not presuppose termination.