The following pages link to (Q3821629):
Displayed 50 items.
- SATCHMO (Q18707) (← links)
- Generating relevant models (Q809621) (← links)
- A relevance restriction strategy for automated deduction (Q814429) (← links)
- Reasoning under minimal upper bounds in propositional logic (Q861253) (← links)
- Representing and building models for decidable subclasses of equational clausal logic (Q861367) (← links)
- Some techniques for proving termination of the hyperresolution calculus (Q861692) (← links)
- Computer supported mathematics with \(\Omega\)MEGA (Q865650) (← links)
- The disconnection tableau calculus (Q877889) (← links)
- Completeness of hyper-resolution via the semantics of disjunctive logic programs (Q1041788) (← links)
- Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction (Q1344881) (← links)
- An alternative approach to the semantics of disjunctive logic programs and deductive databases (Q1344892) (← links)
- Disjunctive stable models: Unfounded sets, fixpoint semantics, and computation (Q1363783) (← links)
- Computing answers with model elimination (Q1402748) (← links)
- Model building with ordered resolution: Extracting models from saturated clause sets (Q1404975) (← links)
- IeanCOP: lean connection-based theorem proving (Q1404981) (← links)
- Eliminating redundant search space on backtracking for forward chaining theorem proving (Q1412130) (← links)
- \(\mathcal I\)-SATCHMORE: An improvement of \(\mathcal A\)-SATCHMORE (Q1429427) (← links)
- Semantically-guided goal-sensitive reasoning: inference system and completeness (Q1707598) (← links)
- Structuring and automating hardware proofs in a higher-order theorem- proving environment (Q1801500) (← links)
- Efficient model generation through compilation. (Q1854374) (← links)
- SATCHMOREBID: SATCHMO(RE) with BIDirectional relevancy (Q1877374) (← links)
- Theorem proving for intensional logic (Q1891256) (← links)
- SATCHMORE: SATCHMO with RElevancy (Q1891262) (← links)
- lean\(T^ AP\): Lean tableau-based deduction (Q1904400) (← links)
- The anatomy of vampire. Implementing bottom-up procedures with code trees (Q1904404) (← links)
- The Fusemate logic programming system (Q2055893) (← links)
- Blocking and other enhancements for bottom-up model generation methods (Q2303239) (← links)
- The model evolution calculus as a first-order DPLL method (Q2389629) (← links)
- Craig interpolation with clausal first-order tableaux (Q2666953) (← links)
- History and Prospects for First-Order Automated Deduction (Q3454079) (← links)
- Programming in logic without logic programming (Q4593027) (← links)
- MGTP: A model generation theorem prover — Its advanced features and applications — (Q4610311) (← links)
- Tableaux for diagnosis applications (Q4610316) (← links)
- Projection: A unification procedure for tableaux in Conceptual Graphs (Q4610329) (← links)
- Simplifying and generalizing formulae in tableaux. Pruning the search space and building models (Q4610336) (← links)
- Minimal model generation with positive unit hyper-resolution tableaux (Q4645233) (← links)
- A tableau calculus for minimal model reasoning (Q4645243) (← links)
- System description generating models by SEM (Q4647530) (← links)
- Efficient model generation through compilation (Q4647539) (← links)
- Superposition for Bounded Domains (Q4913861) (← links)
- MACE4 and SEM: A Comparison of Finite Model Generators (Q4913862) (← links)
- A Resolution-based Model Building Algorithm for a Fragment of OCC1N = (Q4916224) (← links)
- Propositional calculus problems in CHIP (Q5096196) (← links)
- Role of logic programming in the FGCS project (Q5096224) (← links)
- The crisis in finite mathematics: Automated reasoning as cause and cure (Q5210758) (← links)
- A method for building models automatically. Experiments with an extension of OTTER (Q5210763) (← links)
- Semantically guided first-order theorem proving using hyper-linking (Q5210771) (← links)
- Proving with BDDs and control of information (Q5210793) (← links)
- Problems on the generation of finite models (Q5210810) (← links)
- LeanT A P: Lean tableau-based theorem proving (Q5210813) (← links)