SETHEO
From MaRDI portal
Cited in
(only showing first 100 items - show all)- A domain-specific language for cryptographic protocols based on streams
- SETHEO: A high-performance theorem prover
- A Prolog technology theorem prover: A new exposition and implementation in Prolog
- Let's plan it deductively!
- Prolog technology for default reasoning: proof theory and compilation techniques
- Heuristics used by HERBY for semantic tree theorem proving
- On the modelling of search in theorem proving -- towards a theory of strategy analysis
- SPS-parallelism+SETHEO=SPTHEO
- Consolution as a framework for comparing calculi
- PyRes
- Controlled integration of the cut rule into connection tableau calculi
- The use of lemmas in the model elimination procedure
- A disjunctive positive refinement of model elimination and its application to subsumption deletion
- Nagging: A distributed, adversarial search-pruning technique applied to first-order inference
- Clause trees: A tool for understanding and implementing resolution in automated reasoning
- Non-Horn clause logic programming
- Computing answers with model elimination
- Limited resource strategy in resolution theorem proving
- Depth-first proof search without backtracking for free-variable clausal tableaux
- IeanCOP: lean connection-based theorem proving
- AutoBayes/CC
- PLAGIATOR
- TGTP
- OTTER
- Automated reasoning with analytic tableaux and related methods. International conference, TABLEAUX 2000, St Andrews, Scotland, GB, July 3--7, 2000. Proceedings
- Automated deduction. A basis for applications. Vol. 2: Systems and implementation techniques
- A taxonomy of parallel strategies for deduction
- Connection tableau calculi with disjunctive constraints
- Evaluating general purpose automated theorem proving systems
- Towards the qualitative, plan-based simulation of international crises
- SPASS
- TPTP
- Efficient model generation through compilation.
- A uniform procedure for converting matrix proofs into sequent-style systems
- GrAnDe
- SATCHMO
- DCTP
- SCOTT
- A new methodology for query answering in default logics via structure-oriented theorem proving
- lean\(T^ AP\): Lean tableau-based deduction
- The anatomy of vampire. Implementing bottom-up procedures with code trees
- E-SETHEO
- Linear and unit-resulting refutations for Horn theories
- Near-Horn Prolog and the ancestry family of procedures
- Knowledge-based proof planning
- Machine learning guidance for connection tableaux
- Set of support, demodulation, paramodulation: a historical perspective
- Vampire getting noisy: Will random bits help conquer chaos? (system description)
- MGTP
- leanCoP
- ileanCoP
- Amphion
- JProver
- PARTHEO
- SicoTHEO
- leanTAP
- Octopus
- linTAP
- ModLeanTAP
- Roo
- Towards a unified model of search in theorem-proving: subgoal-reduction strategies
- Leibniz
- Craig interpolation with clausal first-order tableaux
- Using automated theorem provers in verification of protocols
- Theorem proving in large theories
- Deduction-based software component retrieval
- randoCoP
- The practicality of generating semantic trees for proofs of unsatisfiability
- scientific article; zbMATH DE number 1612565 (Why is no real title available?)
- scientific article; zbMATH DE number 1612567 (Why is no real title available?)
- scientific article; zbMATH DE number 1614712 (Why is no real title available?)
- EQP
- Model elimination and connection tableau procedures
- scientific article; zbMATH DE number 1696564 (Why is no real title available?)
- Automated deduction techniques for the management of personalized documents. (Extended abstract)
- Mark Stickel: his earliest work
- First-order tableaux in applications (extended abstract)
- Specifying and verifying organizational security properties in first-order logic
- Logic programming as a basis for lean automated deduction
- Waldmeister
- DISCOUNT
- UCPOP
- PROTEIN
- Bliksem
- 3TAP
- HERBY
- SPTHEO
- Efficient Low-Level Connection Tableaux
- scientific article; zbMATH DE number 4164187 (Why is no real title available?)
- mural
- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
- Peers-mcd
- PARTHENON
- THOT
- HARP
- METEOR
- Aquarius
- scientific article; zbMATH DE number 19780 (Why is no real title available?)
- xray
- KoMeT
This page was built for software: SETHEO
