swMATH6619MaRDI QIDQ18707FDOQ18707
Author name not available (Why is that?)
Official website: http://en.wikibooks.org/wiki/Logic_for_Computer_Scientists/Predicate_Logic/SATCHMO
Cited In (only showing first 100 items - show all)
- The anatomy of vampire. Implementing bottom-up procedures with code trees
- 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
- 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
- Title not available (Why is that?)
- 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?)
- 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
- Superposition for bounded domains
- 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
- 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?)
- A resolution-based model building algorithm for a fragment of \(\mathcal{OCC}1\mathcal{N}_{=}\) (extended abstract)
- Ordered semantic hyper-linking
- FINDER
- DCTP
- DWAM
- GrAnDe
- I-SATCHMO
- R-SATCHMO
- SATCHMOREBID
- SCOTT
- wamcc
- E-Darvin
- E-SETHEO
- IeanCOP: lean connection-based theorem proving
- iProver-Eq
- MGTP
- aleanTAP
- leanTAP
- linTAP
- Title not available (Why is that?)
- SLDNFA: An abductive procedure for abductive logic programs
- FALCON
- CLIN
- SNARK
- Waldmeister
- Doris
- E-KRHyper
- 3TAP
- ModGen
- P.rex
- PROTEIN
- Denali
- HARP
- METEOR
- KoMeT
- SWISH DataLab
- Automated Model Building: From Finite to Infinite Models
- 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
- 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
- Short Conjunctive Normal Forms in Finitely Valued Logics
- Generating relevant models
- Programming in logic without logic programming
- SATCHMOREBID: SATCHMO(RE) with BIDirectional relevancy
- Disjunctive stable models: Unfounded sets, fixpoint semantics, and computation
- Hyper tableaux
- Hyperresolution and automated model building
- A relevance restriction strategy for automated deduction
- A new method for automated finite model building exploiting failures and symmetries
- Efficient model generation through compilation.
- Koala
- VeriFly
- Blocking and other enhancements for bottom-up model generation methods
- α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic
- Theorem proving techniques for view deletion in databases
- Lemma matching for a PTTP-based top-down theorem prover
- Eliminating redundant search space on backtracking for forward chaining theorem proving
- Title not available (Why is that?)
- System description generating models by SEM
- \(\mathcal I\)-SATCHMORE: An improvement of \(\mathcal A\)-SATCHMORE
- Title not available (Why is that?)
- Automated deduction techniques for the management of personalized documents. (Extended abstract)
- About knowledge and inference in logical and relational learning
This page was built for software: SATCHMO
