The following pages link to (Q2751354):
Displaying 24 items.
- Semantics and proof-theory of depth bounded Boolean logics (Q385021) (← links)
- Linearity and regularity with negation normal form (Q703486) (← links)
- A sound framework for \(\delta\)-rule variants in free-variable semantic tableaux (Q877883) (← links)
- Superposition-based equality handling for analytic tableaux (Q877891) (← links)
- Liberalized variable splitting (Q877894) (← links)
- Optimization techniques for propositional intuitionistic logic and their implementation (Q959821) (← links)
- The problem of \(\Pi_{2}\)-cut-introduction (Q1680562) (← links)
- A navigational logic for reasoning about graph properties (Q1996850) (← links)
- Machine learning guidance for connection tableaux (Q2031418) (← links)
- Learning from Łukasiewicz and Meredith: investigations into proof structures (Q2055843) (← links)
- Set of support, demodulation, paramodulation: a historical perspective (Q2102923) (← links)
- Constraint tableaux for two-dimensional fuzzy logics (Q2142061) (← links)
- Soundness and completeness proofs by coinductive methods (Q2362498) (← links)
- ABox abduction in the description logic \(\mathcal{ALC}\) (Q2429984) (← links)
- Towards a unified model of search in theorem-proving: subgoal-reduction strategies (Q2456542) (← links)
- Reasoning on UML class diagrams (Q2457652) (← links)
- Craig interpolation with clausal first-order tableaux (Q2666953) (← links)
- nanoCoP: A Non-clausal Connection Prover (Q2817929) (← links)
- Encoding First Order Proofs in SMT (Q2864408) (← links)
- A Non-clausal Connection Calculus (Q3010371) (← links)
- (Q4524785) (← links)
- Programming and verifying a declarative first-order prover in Isabelle/HOL (Q5145439) (← links)
- Range-restricted and Horn interpolation through clausal tableaux (Q6541142) (← links)
- Lemmas: generation, selection, application (Q6541149) (← links)
