Meta-Reasoning
and Its Applications in First-Order
Predicate Logic


Abstract

Automated theorem proving can be used to handle very complex problems such as solving time scheduling problems, computing (nearly) perfect hardware configurations, proving theorems, etc. .

Nevertheless there are still problems which lead to infinite or at least time consuming computations by an automated theorem prover. Many of these can be traced back to sequences structurally similar terms and clauses. In this master thesis we introduce a concept called deductive generalisation which enables an automated theorem prover to cope with sequences structurally similar clauses. Clauses of the form

$T = P \vee Q$ with $Q = \overline{P}\lambda$ for some substitution $\lambda$
are identified as a source for structurally similar clauses while applying the resolution principle. By means of meta-literals we are able to express sequences of structurally similar clauses (in general infinitely many of them); unification is then extended to unify these meta-literals and meta-resolution is used to derive new meta-clauses, which again represent infinite sets of ordinary clauses.

By doing so we can speed up the process of resolution; meta-clauses save space as well as time. Based on the concept of deductive generalisation we will give an implementation of an automated theorem prover, which we will use to prove the completeness of the group axioms (without equality relation).This way we want to demonstrate the usefulness of our approach.

Availability

The automated theorem prover mentioned in the abstract is completely written and tested in Sicstus Prolog v3.6 and its source is available here. If you want to use it with other prolog engines, you only have to modify the file depend.pl to your needs, that should be all which has to be done.

If you are interested in the master thesis, you can find it as postscipt under

and as DVI under I did not have the time to convert the whole master thesis into html, but this should come as soon as possible:)

Feedback

If there are any questions, comments, bugs, ... report them to goth@logic.at . I will do my best to answer your questions as soon as possible.