Paramodulation with non-monotonic orderings and simplification

DOI10.1007/s10817-011-9244-zzbMath1315.03017OpenAlexW2041375296MaRDI QIDQ352977

Miquel Bofill, Albert Rubio

Publication date: 5 July 2013

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

Full work available at URL: https://doi.org/10.1007/s10817-011-9244-z

zbMATH Keywords

equational reasoningautomated theorem provingKnuth-Bendix completionordered paramodulation

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

\( \alpha \)-paramodulation method for a lattice-valued logic \(L_nF(X)\) with equality, Unnamed Item, A Lambda-Free Higher-Order Recursive Path Order, Equational theorem proving modulo

Uses Software

• Slothrop

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Orderings for term-rewriting systems
• Paramodulation and Knuth-Bendix completion with nontotal and nonmonotonic orderings
• Theorem proving with ordering and equality constrained clauses
• Basic paramodulation
• Termination of term rewriting using dependency pairs
• Slothrop: Knuth-Bendix Completion with a Modern Termination Checker
• Paramodulation with Well-founded Orderings
• Proving termination with multiset orderings
• Equational inference, canonical proofs, and proof orderings
• Proving refutational completeness of theorem-proving strategies
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Term Rewriting and All That
• Automated Reasoning
• Termination Tools in Ordered Completion