Previous: TR 92-20 Next: TR 92-24

Intellektik: Technical report 92-21

From Horn Clauses to First Order Logic: A Graceful Ascent

G. Neugebauer

Prolog technology provides a good basis for automated theorem proving. Nevertheless Prolog itself uses only Horn clauses. Full predicate logic requires just a small addition to be complete. This addition is the reduction step known from model elimination and connection method theorem proving.

This paper presents an uniform method to translate arbitrary formulae in normal form into Prolog. Special care is taken to avoid overhead in the case of Horn formulae as input. A criterion is developed to determine superfluous procedures (contrapositives). As a consequence the translation of predicate logic into Prolog can be improved.

Full Paper: Compressed postscript Compressed DVI

BibTeX entry