Equational theorem proving modulo

DOI10.1007/978-3-030-79876-5_10OpenAlexW3179244314MaRDI QIDQ2055853FDOQ2055853

Authors: Christopher Lynch, Dohan Kim 

Publication date: 1 December 2021

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)

Cites Work

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

Cited In (11)

• Title not available (Why is that?)
• Set of support, demodulation, paramodulation: a historical perspective
• Equational theorem proving modulo
• Termination modulo equations by abstract commutation with an application to iteration
• Embedding Deduction Modulo into a Prover
• Learning Modulo Theories
• Verification Modulo theories
• Automated Reasoning
• Title not available (Why is that?)
• Modular proof systems for partial functions with Evans equality
• Equational Theorem Proving for Clauses over Strings

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)