Resolution methods for the decision problem

DOI10.1007/3-540-56732-1zbMath0789.03013OpenAlexW1552596904MaRDI QIDQ1310269

No author found.

Publication date: 8 December 1993

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-56732-1

zbMATH Keywords

theorem provingproof theoryknowledge representation languagesdecision problemnarrowingresolution methoddecision algorithmsautomatical finite model buildingdecision classesfirst-order logic with function symbolsMaslov's \(K\)- classesordering refinementssemantic clash resolution

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Software, source code, etc. for problems pertaining to mathematical logic and foundations (03-04)

Related Items (25)

Representing and building models for decidable subclasses of equational clausal logic ⋮ Some techniques for proving termination of the hyperresolution calculus ⋮ Extracting models from clause sets saturated under semantic refinements of the resolution rule. ⋮ Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments ⋮ Model building with ordered resolution: Extracting models from saturated clause sets ⋮ A calculus combining resolution and enumeration for building finite models ⋮ Ordered tableaux: Extensions and applications ⋮ Simplifying and generalizing formulae in tableaux. Pruning the search space and building models ⋮ Deciding expressive description logics in the framework of resolution ⋮ A resolution-based decision procedure for \({\mathcal{SHOIQ}}\). ⋮ Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators ⋮ Towards a unified model of search in theorem-proving: subgoal-reduction strategies ⋮ A resolution theorem prover for intuitionistic logic ⋮ Semantic trees revisited: Some new completeness results ⋮ Optimized encodings of fragments of type theory in first order logic ⋮ Constructing Bachmair-Ganzinger Models ⋮ A Resolution-based Model Building Algorithm for a Fragment of OCC1N = ⋮ Combining enumeration and deductive techniques in order to increase the class of constructible infinite models ⋮ A method for building models automatically. Experiments with an extension of OTTER ⋮ Detecting non-provable goals ⋮ Semantic tableaux with ordering restrictions ⋮ Blocking and other enhancements for bottom-up model generation methods ⋮ A classification of non-liftable orders for resolution ⋮ Deciding the \(E^+\)-class by an a posteriori, liftable order ⋮ Deciding the guarded fragments by resolution

This page was built for publication: Resolution methods for the decision problem