Pages that link to "Item:Q5544307"

The following pages link to Mechanical Theorem-Proving by Model Elimination (Q5544307):

Displaying 35 items.

• An annotated logic theorem prover for an extended possibilistic logic (Q598578) (← links)
• The undecidability of simultaneous rigid E-unification (Q671659) (← links)
• A relevance restriction strategy for automated deduction (Q814429) (← links)
• Filter-based resolution principle for lattice-valued propositional logic LP\((X)\) (Q867665) (← links)
• Automated inferencing (Q1070835) (← links)
• Completeness results for inequality provers (Q1079960) (← links)
• Hierarchical deduction (Q1098332) (← links)
• An extension to linear resolution with selection function (Q1160497) (← links)
• Refutation graphs (Q1226867) (← links)
• Local simplification (Q1271570) (← 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)
• Decidability and complexity of simultaneous rigid E-unification with one variable and related results (Q1575636) (← links)
• The proof complexity of analytic and clausal tableaux (Q1575658) (← links)
• The linked conjunct method for automatic deduction and related search techniques (Q1836998) (← links)
• A typed resolution principle for deduction with conditional typing theory (Q1855225) (← links)
• Linear and unit-resulting refutations for Horn theories (Q1923821) (← links)
• Near-Horn Prolog and the ancestry family of procedures (Q1924724) (← links)
• Machine learning guidance for connection tableaux (Q2031418) (← links)
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) (Q2351415) (← links)
• Theorem proving with variable-constrained resolution (Q2554609) (← links)
• A Non-clausal Connection Calculus (Q3010371) (← links)
• HOL Light: An Overview (Q3183517) (← links)
• leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions) (Q3541708) (← links)
• Ordered tableaux: Extensions and applications (Q4610325) (← links)
• Optimizing proof search in model elimination (Q4647531) (← links)
• From Schütte’s Formal Systems to Modern Automated Deduction (Q5013905) (← links)
• Model elimination without contrapositives (Q5210764) (← links)
• Detecting non-provable goals (Q5210774) (← links)
• What you always wanted to know about rigid E-unification (Q5235253) (← links)
• Controlled use of clausal lemmas in connection tableau calculi (Q5927985) (← links)
• Simultaneous rigid E-unification is undecidable (Q6560168) (← links)