The following pages link to (Q4692618):
Displaying 50 items.
- Incremental variable splitting (Q429591) (← links)
- Theory matrices (for modal logics) using alphabetical monotonicity (Q687154) (← links)
- Parsing as non-Horn deduction (Q688151) (← links)
- Hypothesis finding with proof theoretical appropriateness criteria (Q817840) (← links)
- TPS: A hybrid automatic-interactive system for developing proofs (Q865629) (← links)
- The disconnection tableau calculus (Q877889) (← links)
- Liberalized variable splitting (Q877894) (← links)
- Hilbert's epsilon as an operator of indefinite committed choice (Q946570) (← links)
- Constraint satisfaction from a deductive viewpoint (Q1103421) (← links)
- A semantic backward chaining proof system (Q1193483) (← links)
- Let's plan it deductively! (Q1274761) (← links)
- Prolog technology for default reasoning: proof theory and compilation techniques (Q1275596) (← links)
- Simplification in a satisfiability checker for VLSI applications (Q1312163) (← links)
- Controlled integration of the cut rule into connection tableau calculi (Q1344875) (← links)
- IeanCOP: lean connection-based theorem proving (Q1404981) (← links)
- A uniform procedure for converting matrix proofs into sequent-style systems (Q1854382) (← links)
- A new methodology for query answering in default logics via structure-oriented theorem proving (Q1896370) (← links)
- TPS: A theorem-proving system for classical type theory (Q1923825) (← links)
- Machine learning guidance for connection tableaux (Q2031418) (← links)
- Set of support, demodulation, paramodulation: a historical perspective (Q2102923) (← links)
- The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics (Q2142078) (← links)
- Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\) (Q2577589) (← links)
- A Connection Calculus for the Description Logic $$ {\mathcal{ALC}} $$ (Q2814524) (← links)
- nanoCoP: A Non-clausal Connection Prover (Q2817929) (← links)
- A Non-clausal Connection Calculus (Q3010371) (← links)
- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions) (Q3541708) (← links)
- Lean induction principles for tableaux (Q4610315) (← links)
- Hintikka multiplicities in matrix decision methods for some propositional modal logics (Q4610320) (← links)
- Non-elementary speed-ups in proof length by different variants of classical analytic calculi (Q4610324) (← links)
- Skeptical query-answering in Constrained Default Logic (Q4632323) (← links)
- Incremental theory reasoning methods for semantic tableaux (Q4645229) (← links)
- The disconnection method (Q4645231) (← links)
- T-string unification: Unifying prefixes in non-classical proof methods (Q4645241) (← links)
- XRay: A prolog technology theorem prover for default reasoning: A system description (Q4647525) (← links)
- On the practical value of different definitional translations to normal form (Q4647537) (← links)
- Converting non-classical matrix proofs into sequent-style systems (Q4647538) (← links)
- Increasing the efficiency of automated theorem proving (Q4835513) (← links)
- (Q4886736) (← links)
- From Schütte’s Formal Systems to Modern Automated Deduction (Q5013905) (← links)
- Practical Proof Search for Coq by Type Inhabitation (Q5048991) (← links)
- Prolog Technology Reinforcement Learning Prover (Q5049033) (← links)
- Proof Search for the First-Order Connection Calculus in Maude (Q5179137) (← links)
- The search efficiency of theorem proving strategies (Q5210762) (← links)
- Model elimination without contrapositives (Q5210764) (← links)
- Detecting non-provable goals (Q5210774) (← links)
- Proving with BDDs and control of information (Q5210793) (← links)
- Semantic tableaux with ordering restrictions (Q5210807) (← links)
- KoMeT (Q5210812) (← links)
- Connection-based proof construction in linear logic (Q5234702) (← links)
- A query answering algorithm for Lukaszewicz' general open default theory (Q5236435) (← links)
