Equational theorem proving modulo
From MaRDI portal
Publication:2055853
DOI10.1007/978-3-030-79876-5_10OpenAlexW3179244314MaRDI QIDQ2055853
Publication date: 1 December 2021
Full work available at URL: https://doi.org/10.1007/978-3-030-79876-5_10
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (3)
Equational Theorem Proving for Clauses over Strings ⋮ Equational theorem proving modulo ⋮ Set of support, demodulation, paramodulation: a historical perspective
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Paramodulation with non-monotonic orderings and simplification
- Completion for rewriting modulo a congruence
- Paramodulation with built-in AC-theories and symbolic constraints
- Theorem proving modulo
- Basic paramodulation
- Folding variant narrowing and optimal variant termination
- Equational theorem proving modulo
- Reviving basic narrowing modulo
- Polarized Resolution Modulo
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Term Rewriting and All That
- Associative-commutative deduction with constraints
- Automated Reasoning
- 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
This page was built for publication: Equational theorem proving modulo
