Resolution decision procedures
The paper presents systematically investigation of the resolution method with respect to its potential as decision procedure and as a tool for a model building.NEWLINENEWLINENEWLINEIt is well known that different types of resolution refinements (ordering strategies, hyperresolution and other) can be turned in to effective means for deciding satisfiability of certain classes of clause sets. This problem was investigated in the papers of H. Yoyner, S. Maslov, N. Zamov and other. The paper reviews some generalizations of their results.NEWLINENEWLINENEWLINEThe authors introduce a notion of nonliftable ordering and show than nonliftable orderings are complete for some classes, for example the class \(E^+\) and the class \(K\) of Maslov.NEWLINENEWLINENEWLINEAuthors investigate the potential of hyperresolution as decision procedure. And show that hyperresolution decides the class \(\text{BSH}^*\), i.e. this refinement of the resolution principle generates the finite set of clauses for all formulae from \(\text{BSH}^*\).NEWLINENEWLINENEWLINEAnalogous result is valid for the classes PVD and OCCI and other.NEWLINENEWLINENEWLINEThen authors discuss the problem of extracting Herbrand model from finite set of clauses which are obtained by hyperresolution for a satisfiable set of clauses. These results can be extended to modal logics and description logics.NEWLINENEWLINEFor the entire collection see [Zbl 0964.00020].
- An overview of resolution decision procedures
- scientific article; zbMATH DE number 1418449
- Resolution methods for the decision problem
- Choice resolutions
- scientific article; zbMATH DE number 4128785
- scientific article; zbMATH DE number 4150119
- Categorical resolutions
- Regular Resolution Versus Unrestricted Resolution
- scientific article; zbMATH DE number 1215470
- Labelled splitting
- A new methodology for developing deduction methods
- Completeness of hyper-resolution via the semantics of disjunctive logic programs
- Decision tactics for derivation search in the resolution method
- Resolution methods for the decision problem
- Extracting models from clause sets saturated under semantic refinements of the resolution rule.
- Hyperresolution for guarded formulae
- Deciding the E^+-class by an a posteriori, liftable order
- On compatibilities of -lock resolution method in linguistic truth-valued lattice-valued logic
- Superposition as a decision procedure for timed automata
- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
- SGGS decision procedures
- The model evolution calculus as a first-order DPLL method
- Towards a unified model of search in theorem-proving: subgoal-reduction strategies
- Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically
- Mechanising first-order temporal resolution
- An overview of resolution decision procedures
- scientific article; zbMATH DE number 1614714 (Why is no real title available?)
- Semantically-guided goal-sensitive reasoning: model representation
- scientific article; zbMATH DE number 440110 (Why is no real title available?)
- Simulation and synthesis of deduction calculi
- Second-order quantifier elimination on relational monadic formulas -- a basic method and some less expected applications
- Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
- Verification of Security Protocols with a Bounded Number of Sessions Based on Resolution for Rigid Variables
- Classic-Like Analytic Tableaux for Finite-Valued Logics
- scientific article; zbMATH DE number 1341614 (Why is no real title available?)
- scientific article; zbMATH DE number 512974 (Why is no real title available?)
- scientific article; zbMATH DE number 516992 (Why is no real title available?)
- scientific article; zbMATH DE number 515732 (Why is no real title available?)
- scientific article; zbMATH DE number 2090304 (Why is no real title available?)
- scientific article; zbMATH DE number 910745 (Why is no real title available?)
- Consequence-based and fixed-parameter tractable reasoning in description logics
- Canonical ground Horn theories
- First-order resolution methods for modal logics
- A resolution-based model building algorithm for a fragment of \(\mathcal{OCC}1\mathcal{N}_{=}\) (extended abstract)
- scientific article; zbMATH DE number 1418449 (Why is no real title available?)
- Decidability Results for Saturation-Based Model Building
- A classification of non-liftable orders for resolution
- Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
- On the complexity of Maslov's class K
- First-order automatic literal model generation
- Bivalent semantics, generalized compositionality and analytic classic-like tableaux for finite-valued logics
- Representing and building models for decidable subclasses of equational clausal logic
- Some techniques for proving termination of the hyperresolution calculus
- Tree tuple languages from the logic programming point of view
- Defining answer classes using resolution refutation
- A resolution-based decision procedure for \({\mathcal{SHOIQ}}\).
- Deciding effectively propositional logic using DPLL and substitution sets
This page was built for publication: Resolution decision procedures
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2751377)
