Pages that link to "Item:Q1189726"

The following pages link to SETHEO: A high-performance theorem prover (Q1189726):

Displaying 50 items.

• Mark Stickel: his earliest work (Q287332) (← links)
• Theo: An interactive proof development system (Q688727) (← links)
• Octopus: combining learning and parallel search (Q861370) (← links)
• \textit{Theorema}: Towards computer-aided mathematical theory exploration (Q865646) (← links)
• Connection tableaux with lazy paramodulation (Q928656) (← links)
• A Prolog technology theorem prover: A new exposition and implementation in Prolog (Q1199932) (← links)
• Let's plan it deductively! (Q1274761) (← 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)
• SET-VAR (Q1319383) (← 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)
• Non-Horn clause logic programming (Q1402738) (← links)
• Computing answers with model elimination (Q1402748) (← links)
• IeanCOP: lean connection-based theorem proving (Q1404981) (← links)
• Evaluating general purpose automated theorem proving systems (Q1606324) (← links)
• Towards the qualitative, plan-based simulation of international crises (Q1610171) (← 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)
• lean\(T^ AP\): Lean tableau-based deduction (Q1904400) (← links)
• Linear and unit-resulting refutations for Horn theories (Q1923821) (← links)
• Near-Horn Prolog and the ancestry family of procedures (Q1924724) (← links)
• Knowledge-based proof planning (Q1978469) (← links)
• Machine learning guidance for connection tableaux (Q2031418) (← links)
• Set of support, demodulation, paramodulation: a historical perspective (Q2102923) (← links)
• Vampire getting noisy: Will random bits help conquer chaos? (system description) (Q2104552) (← links)
• Towards a unified model of search in theorem-proving: subgoal-reduction strategies (Q2456542) (← links)
• Craig interpolation with clausal first-order tableaux (Q2666953) (← links)
• Specifying and Verifying Organizational Security Properties in First-Order Logic (Q3058451) (← links)
• leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions) (Q3541708) (← links)
• Large theory reasoning with SUMO at CASC (Q3568226) (← links)
• Free variable tableaux for propositional modal logics (Q4610317) (← links)
• Ordered tableaux: Extensions and applications (Q4610325) (← links)
• Subgoal alternation in model elimination (Q4610327) (← links)
• A framework for using knowledge in tableau proofs (Q4610337) (← links)
• Situational Calculus, linear connection proofs and STRIPS-like planning: An experimental comparison (Q4645236) (← links)
• T-string unification: Unifying prefixes in non-classical proof methods (Q4645241) (← links)
• SiCoTHEO: Simple competitive parallel theorem provers (Q4647520) (← links)
• Optimizing proof search in model elimination (Q4647531) (← links)
• Converting non-classical matrix proofs into sequent-style systems (Q4647538) (← links)
• From Schütte’s Formal Systems to Modern Automated Deduction (Q5013905) (← links)
• (Q5020994) (← links)
• Model elimination without contrapositives (Q5210764) (← links)
• Detecting non-provable goals (Q5210774) (← links)
• Semantic tableaux with ordering restrictions (Q5210807) (← links)
• KoMeT (Q5210812) (← links)
• ILF-SETHEO (Q5234690) (← links)
• SETHEO goes software engineering: Application of ATP to software reuse (Q5234691) (← links)
• Automatic verification of cryptographic protocols with SETHEO (Q5234693) (← links)
• An automatic proof of Gödel's incompleteness theorem (Q5906916) (← links)