Correo Electrónico
DNINFOA - SIA
Bibliotecas
Convocatorias
Identidad U.N.
Published
CARACTERIZACIÓN SEMANTICA DE LOS ÁRBOLES DE FORZAMIENTO SEMÁNTICO PARA LA LÓGICA DE PREDICADOS
SEMANTIC CHARACTERIZATION OF SEMANTIC FORCING TREES FOR PREDICATE LOGIC
DOI:
https://doi.org/10.15446/rev.fac.cienc.v13n2.110336Keywords:
Arbol de forzamiento, Semántica, predicados monádicos, valoración (es)forcing tree, monadic predicate, semantics, valuation (en)
Downloads
La semántica de modelos para la lógica de predicados monádicos de primer orden, es caracterizada por una herramienta de inferencia visual llamada árboles de forzamiento semántico para la lógica de predicados monádicos. Las fórmulas que resultan válidas (o inválidas) mediante los árboles de forzamiento semántico, coinciden con las fórmulas válidas (o inválidas) mediante la semántica de valoraciones usual. En el caso que, una fórmula sea inválida mediante un árbol de forzamiento, un modelo que la refuta está determinado por las marcas de las hojas de este árbol. Este resultado es extendido a la semántica de modelos para la lógica de predicados diádicos de primer orden con 2 variables.
Model semantics for first-order monadic predicate logic is characterized by a visual inference tool called semantic forcing trees for monadic predicate logic. Formulas that are valid (or invalid) by semantic forcing trees match valid (or invalid) formulas by the usual valuation semantics. In the event that the formula is invalid by a forcing tree, a model that refutes it is determined by the marks of the leaves of this tree. This result is extended to model semantics for first-order dyadic predicate logic with 2 variables.
References
Areces, C., Figueira, D., Gorin, D. and Mera, S. (2009). Tableaux and Model Checking for Memory Logics. In: Giese, M., Waaler, A. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. Tableaux 2009. Lecture Notes in Computer Science, 5607. Springer. Berlin.
Barrero, T. y Carnielli, W. (2005). Tableaux sin refutación. Matemáticas: Enseñanza Universitaria. 13(2), 81-99.
Beth, E. (1962). Formal methods, an introduction to symbolic logic and to the study of effective operations in arithmetic and logic. Reidel Publishing, Dordrecht, 168p.
Bílková, M., Frittella, S., Kozhemiachenko, D. (2021). Constraint Tableaux for Two-Dimensional Fuzzy Logics. In: Das, A., Negri, S. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. Tableaux 2021. Lecture Notes in Computer Science, 12842. Springer, Cham.
Börger, E., Erich Grädel, E. and Gurevich, Y. (1997). The Classical Decision Problem. Springer-Verlag Berlin.
Britz, K. and VarzincZak, I. (2019). Reasoning with Contextual Defeasible ALC. Description Logics, 2373, paper 8.
Caicedo, X. (1990). Elementos de lógica y calculabilidad. Bogotá: Una empresa docente.
Carnielli, W. (1987). Systematization of finite many-valued logics through the method of tableaux. The Journal of Symbolic Logic. 52(2), 473-493.
Cassano, V., Pombo, C.G.L., Maibaum, T.S.E. (2015). A Propositional Tableaux Based Proof Calculus for Reasoning with Default Rules. In: De Nivelle, H. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. Tableaux 2015. Lecture Notes in Computer Science, 9323. Springer, Cham.
Church, A. (1936). A Note on the Entscheidungs problem. The Journal of Symbolic Logic. 1(1), 40-41.
Ferguson, T.M. (2021). Tableaux and Restricted Quantification for Systems Related to Weak Kleene Logic. In: Das, A., Negri, S. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2021. Lecture Notes in Computer Science, 12842. Springer, Cham.
Grätz, L. (2021). Analytic Tableaux for Non-deterministic Semantics. In: Das, A., Negri, S. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2021. Lecture Notes in Computer Science, 12842. Springer, Cham.
Grimaldi, R. (1998). Matemáticas discreta y combinatoria. México: Pearson Educación.
Hammer, E. (1996). Logic and visual information. Stanford University: Center for the Study of Linguistics and Information.
Henkin, L. (1949). The Completeness of the First-Order Functional Calculus. The Journal of Symbolic Logic. 14(3), 159-166.
Indrzejczak, A., Zawidzki, M. (2021). Tableaux for Free Logics with Descriptions. In: Das, A., Negri, S. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2021. Lecture Notes in Computer Science, 12842. Springer, Cham.
Lowenheim, L. (1915). Über Moglichkeiten im Relativkalkül. Mathematische Annalen. 76, 447-471.
Smullyan, R. (1968). First order logic. Springer-Verlag, Berlin, 158p.
Sierra, M. (2001). Árboles de forzamiento semántico. Revista Universidad EAFIT. 37(123), 53-72.
Sierra, M. (2006). Caracterización deductiva de los árboles de forzamiento semántico. Revista Ingeniería y Ciencia. 2(3), 73-102.
Sierra, M. (2010). Argumentación deductiva con diagramas y árboles de forzamiento. Fondo Editorial Universidad EAFIT.
Sierra, M. (2017). Árboles de forzamiento semántico para operaciones entre conjuntos. Revista Facultad de Ciencias Básicas. 13(2), 72-82.
Sierra, M. (2019). Árboles de forzamiento semántico para la semántica de sociedades abiertas. Revista Facultad De Ciencias Básicas, 14(2), 91–99.
Van Dalen, D. (2004). Logic and Structure. Springer-Verlag Berlin Heidelberg.
Venn, J. (1880). On the Diagrammatic and Mechanical Representation of Propositions and Reasonings. The London, Edinburgh, and Dublin Philosophical Magazine and Journal of Science. 10(59), 1-18.
How to Cite
APA
ACM
ACS
ABNT
Chicago
Harvard
IEEE
MLA
Turabian
Vancouver
Download Citation
License
Copyright (c) 2024 Revista de la Facultad de Ciencias
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
The authors or copyright holders of each paper confer to the Journal of the Faculty of Sciences of Universidad Nacional de Colombia a non-exclusive, limited and free authorization on the paper that, once evaluated and approved, is sent for its subsequent publication in accordance with the following characteristics:
- The corrected version is sent according to the suggestions of the evaluators and it is clarified that the paper mentioned is an unpublished document on which the rights are authorized and full responsibility is assumed for the content of the work before both the Journal of the Faculty of Sciences, Universidad Nacional de Colombia and third parties.
- The authorization granted to the Journal will be in force from the date it is included in the respective volume and number of the Journal of the Faculty of Sciences in the Open Journal Systems and on the Journal’s home page (https://revistas.unal.edu.co/index.php/rfc/index), as well as in the different databases and data indexes in which the publication is indexed.
- The authors authorize the Journal of the Faculty of Sciences of Universidad Nacional de Colombia to publish the document in the format in which it is required (printed, digital, electronic or any other known or to be known) and authorize the Journal of the Faculty of Sciences to include the work in the indexes and search engines deemed necessary to promote its diffusion.
- The authors accept that the authorization is given free of charge, and therefore they waive any right to receive any emolument for the publication, distribution, public communication, and any other use made under the terms of this authorization.
- All the contents of the Journal of the Faculty of Sciences are published under the Creative Commons Attribution – Non-commercial – Without Derivative 4.0.License
MODEL LETTER OF PRESENTATION and TRANSFER OF COPYRIGHTS
Personal data processing policy
The names and email addresses entered in this Journal will be used exclusively for the purposes set out in it and will not be provided to third parties or used for other purposes.
