Paramodulation and Knuth-Bendix completion with nontotal and nonmonotonic orderings

DOI10.1023/A:1022515030222zbMath1027.03010MaRDI QIDQ1810859

Robert Nieuwenhuis, Albert Rubio, Guillem Godoy, Miquel Bofill

Publication date: 9 June 2003

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

zbMATH Keywords

term rewritingautomated deduction

Mathematics Subject Classification ID

Related Items (3)

Paramodulation with non-monotonic orderings and simplification ⋮ Termination Tools in Ordered Completion ⋮ A Knuth-Bendix-like ordering for orienting combinator equations

This page was built for publication: Paramodulation and Knuth-Bendix completion with nontotal and nonmonotonic orderings