A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering.

Konstantin Korovin Andrei Voronkov

Published in: LICS (2000)

Keyphrases

knuth bendix
term rewriting
rewrite systems
function symbols
theorem proving
knowledge base
temporal reasoning