loading...
Deciding the Satisfiability of Propositional Formulas in Finitely-Valued Signed Logics
May 22-May 24
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ISMVL.2008.4138th International Symposium on Multi ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Signed logic is a way of expressing the semantics of many-valued connectives and quantifiers in a formalism that is well-suited for automated reasoning. In this paper we consider propositional, finitely-valued formulas in clausal normal form. We show that checking the satisfiability of formulas with three or more literals per clause is eitherNP-complete or trivial, depending on whether the intersection of all signs is empty or not. The satisfiability of bijunctive formulas, i.e., of formulas with at most two literals per clause, is decidable in linear time if the signs form a Helly family, and is NP-complete otherwise. We present a polynomial-time algorithm for deciding whether a given set of signs satisfies the Helly property. Our results unify and extend previous results obtained for particular sets of signs.
Index Terms:
complexity, satisfiability, propositional logic, many-valued logic, Helly property
Citation:
Victor Chepoi, Nadia Creignou, Miki Hermann, Gernot Salzer, "Deciding the Satisfiability of Propositional Formulas in Finitely-Valued Signed Logics," ismvl, pp.100-105, 38th International Symposium on Multiple Valued Logic (ismvl 2008), 2008
Usage of this product signifies your acceptance of the Terms of Use.