Paramodulation with non-monotonic orderings and simplification

DOI10.1007/S10817-011-9244-ZMaRDI QIDQ352977zbMATH OpenOpenAlexFDO

Authors 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

automated theorem provingequational reasoningKnuth-Bendix completionordered paramodulation

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Automated Reasoning
• Paramodulation and Knuth-Bendix completion with nontotal and nonmonotonic orderings
• Simultaneous paramodulation
• Paramodulation with Well-founded Orderings
• On restrictions of ordered paramodulation with simplification

Cites work

• scientific article; zbMATH DE number 1614707 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• scientific article; zbMATH DE number 1487842 (Why is no real title available?)
• scientific article; zbMATH DE number 1552532 (Why is no real title available?)
• scientific article; zbMATH DE number 2090319 (Why is no real title available?)
• Automated Reasoning
• Basic paramodulation
• Equational inference, canonical proofs, and proof orderings
• Orderings for term-rewriting systems
• Paramodulation and Knuth-Bendix completion with nontotal and nonmonotonic orderings
• Paramodulation with Well-founded Orderings
• Paramodulation-based theorem proving
• Proving refutational completeness of theorem-proving strategies
• Proving termination with multiset orderings
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Slothrop: Knuth-Bendix Completion with a Modern Termination Checker
• Term Rewriting and All That
• Termination of term rewriting using dependency pairs
• Termination tools in ordered completion
• Theorem proving with ordering and equality constrained clauses

Cited in

(9)

• Paramodulation and Knuth-Bendix completion with nontotal and nonmonotonic orderings
• Basic paramodulation
• Equational theorem proving modulo
• scientific article; zbMATH DE number 7350767 (Why is no real title available?)
• scientific article; zbMATH DE number 1341621 (Why is no real title available?)
• Automated Reasoning
• Paramodulation with Well-founded Orderings
• \( \alpha \)-paramodulation method for a lattice-valued logic \(L_nF(X)\) with equality
• A Lambda-Free Higher-Order Recursive Path Order

Describes a project that uses

Uses Software

• Slothrop

This page was built for publication: Paramodulation with non-monotonic orderings and simplification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q352977)