Caracterización deductiva de los árboles de forzamiento semántico
Main Article Content
Keywords
tree of forcing, valuation, semantics, deductive system.
Abstract
The classic propositional calculus is characterized by a tool of visual inference called trees of semantic forcing. With this tool the associated nodes of the formula are marked, and with base in these marks it determines if the formula is valid or no. In case of invalidity, the valuation that refutes the validity of the formula is determines by the marks of the leaves in its tree of forcing. In case of validity, a formal deduction of the associated formula to the root of the tree can be constructed, this is possible because each used rule to mark the nodes in the tree is associate to a rule of inference in the deductive system.
MSC: 03BXX, 03B10
Downloads
References
[2] R. Smullyan. First order logic. New York: Dover ed., 1994.
[3] X. Caicedo. Elementos de lógica y calculabilidad. Bogotá: Universidad de los Andes, 1990.
[4] A. Hamilton. Lógica para matemáticos. Madrid: Paraninfo, 1981.
[5] M. Sierra. Árboles de forzamiento semántico. Revista Universidad EAFIT, 123, 2001.
[6] M. Sierra. Lógica básica con afirmación alterna. Ingeniería y Ciencia, 1(1), 115- 129 (2005).