and Its Applications in First-Order
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
for some substitution
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.
The automated theorem prover
mentioned in the abstract is completely written and tested in Sicstus Prolog v3.6 and its source is
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
If there are any questions, comments, bugs, ... report them to
firstname.lastname@example.org . I will do my best to answer your
questions as soon as possible.