SATCHMO
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Completeness of hyper-resolution via the semantics of disjunctive logic programs
- 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
- SETHEO
- Disjunctive stable models: Unfounded sets, fixpoint semantics, and computation
- Computing answers with model elimination
- Model building with ordered resolution: Extracting models from saturated clause sets
- IeanCOP: lean connection-based theorem proving
- Eliminating redundant search space on backtracking for forward chaining theorem proving
- \(\mathcal I\)-SATCHMORE: An improvement of \(\mathcal A\)-SATCHMORE
- HYPROLOG
- OTTER
- Positive unit hyperresolution tableaux and their application to minimal model generation
- Ordered semantic hyper-linking
- Darwin
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- Structuring and automating hardware proofs in a higher-order theorem- proving environment
- FINDER
- Efficient model generation through compilation.
- wamcc
- GrAnDe
- R-SATCHMO
- DCTP
- I-SATCHMO
- SATCHMOREBID
- DWAM
- SATCHMOREBID: SATCHMO(RE) with BIDirectional relevancy
- SCOTT
- SATCHMORE: SATCHMO with RElevancy
- E-Darvin
- The anatomy of vampire. Implementing bottom-up procedures with code trees
- E-SETHEO
- iProver-Eq
- MGTP
- leanTAP
- aleanTAP
- Blocking and other enhancements for bottom-up model generation methods
- The model evolution calculus as a first-order DPLL method
- linTAP
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- Craig interpolation with clausal first-order tableaux
- Nonmonotonic reasoning: Towards efficient calculi and implementations
- Automated deduction techniques for the management of personalized documents. (Extended abstract)
- A fixpoint characterization of abductive logic programs
- Waldmeister
- SNARK
- CLIN
- PROTEIN
- P.rex
- Doris
- ModGen
- FALCON
- E-KRHyper
- 3TAP
- Denali
- The hyper tableaux calculus with equality and an application to finite model computation
- History and prospects for first-order automated deduction
- System Description: E- KRHyper
- Blocking and Other Enhancements for Bottom-Up Model Generation Methods
- HARP
- METEOR
- SLDNFA: An abductive procedure for abductive logic programs
- scientific article; zbMATH DE number 51274 (Why is no real title available?)
- KoMeT
- A new method for automated finite model building exploiting failures and symmetries
- SWISH DataLab
- scientific article; zbMATH DE number 1301750 (Why is no real title available?)
- scientific article; zbMATH DE number 1341618 (Why is no real title available?)
- scientific article; zbMATH DE number 1348475 (Why is no real title available?)
- scientific article; zbMATH DE number 1348483 (Why is no real title available?)
- scientific article; zbMATH DE number 515732 (Why is no real title available?)
- scientific article; zbMATH DE number 559756 (Why is no real title available?)
- Short Conjunctive Normal Forms in Finitely Valued Logics
- Model generation and state generation for disjunctive logic programs
- scientific article; zbMATH DE number 1950264 (Why is no real title available?)
- Programming in logic without logic programming
- 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
- Minimal model generation with positive unit hyper-resolution tableaux
- A tableau calculus for minimal model reasoning
- System description generating models by SEM
- Efficient model generation through compilation
- scientific article; zbMATH DE number 219222 (Why is no real title available?)
- scientific article; zbMATH DE number 753769 (Why is no real title available?)
- scientific article; zbMATH DE number 1926616 (Why is no real title available?)
- Hyperresolution and automated model building
- Superposition for bounded domains
- MACE4 and SEM: a comparison of finite model generators
- A resolution-based model building algorithm for a fragment of \(\mathcal{OCC}1\mathcal{N}_{=}\) (extended abstract)
- 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
- 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
This page was built for software: SATCHMO
