The following pages link to SETHEO (Q13461):
Displayed 50 items.
- Mark Stickel: his earliest work (Q287332) (← links)
- Octopus: combining learning and parallel search (Q861370) (← links)
- \textit{Theorema}: Towards computer-aided mathematical theory exploration (Q865646) (← links)
- The disconnection tableau calculus (Q877889) (← links)
- Connection tableaux with lazy paramodulation (Q928656) (← links)
- Combined reasoning by automated cooperation (Q946572) (← links)
- A domain-specific language for cryptographic protocols based on streams (Q1001891) (← links)
- SETHEO: A high-performance theorem prover (Q1189726) (← links)
- A Prolog technology theorem prover: A new exposition and implementation in Prolog (Q1199932) (← links)
- Let's plan it deductively! (Q1274761) (← links)
- Prolog technology for default reasoning: proof theory and compilation techniques (Q1275596) (← links)
- Heuristics used by HERBY for semantic tree theorem proving (Q1277339) (← links)
- On the modelling of search in theorem proving -- towards a theory of strategy analysis (Q1281504) (← links)
- SPS-parallelism+SETHEO=SPTHEO (Q1284705) (← links)
- Consolution as a framework for comparing calculi (Q1322772) (← links)
- Controlled integration of the cut rule into connection tableau calculi (Q1344875) (← links)
- The use of lemmas in the model elimination procedure (Q1367083) (← links)
- A disjunctive positive refinement of model elimination and its application to subsumption deletion (Q1369080) (← links)
- Nagging: A distributed, adversarial search-pruning technique applied to first-order inference (Q1373304) (← links)
- Clause trees: A tool for understanding and implementing resolution in automated reasoning (Q1402732) (← links)
- Non-Horn clause logic programming (Q1402738) (← links)
- Computing answers with model elimination (Q1402748) (← links)
- Limited resource strategy in resolution theorem proving (Q1404979) (← links)
- Depth-first proof search without backtracking for free-variable clausal tableaux (Q1404980) (← links)
- IeanCOP: lean connection-based theorem proving (Q1404981) (← links)
- Automated reasoning with analytic tableaux and related methods. International conference, TABLEAUX 2000, St Andrews, Scotland, GB, July 3--7, 2000. Proceedings (Q1572743) (← links)
- Automated deduction. A basis for applications. Vol. 2: Systems and implementation techniques (Q1581359) (← links)
- A taxonomy of parallel strategies for deduction (Q1601867) (← links)
- Connection tableau calculi with disjunctive constraints (Q1604795) (← links)
- Evaluating general purpose automated theorem proving systems (Q1606324) (← links)
- Towards the qualitative, plan-based simulation of international crises (Q1610171) (← links)
- Efficient model generation through compilation. (Q1854374) (← links)
- A uniform procedure for converting matrix proofs into sequent-style systems (Q1854382) (← links)
- A new methodology for query answering in default logics via structure-oriented theorem proving (Q1896370) (← links)
- lean\(T^ AP\): Lean tableau-based deduction (Q1904400) (← links)
- The anatomy of vampire. Implementing bottom-up procedures with code trees (Q1904404) (← links)
- Linear and unit-resulting refutations for Horn theories (Q1923821) (← links)
- Near-Horn Prolog and the ancestry family of procedures (Q1924724) (← links)
- Knowledge-based proof planning (Q1978469) (← links)
- Machine learning guidance for connection tableaux (Q2031418) (← links)
- Set of support, demodulation, paramodulation: a historical perspective (Q2102923) (← links)
- Vampire getting noisy: Will random bits help conquer chaos? (system description) (Q2104552) (← links)
- Towards a unified model of search in theorem-proving: subgoal-reduction strategies (Q2456542) (← links)
- Craig interpolation with clausal first-order tableaux (Q2666953) (← links)
- (Q2702601) (← links)
- (Q2702602) (← links)
- (Q2702605) (← links)
- The practicality of generating semantic trees for proofs of unsatisfiability (Q2710799) (← links)
- (Q2721210) (← links)
- (Q2721213) (← links)