scientific article
From MaRDI portal
Publication:3821629
zbMath0668.68104MaRDI QIDQ3821629
Publication date: 1988
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
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, Theorem proving for intensional logic, SATCHMORE: SATCHMO with RElevancy, History and Prospects for First-Order Automated Deduction, lean\(T^ AP\): Lean tableau-based deduction, 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, 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, Computer supported mathematics with \(\Omega\)MEGA, The disconnection tableau calculus, Craig interpolation with clausal first-order tableaux, Propositional calculus problems in CHIP, Role of logic programming in the FGCS project, Fifty Years of Prolog and Beyond, Programming in logic without logic programming, Computing answers with model elimination, Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover, 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, 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, \(\mathcal I\)-SATCHMORE: An improvement of \(\mathcal A\)-SATCHMORE, 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, 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, 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, Blocking and other enhancements for bottom-up model generation methods, The Fusemate logic programming system, SATCHMO, Lemma matching for a PTTP-based top-down theorem prover, Non-horn magic sets to incorporate top-down inference into bottom-up theorem proving, Soft typing for ordered resolution, Hyper tableaux, Completeness of hyper-resolution via the semantics of disjunctive logic programs, α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic, Efficient model generation through compilation., Generating relevant models, A relevance restriction strategy for automated deduction
