The following pages link to Basic paramodulation (Q1899908):
Displayed 25 items.
- Paramodulation with non-monotonic orderings and simplification (Q352977) (← links)
- Lazy narrowing: strong completeness and eager variable elimination (Q671677) (← links)
- Superposition-based equality handling for analytic tableaux (Q877891) (← links)
- Deciding expressive description logics in the framework of resolution (Q924723) (← links)
- Connection tableaux with lazy paramodulation (Q928656) (← links)
- A resolution-based decision procedure for \({\mathcal{SHOIQ}}\). (Q928657) (← links)
- Superposition theorem proving for abelian groups represented as integer modules (Q1275020) (← links)
- Decidability and complexity analysis by basic paramodulation (Q1281494) (← links)
- Theorem proving modulo (Q1431339) (← links)
- Superposition with completely built-in abelian groups (Q1432887) (← links)
- ELAN from a rewriting logic point of view (Q1608914) (← links)
- Induction = I-axiomatization + first-order consistency. (Q1854350) (← links)
- Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes) (Q2051565) (← links)
- Equational theorem proving modulo (Q2055853) (← links)
- Ground joinability and connectedness in the superposition calculus (Q2104507) (← links)
- AC simplifications and closure redundancies in the superposition calculus (Q2142076) (← links)
- \( \alpha \)-paramodulation method for a lattice-valued logic \(L_nF(X)\) with equality (Q2156971) (← links)
- Model completeness, covers and superposition (Q2305411) (← links)
- Tree automata with equality constraints modulo equational theories (Q2426520) (← links)
- Reasoning in description logics by a reduction to disjunctive datalog (Q2462648) (← links)
- Superposition with equivalence reasoning and delayed clause normal form transformation (Q2486577) (← links)
- Translation of resolution proofs into short first-order proofs without choice axioms (Q2486578) (← links)
- Encoding Monomorphic and Polymorphic Types (Q2974796) (← links)
- Harald Ganzinger’s Legacy: Contributions to Logics and Programming (Q4916069) (← links)
- What you always wanted to know about rigid E-unification (Q5235253) (← links)