Pages that link to "Item:Q1344875"
From MaRDI portal
The following pages link to Controlled integration of the cut rule into connection tableau calculi (Q1344875):
Displaying 36 items.
- The disconnection tableau calculus (Q877889) (← links)
- Prolog technology for default reasoning: proof theory and compilation techniques (Q1275596) (← links)
- Controlled integration of the cut rule into connection tableau calculi (Q1344875) (← links)
- Clause trees: A tool for understanding and implementing resolution in automated reasoning (Q1402732) (← links)
- Computing answers with model elimination (Q1402748) (← links)
- IeanCOP: lean connection-based theorem proving (Q1404981) (← links)
- The proof complexity of analytic and clausal tableaux (Q1575658) (← links)
- Practically useful variants of definitional translations to normal form (Q1854384) (← links)
- Linear and unit-resulting refutations for Horn theories (Q1923821) (← links)
- Resolution remains hard under equivalence (Q1961451) (← links)
- Complexity analysis of propositional resolution with autarky pruning (Q1961454) (← links)
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search (Q2142075) (← links)
- The model evolution calculus as a first-order DPLL method (Q2389629) (← links)
- Towards a unified model of search in theorem-proving: subgoal-reduction strategies (Q2456542) (← links)
- Another look at graph coloring via propositional satisfiability (Q2467359) (← links)
- Craig interpolation with clausal first-order tableaux (Q2666953) (← links)
- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions) (Q3541708) (← links)
- MGTP: A model generation theorem prover — Its advanced features and applications — (Q4610311) (← links)
- Non-elementary speed-ups in proof length by different variants of classical analytic calculi (Q4610324) (← links)
- Subgoal alternation in model elimination (Q4610327) (← links)
- A framework for using knowledge in tableau proofs (Q4610337) (← links)
- The disconnection method (Q4645231) (← links)
- Minimal model generation with positive unit hyper-resolution tableaux (Q4645233) (← links)
- Situational Calculus, linear connection proofs and STRIPS-like planning: An experimental comparison (Q4645236) (← links)
- The tableau-based theorem prover 3 T A P Version 4.0 (Q4647529) (← links)
- Optimizing proof search in model elimination (Q4647531) (← links)
- On the practical value of different definitional translations to normal form (Q4647537) (← links)
- From Schütte’s Formal Systems to Modern Automated Deduction (Q5013905) (← links)
- Model elimination without contrapositives (Q5210764) (← links)
- ILF-SETHEO (Q5234690) (← links)
- Automatic verification of cryptographic protocols with SETHEO (Q5234693) (← links)
- Lemma matching for a PTTP-based top-down theorem prover (Q5234698) (← links)
- Hyper tableaux (Q5235250) (← links)
- Controlled use of clausal lemmas in connection tableau calculi (Q5927985) (← links)
- Lemmas: generation, selection, application (Q6541149) (← links)
- Investigations into proof structures (Q6653096) (← links)
