What you always wanted to know about rigid E-unification
From MaRDI portal
Publication:5235253
DOI10.1007/3-540-61630-6_4zbMath1427.03032OpenAlexW1530817558MaRDI QIDQ5235253
Andrei Voronkov, Anatoli Degtyarev
Publication date: 8 October 2019
Published in: Logics in Artificial Intelligence (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/3-540-61630-6_4
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Uses Software
Cites Work
- The undecidability of simultaneous rigid E-unification
- Simple LPO constraint solving methods
- Rigid E-unification: NP-completeness and applications to equational matings
- Gentzen-type systems, resolution and tableaux
- Consolution as a framework for comparing calculi
- What you always wanted to know about rigid \(E\)-unification
- Theorem proving with ordering and equality constrained clauses
- Basic paramodulation
- Special cases and substitutes for rigid \(E\)-unification
- Theorem proving with variable-constrained resolution
- An improved proof procedure1
- Theorem Proving via General Matings
- On Matrices with Connections
- Proving Theorems with the Modification Method
- An algorithm for reasoning about equality
- Theorem proving using equational matings and rigid E -unification
- Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-unification
- A completion-based method for mixed universal and rigid E-unification
- Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture
- Mechanical Theorem-Proving by Model Elimination
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: What you always wanted to know about rigid E-unification
