SATCHMO

swMATH6619MaRDI QIDQ18707

No author found.

Related Items (89)

SATCHMOREBID: SATCHMO(RE) with BIDirectional relevancy ⋮ Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction ⋮ An alternative approach to the semantics of disjunctive logic programs and deductive databases ⋮ SATCHMORE: SATCHMO with RElevancy ⋮ History and Prospects for First-Order Automated Deduction ⋮ About Knowledge and Inference in Logical and Relational Learning ⋮ Unnamed Item ⋮ Logic for Programming, Artificial Intelligence, and Reasoning ⋮ The anatomy of vampire. Implementing bottom-up procedures with code trees ⋮ The model evolution calculus as a first-order DPLL method ⋮ Disjunctive stable models: Unfounded sets, fixpoint semantics, and computation ⋮ Unnamed Item ⋮ Reasoning under minimal upper bounds in propositional logic ⋮ Representing and building models for decidable subclasses of equational clausal logic ⋮ Some techniques for proving termination of the hyperresolution calculus ⋮ Unnamed Item ⋮ Computer supported mathematics with \(\Omega\)MEGA ⋮ The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 ⋮ Unnamed Item ⋮ Unnamed Item ⋮ The disconnection tableau calculus ⋮ Craig interpolation with clausal first-order tableaux ⋮ Unnamed Item ⋮ Programming in logic without logic programming ⋮ Short Conjunctive Normal Forms in Finitely Valued Logics ⋮ Computing answers with model elimination ⋮ Model building with ordered resolution: Extracting models from saturated clause sets ⋮ IeanCOP: lean connection-based theorem proving ⋮ Extracting the resolution algorithm from a completeness proof for the propositional calculus ⋮ Eliminating redundant search space on backtracking for forward chaining theorem proving ⋮ Semantically-guided goal-sensitive reasoning: inference system and completeness ⋮ MGTP: A model generation theorem prover — Its advanced features and applications — ⋮ Tableaux for diagnosis applications ⋮ Projection: A unification procedure for tableaux in Conceptual Graphs ⋮ Simplifying and generalizing formulae in tableaux. Pruning the search space and building models ⋮ Hyperresolution and automated model building ⋮ Model generation and state generation for disjunctive logic programs ⋮ \(\mathcal I\)-SATCHMORE: An improvement of \(\mathcal A\)-SATCHMORE ⋮ Abductive logic programming agents with destructive databases ⋮ Automating Coherent Logic ⋮ Minimal model generation with positive unit hyper-resolution tableaux ⋮ A tableau calculus for minimal model reasoning ⋮ Mechanizing Mathematical Reasoning ⋮ System description generating models by SEM ⋮ Efficient model generation through compilation ⋮ Unnamed Item ⋮ Superposition for Bounded Domains ⋮ MACE4 and SEM: A Comparison of Finite Model Generators ⋮ A Resolution-based Model Building Algorithm for a Fragment of OCC1N = ⋮ Theorem proving techniques for view deletion in databases ⋮ Combining enumeration and deductive techniques in order to increase the class of constructible infinite models ⋮ Logic programming, knowledge representation, and nonmonotonic reasoning. Essays dedicated to Michael Gelfond on the occasion of his 65th birthday ⋮ SLDNFA: An abductive procedure for abductive logic programs ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Automated reasoning with analytic tableaux and related methods. 20th international conference, TABLEAUX 2011, Bern, Switzerland, July 4--8, 2011. Proceedings ⋮ Unnamed Item ⋮ I-SATCHMO: An improvement of SATCHMO ⋮ Unnamed Item ⋮ System Description: E- KRHyper ⋮ KI 2004: Advances in Artificial Intelligence ⋮ Blocking and Other Enhancements for Bottom-Up Model Generation Methods ⋮ Unnamed Item ⋮ Structuring and automating hardware proofs in a higher-order theorem- proving environment ⋮ The crisis in finite mathematics: Automated reasoning as cause and cure ⋮ A method for building models automatically. Experiments with an extension of OTTER ⋮ Semantically guided first-order theorem proving using hyper-linking ⋮ Proving with BDDs and control of information ⋮ Problems on the generation of finite models ⋮ LeanT A P: Lean tableau-based theorem proving ⋮ Automated Reasoning with Analytic Tableaux and Related Methods ⋮ Blocking and other enhancements for bottom-up model generation methods ⋮ Lemma matching for a PTTP-based top-down theorem prover ⋮ Non-horn magic sets to incorporate top-down inference into bottom-up theorem proving ⋮ Constructing a normal form for Property Theory ⋮ Soft typing for ordered resolution ⋮ Hyper tableaux ⋮ The Hyper Tableaux Calculus with Equality and an Application to Finite Model Computation ⋮ A new method for automated finite model building exploiting failures and symmetries ⋮ Completeness of hyper-resolution via the semantics of disjunctive logic programs ⋮ Positive unit hyperresolution tableaux and their application to minimal model generation ⋮ Ordered semantic hyper-linking ⋮ α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic ⋮ Automated Model Building: From Finite to Infinite Models ⋮ A fixpoint characterization of abductive logic programs ⋮ Efficient model generation through compilation. ⋮ Generating relevant models ⋮ A relevance restriction strategy for automated deduction

This page was built for software: SATCHMO