Deductive characterization of semantic forcing trees
The classic propositional calculus is characterized by a visual inference tool called semantic forcing trees. With this tool the nodes of the tree associated with a given formula are marked, and based on these marks it is determined whether the formula is valid or not. In case of disability, the val...
- Autores:
-
Sierra A., Manuel
- Tipo de recurso:
- Fecha de publicación:
- 2006
- Institución:
- Universidad EAFIT
- Repositorio:
- Repositorio EAFIT
- Idioma:
- spa
- OAI Identifier:
- oai:repository.eafit.edu.co:10784/14564
- Acceso en línea:
- http://hdl.handle.net/10784/14564
- Palabra clave:
- Forcing Tree
Valuation
Semantics
Deductive System
Árbol De Forzamiento
Valuación
Semántica
Sistema Deductivo
- Rights
- License
- Copyright (c) 2006 Manuel Sierra A.
Summary: | The classic propositional calculus is characterized by a visual inference tool called semantic forcing trees. With this tool the nodes of the tree associated with a given formula are marked, and based on these marks it is determined whether the formula is valid or not. In case of disability, the valuation that refutes the validity of the formula is determined by the marks of the leaves in its forcing tree. In case of validity, a formal deduction of the formula associated with the root of the tree can be constructed; This is achieved because each rule used to mark the nodes in the tree is associated with an inference rule in the deductive system. |
---|