SETHEO
From MaRDI portal
Software:13461
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