SETHEO

swMATH707MaRDI QIDQ13461FDOQ13461

Author name not available (Why is that?)

Cited In (only showing first 100 items - show all)

• KoMeT
• The anatomy of vampire. Implementing bottom-up procedures with code trees
• Automated Reasoning
• Nagging: A distributed, adversarial search-pruning technique applied to first-order inference
• Title not available (Why is that?)
• Model elimination without contrapositives
• Automated reasoning with analytic tableaux and related methods. International conference, TABLEAUX 2000, St Andrews, Scotland, GB, July 3--7, 2000. Proceedings
• Title not available (Why is that?)
• Clause trees: A tool for understanding and implementing resolution in automated reasoning
• Title not available (Why is that?)
• Near-Horn Prolog and the ancestry family of procedures
• Using automated theorem provers in verification of protocols
• Title not available (Why is that?)
• Automatic verification of cryptographic protocols with SETHEO
• Mechanizing Mathematical Reasoning
• Mark Stickel: his earliest work
• Non-Horn clause logic programming
• The use of lemmas in the model elimination procedure
• leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
• Automated Reasoning with Analytic Tableaux and Related Methods
• Octopus: combining learning and parallel search
• A new methodology for query answering in default logics via structure-oriented theorem proving
• A domain-specific language for cryptographic protocols based on streams
• \textit{Theorema}: Towards computer-aided mathematical theory exploration
• Title not available (Why is that?)
• Title not available (Why is that?)
• Free-variable tableaux for propositional modal logics
• Combined reasoning by automated cooperation
• The disconnection tableau calculus
• Let's plan it deductively!
• Title not available (Why is that?)
• SETHEO: A high-performance theorem prover
• A Prolog technology theorem prover: A new exposition and implementation in Prolog
• Computing answers with model elimination
• On the modelling of search in theorem proving -- towards a theory of strategy analysis
• Consolution as a framework for comparing calculi
• Title not available (Why is that?)
• Optimizing proof search in model elimination
• Depth-first proof search without backtracking for free-variable clausal tableaux
• Free variable tableaux for propositional modal logics
• A uniform procedure for converting matrix proofs into sequent-style systems
• Controlled integration of the cut rule into connection tableau calculi
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Evaluating general purpose automated theorem proving systems
• Knowledge-based proof planning
• IeanCOP: lean connection-based theorem proving
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• ILF-SETHEO
• Efficient Low-Level Connection Tableaux
• Limited resource strategy in resolution theorem proving
• Title not available (Why is that?)
• Title not available (Why is that?)
• Prolog technology for default reasoning: proof theory and compilation techniques
• Title not available (Why is that?)
• Towards a unified model of search in theorem-proving: subgoal-reduction strategies
• Ordered tableaux: Extensions and applications
• Connection tableaux with lazy paramodulation
• Title not available (Why is that?)
• Title not available (Why is that?)
• Model elimination and connection tableau procedures
• Short Conjunctive Normal Forms in Finitely Valued Logics
• Heuristics used by HERBY for semantic tree theorem proving
• SPS-parallelism+SETHEO=SPTHEO
• A disjunctive positive refinement of model elimination and its application to subsumption deletion
• A taxonomy of parallel strategies for deduction
• T-string unification: Unifying prefixes in non-classical proof methods
• Converting non-classical matrix proofs into sequent-style systems
• XRay: A prolog technology theorem prover for default reasoning: A system description
• lean\(T^ AP\): Lean tableau-based deduction
• Linear and unit-resulting refutations for Horn theories
• Theorem proving in large theories
• Efficient model generation through compilation.
• Specifying and Verifying Organizational Security Properties in First-Order Logic
• Set of support, demodulation, paramodulation: a historical perspective
• Vampire getting noisy: Will random bits help conquer chaos? (system description)
• A framework for using knowledge in tableau proofs
• Connection tableau calculi with disjunctive constraints
• Lemma matching for a PTTP-based top-down theorem prover
• SETHEO goes software engineering: Application of ATP to software reuse
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Towards the qualitative, plan-based simulation of international crises
• Title not available (Why is that?)
• Automated deduction techniques for the management of personalized documents. (Extended abstract)
• Detecting non-provable goals
• SiCoTHEO: Simple competitive parallel theorem provers
• Title not available (Why is that?)
• Title not available (Why is that?)
• Machine learning guidance for connection tableaux
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Automated Reasoning with Analytic Tableaux and Related Methods
• An automatic proof of Gödel's incompleteness theorem

This page was built for software: SETHEO