The Existential Theories of Term Algebras with the Knuth-Bendix Orderings are Decidable.

Konstantin Korovin Andrei Voronkov

Published in: ARW (2000)

Keyphrases

knuth bendix
function symbols
term rewriting
logic programs
existentially quantified
first order logic
logic programming
rewrite systems
normal form
answer set programming
theorem prover
artificial intelligence
knowledge base
sat solvers
theorem proving
reasoning tasks