SETHEO

swMATH707MaRDI QIDQ13461FDOQ13461

Author name not available (Why is that?)

Official website: http://www2.tcs.ifi.lmu.de/~letz/TU/setheo/

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

• Efficient model generation through compilation.
• Automated Reasoning
• Nagging: A distributed, adversarial search-pruning technique applied to first-order inference
• Set of support, demodulation, paramodulation: a historical perspective
• Vampire getting noisy: Will random bits help conquer chaos? (system description)
• Title not available (Why is that?)
• Connection tableau calculi with disjunctive constraints
• Towards the qualitative, plan-based simulation of international crises
• Title not available (Why is that?)
• 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
• Ordered tableaux: extensions and applications
• Automated deduction techniques for the management of personalized documents. (Extended abstract)
• Non-Horn clause logic programming
• The use of lemmas in the model elimination procedure
• Title not available (Why is that?)
• Title not available (Why is that?)
• A new methodology for query answering in default logics via structure-oriented theorem proving
• T-string unification: unifying prefixes in non-classical proof methods
• \(\mathsf{XRay}\): a Prolog technology theorem prover for default reasoning: a system description
• A domain-specific language for cryptographic protocols based on streams
• \textsf{Ko\(_{\mathsf{M}}\)eT}
• Title not available (Why is that?)
• Machine learning guidance for connection tableaux
• Title not available (Why is that?)
• Let's plan it deductively!
• Title not available (Why is that?)
• Computing answers with model elimination
• Title not available (Why is that?)
• Free variable tableaux for propositional modal logics
• Craig interpolation with clausal first-order tableaux
• Title not available (Why is that?)
• Title not available (Why is that?)
• PyRes
• Logic programming as a basis for lean automated deduction
• Subgoal alternation in model elimination
• Efficient model generation through compilation
• BanditFuzz
• Semantic tableaux with ordering restrictions
• Connection tableaux with lazy paramodulation
• Integration of automated and interactive theorem proving in ILF
• Controlled use of clausal lemmas in connection tableau calculi
• A disjunctive positive refinement of model elimination and its application to subsumption deletion
• Automated deduction. A basis for applications. Vol. 2: Systems and implementation techniques
• Converting non-classical matrix proofs into sequent-style systems
• Deduction-based software component retrieval
• The practicality of generating semantic trees for proofs of unsatisfiability
• Linear and unit-resulting refutations for Horn theories
• A framework for using knowledge in tableau proofs
• Lemma matching for a PTTP-based top-down theorem prover
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Detecting non-provable goals
• SiCoTHEO: Simple competitive parallel theorem provers
• Title not available (Why is that?)
• Title not available (Why is that?)
• SETHEO goes software engineering: application of ATP to software reuse
• Situational calculus, linear connection proofs and STRIPS-like planning: an experimental comparison
• First-order tableaux in applications (extended abstract)
• Title not available (Why is that?)
• Automated Reasoning with Analytic Tableaux and Related Methods
• An automatic proof of Gödel's incompleteness theorem
• Title not available (Why is that?)
• Title not available (Why is that?)
• Specifying and verifying organizational security properties in first-order logic
• The anatomy of vampire. Implementing bottom-up procedures with code trees
• 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
• Mechanizing Mathematical Reasoning
• Mark Stickel: his earliest work
• 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
• \textit{Theorema}: Towards computer-aided mathematical theory exploration
• Title not available (Why is that?)
• Free-variable tableaux for propositional modal logics
• Combined reasoning by automated cooperation
• The disconnection tableau calculus
• SETHEO: A high-performance theorem prover
• A Prolog technology theorem prover: A new exposition and implementation in Prolog
• On the modelling of search in theorem proving -- towards a theory of strategy analysis
• Consolution as a framework for comparing calculi
• Optimizing proof search in model elimination
• Depth-first proof search without backtracking for free-variable clausal tableaux
• 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?)
• SPASS
• DCTP
• GrAnDe
• SATCHMO
• SCOTT

This page was built for software: SETHEO