SETHEO

swMATH707MaRDI QIDQ13461

No author found.

Related Items (only showing first 100 items - show all)

Unnamed Item ⋮ Unnamed Item ⋮ Mark Stickel: his earliest work ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Controlled integration of the cut rule into connection tableau calculi ⋮ Efficient Low-Level Connection Tableaux ⋮ A new methodology for query answering in default logics via structure-oriented theorem proving ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ lean\(T^ AP\): Lean tableau-based deduction ⋮ The anatomy of vampire. Implementing bottom-up procedures with code trees ⋮ Octopus: combining learning and parallel search ⋮ The use of lemmas in the model elimination procedure ⋮ A disjunctive positive refinement of model elimination and its application to subsumption deletion ⋮ \textit{Theorema}: Towards computer-aided mathematical theory exploration ⋮ Nagging: A distributed, adversarial search-pruning technique applied to first-order inference ⋮ Unnamed Item ⋮ Unnamed Item ⋮ The disconnection tableau calculus ⋮ Linear and unit-resulting refutations for Horn theories ⋮ Craig interpolation with clausal first-order tableaux ⋮ Near-Horn Prolog and the ancestry family of procedures ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Short Conjunctive Normal Forms in Finitely Valued Logics ⋮ 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 ⋮ Free variable tableaux for propositional modal logics ⋮ Ordered tableaux: Extensions and applications ⋮ Subgoal alternation in model elimination ⋮ A framework for using knowledge in tableau proofs ⋮ Unnamed Item ⋮ The practicality of generating semantic trees for proofs of unsatisfiability ⋮ Unnamed Item ⋮ Connection tableaux with lazy paramodulation ⋮ leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions) ⋮ Towards a unified model of search in theorem-proving: subgoal-reduction strategies ⋮ Knowledge-based proof planning ⋮ SETHEO: A high-performance theorem prover ⋮ Combined reasoning by automated cooperation ⋮ First-Order Tableaux in Applications (Extended Abstract) ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Situational Calculus, linear connection proofs and STRIPS-like planning: An experimental comparison ⋮ T-string unification: Unifying prefixes in non-classical proof methods ⋮ Unnamed Item ⋮ SiCoTHEO: Simple competitive parallel theorem provers ⋮ XRay: A prolog technology theorem prover for default reasoning: A system description ⋮ Optimizing proof search in model elimination ⋮ Converting non-classical matrix proofs into sequent-style systems ⋮ Efficient model generation through compilation ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A Prolog technology theorem prover: A new exposition and implementation in Prolog ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Specifying and Verifying Organizational Security Properties in First-Order Logic ⋮ Machine learning guidance for connection tableaux ⋮ Unnamed Item ⋮ A domain-specific language for cryptographic protocols based on streams ⋮ Model elimination without contrapositives ⋮ Detecting non-provable goals ⋮ 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 ⋮ Automated reasoning with analytic tableaux and related methods. International conference, TABLEAUX 2000, St Andrews, Scotland, GB, July 3--7, 2000. Proceedings ⋮ Unnamed Item ⋮ Automated deduction. A basis for applications. Vol. 2: Systems and implementation techniques ⋮ Logic programming as a basis for lean automated deduction ⋮ Efficient model generation through compilation. ⋮ A uniform procedure for converting matrix proofs into sequent-style systems ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ Vampire getting noisy: Will random bits help conquer chaos? (system description) ⋮ A taxonomy of parallel strategies for deduction ⋮ Connection tableau calculi with disjunctive constraints ⋮ Evaluating general purpose automated theorem proving systems ⋮ Consolution as a framework for comparing calculi ⋮ Towards the qualitative, plan-based simulation of international crises

This page was built for software: SETHEO