Trabajo Fin de Grado
Elementos de lógica formalizados en Isabelle/HOL
Autor/es | Santiago Fernández, Sofía |
Director | Alonso Jiménez, José Antonio
Hidalgo Doblado, María José |
Departamento | Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial |
Fecha de publicación | 2020 |
Fecha de depósito | 2021-07-06 |
Titulación | Universidad de Sevilla. Grado en Matemáticas |
Resumen | El objetivo de la Lógica es la formalización del conocimiento y su razonamiento. En
este trabajo, estudiaremos elementos de la lógica proposicional desde la perspectiva
teórica de First−Order Logic and Automated Theorem ... El objetivo de la Lógica es la formalización del conocimiento y su razonamiento. En este trabajo, estudiaremos elementos de la lógica proposicional desde la perspectiva teórica de First−Order Logic and Automated Theorem Proving [4] de Melvin Fitting. En particular, nos centraremos en la sintaxis y la semántica, concluyendo con la versión proposicional del lema de Hintikka sobre la satisfacibilidad de una clase determinada de conjuntos de formulas. Siguiendo la inspiración de Propositional Proof Systems [10] por Julius Michaelis y Tobias Nipkow, los resultados expuestos serán formalizados me- diante Isabelle: un demostrador interactivo que incluye herramientas de razonamiento automático para guiar al usuario en el proceso de formalización, verificación y automa- tización de resultados. Concretamente, Isabelle/HOL es una especialización de Isabelle para la lógica de orden superior. Las demostraciones de los resultados en Isabelle/HOL se elaboraran siguiendo dos tácticas distintas a lo largo del trabajo. En primer lugar, cada lema será probado de manera detallada prescindiendo de toda herramienta de ra- zonamiento automático, como resultado de una búsqueda inversa en cada paso de la prueba. En contraposición, elaboraremos una demostración automática alternativa de cada resultado que utilice todas las herramientas de razonamiento automático que pro- porciona el demostrador. De este modo, se evidenciara la capacidad de razonamiento automático de Isabelle. Logic’s purpose is about knowledge’s formalisation and its reasoning. In this project, we will approach Propositional Logic’s elements from the theoretical perspective of First−Order Logic and Automated Theorem Proving ... Logic’s purpose is about knowledge’s formalisation and its reasoning. In this project, we will approach Propositional Logic’s elements from the theoretical perspective of First−Order Logic and Automated Theorem Proving [4] by Melvin Fitting. We will focus on the study of Syntax and Semantics to reach propositional version of Hintikka’s lemma, which determinate the satisfiability of a concrete type of formula set. Inspired by Propositional Proof Systems [10] by Julius Michaelis and Tobias Nipkow, these results will be formalised using Isabelle: a proof assistant including automatic reasoning tools to guide the user on formalising, verifying and automating results. In particular, Isabelle/HOL is the specialization of Isabelle for High-Order Logic. The processing of the results formalised in Isabelle/HOL follows two directions. In the first place, each lemma will be proved on detail without any automation, as the result of an inverse research on every step of the demonstration until it is only completed with deductions based on elementary rules and definitions. Conversely, we will alternatively prove the results using all the automatic reasoning tools that are provide by the proof assistant. In this way, Isabelle’s power of automatic reasoning will be shown as the contrast between these two different proving tactics. |
Cita | Santiago Fernández, S. (2020). Elementos de lógica formalizados en Isabelle/HOL. (Trabajo Fin de Grado Inédito). Universidad de Sevilla, Sevilla. |
Ficheros | Tamaño | Formato | Ver | Descripción |
---|---|---|---|---|
GM Santiago Fernández, Sofia.pdf | 507.9Kb | [PDF] | Ver/ | |