The following pages link to (Q3997615):
Displaying 27 items.
- Invariant-free clausal temporal resolution (Q352974) (← links)
- CERES: An analysis of Fürstenberg's proof of the infinity of primes (Q944367) (← links)
- A solver for QBFs in negation normal form (Q1020501) (← links)
- A new methodology for developing deduction methods (Q1037405) (← links)
- An answer to an open problem of Urquhart (Q1129262) (← links)
- Prolog technology for default reasoning: proof theory and compilation techniques (Q1275596) (← links)
- On the modelling of search in theorem proving -- towards a theory of strategy analysis (Q1281504) (← links)
- On the relative merits of path dissolution and the method of analytic tableaux (Q1331929) (← links)
- Accelerating tableaux proofs using compact representations (Q1334905) (← links)
- On resolution with short clauses (Q1380411) (← links)
- Practically useful variants of definitional translations to normal form (Q1854384) (← links)
- A new methodology for query answering in default logics via structure-oriented theorem proving (Q1896370) (← links)
- Generalizing theorems in real closed fields (Q1899140) (← links)
- lean\(T^ AP\): Lean tableau-based deduction (Q1904400) (← links)
- Learning from Łukasiewicz and Meredith: investigations into proof structures (Q2055843) (← links)
- Andrews Skolemization may shorten resolution proofs non-elementarily (Q2151391) (← links)
- Towards a unified model of search in theorem-proving: subgoal-reduction strategies (Q2456542) (← links)
- On Stronger Calculi for QBFs (Q2818031) (← links)
- Lean induction principles for tableaux (Q4610315) (← links)
- Non-elementary speed-ups in proof length by different variants of classical analytic calculi (Q4610324) (← links)
- On the practical value of different definitional translations to normal form (Q4647537) (← links)
- Analytic tableaux for default logics (Q4868235) (← links)
- The search efficiency of theorem proving strategies (Q5210762) (← links)
- Model elimination without contrapositives (Q5210764) (← links)
- KoMeT (Q5210812) (← links)
- LeanT A P: Lean tableau-based theorem proving (Q5210813) (← links)
- Some pitfalls of LK-to-LJ translations and how to avoid them (Q5234695) (← links)
