Intellektik: Technical report 92-21
From Horn Clauses to First Order Logic: A Graceful Ascent
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
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.