Equational theorem proving modulo

DOI10.1007/978-3-030-79876-5_10MaRDI QIDQ2055853zbMATH OpenOpenAlexFDO

Authors Christopher Lynch, Dohan Kim

Publication date 1 December 2021

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-79876-5_10

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• scientific article; zbMATH DE number 1552532
• Theorem proving modulo associativity
• Theorem proving modulo
• Computer Science Logic
• Equational Theorem Proving for Clauses over Strings

Cites work

• scientific article; zbMATH DE number 1552532 (Why is no real title available?)
• scientific article; zbMATH DE number 7015114 (Why is no real title available?)
• scientific article; zbMATH DE number 3349331 (Why is no real title available?)
• A Machine-Oriented Logic Based on the Resolution Principle
• An RPO-Based Ordering Modulo Permutation Equations and Its Applications to Rewrite Systems
• Associative unification and symbolic reasoning modulo associativity in Maude
• Associative-commutative deduction with constraints
• Automated Reasoning
• Basic paramodulation
• Completion for rewriting modulo a congruence
• Equational theorem proving modulo
• Folding variant narrowing and optimal variant termination
• Paramodulation with built-in AC-theories and symbolic constraints
• Paramodulation with non-monotonic orderings and simplification
• Paramodulation-based theorem proving
• Polarized Resolution Modulo
• Reviving basic narrowing modulo
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Rewriting
• Term Rewriting and All That
• Theorem proving modulo
• Unification theory

Cited in

(13)

• scientific article; zbMATH DE number 1538015 (Why is no real title available?)
• Verification Modulo theories
• scientific article; zbMATH DE number 1765692 (Why is no real title available?)
• Equational theorem proving modulo
• Modular proof systems for partial functions with Evans equality
• Automated Reasoning
• Termination modulo equations by abstract commutation with an application to iteration
• Set of support, demodulation, paramodulation: a historical perspective
• Embedding Deduction Modulo into a Prover
• Learning Modulo Theories
• Equational Theorem Proving for Clauses over Strings
• Positive deduction modulo regular theories
• Theorem proving modulo associativity

This page was built for publication: Equational theorem proving modulo

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