The following pages link to (Q5624683):
Displaying 50 items.
- On deciding satisfiability by theorem proving with speculative inferences (Q438533) (← links)
- Proof-guided test selection from first-order specifications with equality (Q616851) (← links)
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (Q682374) (← links)
- Using forcing to prove completeness of resolution and paramodulation (Q757093) (← links)
- Theorem-proving with resolution and superposition (Q757094) (← links)
- On word problems in Horn theories (Q757095) (← links)
- A new use of an automated reasoning assistant: Open questions in equivalential calculus an the study of infinite domains (Q759491) (← links)
- Steps toward a computational metaphysics (Q877243) (← links)
- Superposition-based equality handling for analytic tableaux (Q877891) (← links)
- A superposition oriented theorem prover (Q1060857) (← links)
- Incorporating equality into logic programming via surface deduction (Q1087023) (← links)
- History and basic features of the critical-pair/completion procedure (Q1103414) (← links)
- An order-sorted logic for knowledge representation systems (Q1193487) (← links)
- An improved general \(E\)-unification method (Q1201347) (← links)
- A unification algorithm for typed \(\bar\lambda\)-calculus (Q1227601) (← links)
- A unification algorithm for typed \(\overline\lambda\)-calculus (Q1230505) (← links)
- Non-resolution theorem proving (Q1238434) (← links)
- Mechanizing \(\omega\)-order type theory through unification (Q1239309) (← links)
- Paramodulated connection graphs (Q1257912) (← links)
- Local simplification (Q1271570) (← links)
- The problem of naming and function replacement (Q1311398) (← links)
- The kernel strategy and its use for the study of combinatory logic (Q1311399) (← links)
- Completeness issues in RUE-NRF deduction: The undecidability of viability (Q1311402) (← links)
- Deductive and inductive synthesis of equational programs (Q1322836) (← links)
- A resolution principle for constrained logics (Q1327159) (← links)
- Hybrid reasoning using universal attachment (Q1329365) (← links)
- Basic research problems: The problem of strategy and hyperresolution (Q1332645) (← links)
- The problem of hyperparamodulation (Q1337565) (← links)
- Automated deduction with associative-commutative operators (Q1340508) (← links)
- The application of automated reasoning to questions in mathematics and logic (Q1354049) (← links)
- On Skolemization in constrained logics (Q1380406) (← links)
- Presenting inequations in mathematical proofs (Q1818758) (← links)
- Complete sets of unifiers and matchers in equational theories (Q1820760) (← links)
- The problem of guaranteeing the existence of a complete set of reductions (Q1823015) (← links)
- Horn equational theories and paramodulation (Q1824409) (← links)
- Basic narrowing revisited (Q1824412) (← links)
- The application of automated reasoning to formal models of combinatorial optimization (Q1854978) (← links)
- The anatomy of vampire. Implementing bottom-up procedures with code trees (Q1904404) (← links)
- Induction using term orders (Q1915132) (← links)
- Linear and unit-resulting refutations for Horn theories (Q1923821) (← links)
- Reasoning with conditional axioms (Q1924731) (← links)
- Equational theorem proving modulo (Q2055853) (← links)
- Neural precedence recommender (Q2055885) (← links)
- Larry Wos: visions of automated reasoning (Q2102922) (← links)
- Set of support, demodulation, paramodulation: a historical perspective (Q2102923) (← links)
- SCL(EQ): SCL for first-order logic with equality (Q2104511) (← links)
- \( \alpha \)-paramodulation method for a lattice-valued logic \(L_nF(X)\) with equality (Q2156971) (← links)
- Renamable paramodulation for automatic theorem proving with equality (Q2542996) (← links)
- The unit-clause proof procedure with equality (Q2547127) (← links)
- Splitting and reduction heuristics in automatic theorem proving (Q2547495) (← links)
