Estoy buscando una buena fuente introductoria al cálculo sequent adecuado para alguien que ha estudiado la deducción natural antes. Libros y recursos en línea son ambos aceptables, como se explicaron cada regla de inferencia y cualquier convenio notacional. Gracias.
Respuestas
¿Demasiados anuncios?
dStulle
Puntos
28
Puede leer el capítulo sobre el cálculo Sequent del manuscrito de Frank Pfenning en Automatizado teorema demostrando. Este capítulo se construye hacia una explicación del cálculo sequent por medio de su relación con la deducción natural.
Sekhat
Puntos
2555
De Girard pruebas y tipos contiene una buena introducción a esta materia. Es una traducción al inglés por Paul Taylor y Yves Lafont disponible en línea gratuitos. También como Negri y van Platón Teoría estructural de la prueba y han escuchado cosas buenas sobre Troelstra y de Schwichtenberg Teoría básica de la prueba.
David Sykes
Puntos
3027
Gentzen, 1934, "Investigaciones en la Deducción Lógica' — Esto es muy legible, y presenta muchas ideas que más tarde sintético funciona invariablemente faltar algunos. Si vas en serio, este, y algunos otros papeles de Gentzen, son indispensables.
Stan Wainer ha escrito algunos de los excelentes textos introductorios. No creo que están libremente disponibles para su descarga, aunque los archivos Pdf son el lavado de aquí y de allí. Wainer, 1997, Básicas de la Prueba de la Teoría con Aplicaciones a la Computación', en Schwichtenberg, la Lógica de la Computación, Springer Verlag, lo recomiendo encarecidamente.
Pero el mejor punto de partida es, probablemente, Pruebas y Tipos, según lo recomendado por Neel, la lectura de, al menos, hasta la prueba de corte de eliminación. Una advertencia: Girard su estilo es un poco resbaladiza, y es común que los estudiantes dicen que la han leído, que han absorbido las opiniones, pero poco de los resultados.
Postscript — Si usted se preocupa por la multa de tecnicismos de la coincidencia de las normales de las pruebas natural deducciones con el corte libre de pruebas en el secuente cálculo, Ungar, 1992 Normalización, corte de eliminación, y la teoría de las pruebas es un buen texto, generosamente hizo libremente disponible como parte de la universidad de Stanford Pensamiento Medieval y Moderno Proyecto de Digitalización. Esta literatura es un poco complicado, ya que las dos pruebas cálculos son formulados, y sus metatheory han llegado en un poco diferente manera. La literatura no se remontan a Gentzen, excepto para el trivial medida en que los dos cálculos se muestran los equivalentes fuerza expresiva, porque la teoría de la normalización para deducción natural no era fijo untilo Prawitz, 1965, Deducción Natural.
Joe
Puntos
46
Recomiendo lectura "Cinco conferencias sobre análisis de prueba" de Sara Negri que usted puede encontrar aquí http://www.helsinki.fi/~negri/prana.pdf. En la primera Conferencia trata de obtener el siguiente cálculo de deducción natural muy naturalmente (por supuesto, haciendo hipótesis explícitas).
Evan Anderson
Puntos
118832
Si usted está buscando una fuente en basic sequent cálculo, tanto proposicional y la lógica de primer orden---por que me refiero a las definiciones, explicaciones y teoremas fundamentales (como el corte de eliminación), y todo esto desarrollado desde cero y en una muy legible, con todas las anotaciones explicó---me gustaría recomendar el libro de Cook y Nguyen, Fundamentos Lógicos de la Prueba de la Complejidad (2010, Cambridge University Press, ASL Perspectivas en la Lógica).
Un borrador en línea (que es casi idéntica a la del libro) es aquí.
Lo que usted necesita para leer es sólo el Capítulo 2:
El Predicado de Cálculo y el Sistema LC: Cálculo proposicional, Gentzen del proposicional sistema a prueba de PK, La solidez y la integridad de PK, PK pruebas de hipótesis, Proposicional compacidad, Predicado de cálculo, La sintaxis de los predicados de cálculo, La semántica del predicado de cálculo, El primer orden de la prueba del sistema LC, Libre de la variable de forma normal, La integridad de la LC, sin igualdad, Igualdad de axiomas, Igualdad de axiomas para la LC, Revisado por la solidez y la integridad de la LC, Las principales consecuencias de la integridad, El Teorema De Herbrand.
