Abstract
In this paper we deal with the SAT problem in many-valued logics which is of relevant interest in many areas of Artificial Intelligence and Computer Science. Regarding tractability issues, several works have been previously published solving polynomially some clausal many-valued SAT problems. Thus, our aim is to show that certain non-clausal many-valued SAT problems can be solved in polynomial time too, extending in this way, earlier results from the clausal framework to the more general non-clausal one.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
E. Altamirano and G. Escalada-Imaz. Algoritmos óptimos para algunas teorías de Horn factorizadas. In II Congrés Catalá d’Intel-ligéncia Artificial, CCIA’99, pages 31–38, Girona, Spain, october 1999.
E. Altamirano and G. Escalada-Imaz. An almost linear class of multiple-valued non-clausal Horn formulas. In X Congreso Español sobre Tecnologías y Lógica Fuzzy, ESTYLF’00, pages 145–150, Sevilla, Spain, September 2000.
E. Altamirano and G. Escalada-Imaz. An efficient proof method for non-clausal reasoning. In XII International Symposium on Methodologies for Intelligent Systems, volume 1932 of LNAI, pages 534–542, Charlotte, USA, October 2000. Springer-Verlag.
E. Altamirano and G. Escalada-Imaz. Finding tractable formulas in NNF. In I International Conference on Computational Logic, volume 1861 of LNAI, pages 493–507, London, UK, July 2000. Springer-Verlag.
B. Beckert, R. Hähnle, and F. Manya. Transformations between signed and classical clause logic. In Proc. Int. Symp. on Multiple Valued Logics, ISMVL’99, Freiburg, Germany, 1999.
G. Escalada-Imaz. Moteurs d’Inférence Lineaires en Chaŷnage-Avant pour une classe de Systémes de Régles. Technical Report LAAS-89172, Laboratoire D’Automatique et Analyse des Systemes, Toulouse, France, 1989.
G. Escalada-Imaz. Optimisation d’algorithmes d’inference monotone en logique des propositions et du premier ordre. PhD thesis, Université Paul Sabatier, Toulouse, France, 1989.
G. Escalada-Imaz and F. Manya. The satisfiability problem for multiple-valued horn formulae. In Proc. International Symposium on Multiple-Valued Logics, ISMVL’94, pages 250–256, Boston/MA, USA, 1994. IEEE Press, Los Alamitos.
G. Escalada-Imaz and F. Manya. On the 2-SAT problem for signed formulas. In Proc. Workshop/Conference on Many-Valued Logics for Computer Science Applications, COST Action 15., Barcelona, Spain, 1996.
G. Escalada-Imaz and A.M. Martínez-Enríquez. Motores de Inferencia de Complejidad Optima de encadenamiento hacia adelante para diversas clases de sistemas de reglas. Informática y Automática, 27(3):23–30, 1994.
M. Ghallab and G. Escalada-Imaz. A linear control algorithm for a class of rule-based systems. Journal of Logic Programming, (11):117–132, 1991.
R. Hähnle. Automated deduction in multiple-valued logics, volume 10 of International Series of Monographs in Computer Sciences. Oxford University Press, 1993.
R. Hähnle. Short conjunctive normal forms in finitely-valued logics. Journal of Logic and Computation, 4(6):905–927, 1994.
R. Hähnle. Exploiting data dependencies in many-valued logics. Journal of Applied Non-classical Logics, (6):49–69, 1996.
R. Hahnle and G. Escalada-Imaz. Deduction in many-valued logics: A survey. Mathware and Soft Computing, 4(2):69–97, 1997.
F. Manya. Proof Procedures for Multiple-Valued Propositional Logics. PhD thesis, Universidad Autónoma de Barcelona, 1996.
N.V. Murray. Completely Non-Clausal Theorem Proving. Artificial Intelligence, 18(1):67–85, 1982.
R. Roy-Chowdhury-Dalal. Model theoretic semantics and tractable algorithm for CNF-BCP. In Proc. of the AAAI-97, pages 227–232, 1997.
Z. Stachniak. Non-clausal reasoning with propositional definite theories. In International Conferences on Artificial Intelligence and Symbolic Computation, volume 1476 of Lecture Notes in Computer Science, pages 296–307. Springer Verlag, 1998.
Z. Stachniak. Polarity guided tractable reasoning. In International American Association on Artificial Intelligence, AAAI-99, pages 751–758, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Altamirano, E., Escalada-Imaz, G. (2001). Extending Polynomiality to a Class of Non-clausal Many-Valued Horn-Like Formulas. In: Benferhat, S., Besnard, P. (eds) Symbolic and Quantitative Approaches to Reasoning with Uncertainty. ECSQARU 2001. Lecture Notes in Computer Science(), vol 2143. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44652-4_70
Download citation
DOI: https://doi.org/10.1007/3-540-44652-4_70
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42464-2
Online ISBN: 978-3-540-44652-1
eBook Packages: Springer Book Archive