Pages that link to "Item:Q1344875"

The following pages link to Controlled integration of the cut rule into connection tableau calculi (Q1344875):

Displaying 20 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)
• 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)