SETHEO
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Efficient model generation through compilation.
- The anatomy of vampire. Implementing bottom-up procedures with code trees
- Nagging: A distributed, adversarial search-pruning technique applied to first-order inference
- Automated Reasoning
- Set of support, demodulation, paramodulation: a historical perspective
- Vampire getting noisy: Will random bits help conquer chaos? (system description)
- Connection tableau calculi with disjunctive constraints
- scientific article; zbMATH DE number 1330425 (Why is no real title available?)
- A framework for using knowledge in tableau proofs
- Model elimination without contrapositives
- Lemma matching for a PTTP-based top-down theorem prover
- scientific article; zbMATH DE number 1943847 (Why is no real title available?)
- Towards the qualitative, plan-based simulation of international crises
- scientific article; zbMATH DE number 1222430 (Why is no real title available?)
- scientific article; zbMATH DE number 1389651 (Why is no real title available?)
- Automated reasoning with analytic tableaux and related methods. International conference, TABLEAUX 2000, St Andrews, Scotland, GB, July 3--7, 2000. Proceedings
- scientific article; zbMATH DE number 19780 (Why is no real title available?)
- scientific article; zbMATH DE number 1543301 (Why is no real title available?)
- Clause trees: A tool for understanding and implementing resolution in automated reasoning
- Near-Horn Prolog and the ancestry family of procedures
- scientific article; zbMATH DE number 1348483 (Why is no real title available?)
- Using automated theorem provers in verification of protocols
- scientific article; zbMATH DE number 1140678 (Why is no real title available?)
- Automatic verification of cryptographic protocols with SETHEO
- Mark Stickel: his earliest work
- Non-Horn clause logic programming
- The use of lemmas in the model elimination procedure
- Ordered tableaux: extensions and applications
- Mechanizing Mathematical Reasoning
- Automated deduction techniques for the management of personalized documents. (Extended abstract)
- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
- Octopus: combining learning and parallel search
- Automated Reasoning with Analytic Tableaux and Related Methods
- Detecting non-provable goals
- SiCoTHEO: Simple competitive parallel theorem provers
- scientific article; zbMATH DE number 7178359 (Why is no real title available?)
- A domain-specific language for cryptographic protocols based on streams
- A new methodology for query answering in default logics via structure-oriented theorem proving
- \textit{Theorema}: Towards computer-aided mathematical theory exploration
- scientific article; zbMATH DE number 1285157 (Why is no real title available?)
- Machine learning guidance for connection tableaux
- scientific article; zbMATH DE number 1612565 (Why is no real title available?)
- T-string unification: unifying prefixes in non-classical proof methods
- \(\mathsf{XRay}\): a Prolog technology theorem prover for default reasoning: a system description
- Combined reasoning by automated cooperation
- \textsf{Ko\(_{\mathsf{M}}\)eT}
- scientific article; zbMATH DE number 1552511 (Why is no real title available?)
- The disconnection tableau calculus
- scientific article; zbMATH DE number 1612567 (Why is no real title available?)
- Free-variable tableaux for propositional modal logics
- Let's plan it deductively!
- scientific article; zbMATH DE number 778198 (Why is no real title available?)
- scientific article; zbMATH DE number 516986 (Why is no real title available?)
- SETHEO: A high-performance theorem prover
- A Prolog technology theorem prover: A new exposition and implementation in Prolog
- Situational calculus, linear connection proofs and STRIPS-like planning: an experimental comparison
- Computing answers with model elimination
- SETHEO goes software engineering: application of ATP to software reuse
- On the modelling of search in theorem proving -- towards a theory of strategy analysis
- scientific article; zbMATH DE number 1552517 (Why is no real title available?)
- AutoBayes/CC
- PLAGIATOR
- TGTP
- OTTER
- SPASS
- TPTP
- DCTP
- GrAnDe
- SATCHMO
- SCOTT
- E-SETHEO
- MGTP
- ileanCoP
- leanCoP
- Amphion
- JProver
- leanTAP
- PARTHEO
- SicoTHEO
- Octopus
- linTAP
- ModLeanTAP
- Roo
- Leibniz
- randoCoP
- EQP
- Consolution as a framework for comparing calculi
- DISCOUNT
- Waldmeister
- Bliksem
- 3TAP
- PROTEIN
- HERBY
- UCPOP
- SPTHEO
- mural
- Peers-mcd
- PARTHENON
- HARP
- METEOR
This page was built for software: SETHEO
