Complete Equational Unification Based on an Extension of the Knuth-Bendix Completion Procedure.

Akihiko Ohsuga Kô Sakai

Published in: IWWERT (1990)

Keyphrases

knuth bendix
term rewriting
theorem proving
function symbols
theorem prover
rewrite systems
equational theories
first order logic
logic programs
horn clauses
operational semantics
databases
inference rules
information systems
np complete
automated reasoning