DOI:
https://doi.org/10.14483/2322939X.4119Publicado:
2013-07-09Número:
Vol. 4 Núm. 2 (2008)Sección:
Investigación y DesarrolloFÓRMULAS CON SIGNO
Palabras clave:
Multi-valuable logic, SAT, Davis and Putnam, multivaluable formulas, regular formula. (es).Descargas
Resumen (es)
En este artículo, se hace una descripción breve del problema SAT signado (SAT Signed). Las fórmulas signadas son un lenguaje para la representación del conocimiento [1], que se encuentra ubicado en la intersección de propagación de restricciones (CP), Lógica multivaluada (MVL) y programación lógica annotated (ALP).
Una fórmula normal conjuntiva con signo (FNC Signada) está compuesta por; la conjunción de cláusulas disyuntivas con signo. Cada cláusula contiene literales con signo. Una literal, es llamada un átomo signado, el cual es una expresión de la forma S:p, donde p es un átomo clásico y S es su signo, el cual se compone de un subconjunto de dominio N.
Las aplicaciones para deducir en lógica con signo se derivan de la programación lógica anotada (eje, bases de datos deductivas), satisfacción de restricciones (eje, problema de scheduling) y lógica multivaluada (eje, procesamiento del lenguaje natural). El papel fundamental de esta lógica justifi ca el estudio de algoritmos y problemas SAT asociados.
Referencias
Bernhard Beckert, Reiner Hahnle, and Felip Manya. The 2-Sat Problem of Regular
Signed CNF Formulas. In Proceedings, IEEE 30th International Symposiumon Multiple-Valued Logics, pages 331-336. IEEE Press, 2000.
Bernhard Beckert , Reiner Hahnle, and Felip Manyá. The SAT Problem of Signed
CMF Formulas. Pages 59-80,200.
Bernhard Beckert, Reiner Hahnle, and Felip Manyá. Transformations between Signed and Classical Clause Logic. In In Proceedings, 29th International Symposium on Multiple-Valued Logics (ISMVL), pages 248-255. IEEE Press, 1999.
Reiner Hahnle Bernhard Beckert and Felip Many´a. On the Regular 2-SAT Problem. University of Karlsruhe, Dept. of Computer Science. Available at ftp://sonja.ira.uka.de/pub/beckert/Regular 2SAT.ps.gz, 1999.
M. Davis, G. Logemann, and D. Loveland. A Machine Program for Theorem Proving. Comunnications of the ACM, 5:394–397, 1962.
W.F. Dowling and J.H. Gallier. Linear-time algorithms for testing the satisfiability of horn propositional formulae. Journal of Logic Programming, 3:267–284, 1984.
Gonzalo Escalada-Imaz and Felip Manya. The Satisfiability Problem for Multiple- Valued Horn Formulae. In Proceedings, International Symposium The SAT Problem of Signed CNF Formulas 21 on Multiple-Valued Logics(ISMVL), pages 250-256, 1994.
Reiner Hahnle. Exploiting Data Dependencies Inmany-Valued Logics. Journal of Applied Non-Classical Logics, pages 49-69, 1996.
REINERH˜DHNLE. Short Conjunctive Normal Forms in finitely Valued Logics. Journal of Logic and Computation, 1994.
Felip Manyá. Proof Procedures Formultiple-Valued Propositional Logcs. Monografi es de LSInstitud dSInvertigacit’o en Inter.lig’encia Artificial.
Felip Manyá. The 2-SAT Problem in Signd CNF Formulas. Multiple-Values Logic. An International Journal, 1999.
A. Itai S. Even and A. Shamir. On the Complexity of Timetable and Multicommodity
flow Problems. SIAM Journal of Computing, pages 691-703, 76.
S.A.Cook. The Complexity of Theorem-Proving Procedures. In In Proceedings of the Third ACM Symposium on theory of Computing, pages 151-158, 1971.
Viorica Sofronie-Stokkermans. On Translation of finitely-Valued Logics to Classical
first-Order Logic. page pages 410-411, 1998.
2.png)
