On the refutational completeness of signed binary resolution and hyperresolution
type: Item
instance of: scholarly article
title: On the refutational completeness of signed binary resolution and hyperresolution
zbMATH Open document ID: 1191.03009
author: Dušan Guller
published in: Fuzzy Sets and Systems
publication date: 2009-11-17T00:00:00Z
review text: This article addresses the problem of refutational completeness of signed binary resolution and hyperresolution in many-valued logic. The main results of the paper can be summarized as follows: 1. After introducing the resolution calculi studied in the paper, the author shows that one of the rules of the calculus (namely the merging rule) is redundant. 2. Refutational completeness of signed resolution is studied. {\parindent=6mm \begin{itemize}\item[(a)] It is proved that refutational completeness is guaranteed provided that the sets of signs which appear in any subset of the clauses under consideration satisfy the ``finitary disjunction condition'' (the ``finitary disjunction condition'' holds for a family of sets \(X\) if for all \(Y \subseteq X\) such that \(\bigcap Y = \emptyset\) there exists a finite subset \(Y_f\) of \(Y\) with \(\bigcap Y_f = \emptyset\)). \item[(b)] It is shown that the additional restriction is essential. An example of a countable clausal theory is given which is unsatisfiable and for which no refutations by signed binary resolution (or hyperresolution) exist. \end{itemize}} 3. The satisfiability problem in many-valued logics is studied (both for finite and for infinite sets of truth values). A signed DPLL procedure is then introduced (which is sound and complete for finite sets of clauses and finite sets of truth values).
reviewed by: Viorica Sofronie-Stokkermans
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03B50
Mathematics Subject Classification ID: 03F07
zbMATH DE Number: 5634431
zbMATH Keywords: many-valued logics
zbMATH Keywords: automated deduction
zbMATH Keywords: signed resolution
zbMATH Keywords: satisfiability
zbMATH Keywords: signed logic
MaRDI profile type: Publication
full work available at URL: j.fss.2008.05.011
OpenAlex ID: W2021448969
cites work: Finiteness in infinite-valued Łukasiewicz logic
cites work: A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
cites work: Resolution-based theorem proving for many-valued logics
cites work: Herbrand’s Theorem for Prenex Gödel Logic and Its Consequences for Theorem Proving
cites work: Automated deduction for many-valued logics
cites work: Rewrite-based Equational Theorem Proving with Selection and Simplification
cites work: Ordered chaining calculi for first-order theories of transitive relations
cites work: The SAT problem of signed CNF formulas
cites work: Q5715690
cites work: Q5715661
cites work: Binary resolution over Boolean lattices
cites work: Binary resolution over complete residuated Stone lattices
cites work: Many-valued logic and mixed integer programming
cites work: Short Conjunctive Normal Forms in Finitely Valued Logics
cites work: Exploiting data dependencies in many-valued logics
cites work: Q4789457
cites work: The state of SAT
cites work: A framework for automated reasoning in multiple-valued logics
cites work: Satisfiability in many-valued sentential logic is NP-complete
cites work: Q4314600
cites work: Q4544342
cites work: Q4450440
cites work: Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators
cites work: Automated theorem proving by resolution in non-classical logics
DOI: 10.1016/J.FSS.2008.05.011
description: scientific article; zbMATH DE number 5634431