On solving the equality problem in theories defined by Horn clauses (Q1085152)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | On solving the equality problem in theories defined by Horn clauses |
scientific article |
Statements
On solving the equality problem in theories defined by Horn clauses (English)
0 references
1986
0 references
The Knuth-Bendix completion procedure for solving the equality problem in equational theories is adapted to nonequational theories defined by sets of Horn clauses. Completeness can be achieved by endowing the procedure with a weak axiomatization of Boolean calculus and the reflexivity axiom for equality. It is shown that the procedure can also be used for inductive proofs, i.e., for proving universally quantified formulas in the initial model defined by a set of Horn clauses. The relationships to some resolution and paramodulation methods are discussed, and experimental results are appended.
0 references
Knuth-Bendix completion procedure
0 references
equality problem
0 references
nonequational theories
0 references
Horn clauses
0 references