SATCHMO

swMATH6619MaRDI QIDQ18707FDOQ18707

Author name not available (Why is that?)

Cited In (89)

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

This page was built for software: SATCHMO