La lógica proposicional es un sistema formal que nos proporciona la capacidad de examinar y analizar enunciados a través de reglas y principios claramente definidos. El objetivo principal de este trabajo es comprender y analizar el método de resolución, una técnica sintáctica que nos permite demostrar la insatisfactibilidad de conjuntos de fórmulas en la lógica proposicional. A lo largo de los distintos capítulos, llevaremos a cabo un análisis de la sintaxis, semántica y formas normales en la lógica proposicional, estableciéndolas como bases fundamentales para abordar el método de resolución de manera rigurosa y probar su corrección y completitud.
Propositional logic is a formal system that allows to examine and analyze statements through well-defined rules and principles. The main objective of this dissertation is to understand and analyze the resolution method, a syntactic technique that allows us to demonstrate the unsatisfiability of sets of formulas in propositional logic. Throughout the different chapters, we will conduct an analysis of the syntax, semantics and normal forms in propositional logic, establishing them as fundamental foundations to rigorously approach the resolution method and prove its correctness and completeness.
