Show simple item record

PhD Thesis

dc.contributor.advisorMartín Mateos, Francisco Jesúses
dc.contributor.advisorAlonso Jiménez, José Antonioes
dc.creatorSerrano Suárez, Fabián Fernandoes
dc.date.accessioned2017-04-19T06:32:55Z
dc.date.available2017-04-19T06:32:55Z
dc.date.issued2012-06-12
dc.identifier.citationSerrano Suárez, F.F. (2012). Formalización en Isar de la metalógica de primer orden. (Tesis Doctoral Inédita). Universidad de Sevilla, Sevilla.
dc.identifier.urihttp://hdl.handle.net/11441/57780
dc.descriptionTesis descargada desde internet: https://www.cs.us.es/~jalonso/trabajos_dirigidos/2012-tesis-FFS.pdfes
dc.description.abstractEl objetivo del trabajo es formalizar razonamiento complejo de forma legible por los humanos y procesable por las máquinas. Más precisamente, formalizar en el sistema de razonamiento Isabelle/HOL/Isar la metateoría de la lógica de primer orden como se expone en capítulo 1 del libro "Introduction to mathematical logic" de Elliott Mendelson y en los primeros cinco capítulos del libro "First-Order Logic and Automated Theorem Proving" de M. Fitting. 1) Se presenta una formalización de un sistema axiomático de la lógica proposicional y la demostración de la completitud del sistema usando el método de Kalmar de eliminación de variables. 2) Se presenta una formalización de la terminación y corrección de un algoritmo para calcular una forma normal conjuntiva de una fórmula proposicional. El algoritmo está descrito en términos de la notación uniforme para las fórmulas de la lógica proposicional; para demostrar su terminación se define una función de medida en términos de los conceptos de "multiconjunto" y "rango" de una fórmula. 3) Se formaliza la corrección de un procedimiento de prueba de tautologías usando tableros semánticos. La terminación se demuestra de la misma forma que en el caso del algoritmo de la forma normal conjuntiva. Para la formalización de la completitud de este método de prueba se utiliza el lemma de Hintikka. 4) Se formaliza la demostración del teorema de existencia de modelos para un conjunto consistente S de fórmulas pertenecientes a un lenguaje proposicional L. Esta demostración está basada en extender S a un conjunto consistente maximal M el cual resulta ser satisfacible (por ser un conjunto de Hintikka) y por tanto S también. Como una aplicación del teorema de existencia de modelos en la lógica proposicional, se formalizan el teorema de compacidad y el teorema de interpolación de Craig. 6) Se presenta la formalización de la sintaxis y semántica de la lógica de primer orden. Para la representación de las fórmulas se emplea la notación de de Bruijn y se formaliza el teorema de existencia de modelos en la lógica de primer orden siguiendo el mismo orden de ideas que en el caso proposicional, y como una aplicación se formaliza la demostracion del teorema de Löwenheim-Skolem. 7) Por último, se define un sistema de deducción natural para lo lógica de primer orden. Se formaliza su corrección y como una consecuencia del teorema de existencia de modelos para la lógica de primer orden, se formaliza su completitud.es
dc.formatapplication/pdfes
dc.language.isospaes
dc.rightsAttribution-NonCommercial-NoDerivatives 4.0 Internacional*
dc.rights.urihttp://creativecommons.org/licenses/by-nc-nd/4.0/*
dc.subjectTeoría de la demostraciónes
dc.titleFormalización en Isar de la metalógica de primer ordenes
dc.typeinfo:eu-repo/semantics/doctoralThesises
dcterms.identifierhttps://ror.org/03yxnpp24
dc.type.versioninfo:eu-repo/semantics/publishedVersiones
dc.rights.accessRightsinfo:eu-repo/semantics/openAccesses
dc.contributor.affiliationUniversidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificiales
idus.format.extent358 p.es

FilesSizeFormatViewDescription
2012-tesis-FFS.pdf1.297MbIcon   [PDF] View/Open  

This item appears in the following collection(s)

Show simple item record

Attribution-NonCommercial-NoDerivatives 4.0 Internacional
Except where otherwise noted, this item's license is described as: Attribution-NonCommercial-NoDerivatives 4.0 Internacional