El cálculo circular es un cálculo de prueba que manipula construcciones de estilo gráfico denominadas cirquents , a diferencia de los objetos tradicionales de estilo árbol, como fórmulas o secuencias . Los círculos vienen en una variedad de formas, pero todos comparten un rasgo característico principal, lo que los hace diferentes de los objetos más tradicionales de manipulación sintáctica. Esta característica es la capacidad de explicar explícitamente la posibilidad de compartir subcomponentes entre diferentes componentes. Por ejemplo, es posible escribir una expresión donde dos subexpresiones F y E , mientras que ninguna es una subexpresión de la otra, todavía tienen una ocurrencia común de una subexpresión G(a diferencia de tener dos apariciones diferentes de G , una en F y otra en E ).
Descripción general
El enfoque fue introducido por G. Japaridze en [1] como una teoría de prueba alternativa capaz de "domesticar" varios fragmentos no triviales de su lógica de computabilidad , que de otra manera se había resistido a todos los intentos de axiomatización dentro de los marcos tradicionales de la teoría de la prueba. [2] [3] El origen del término "cirquent" es CIRcuit + seQUENT, ya que la forma más simple de cirquents, aunque se asemeja a circuitos en lugar de fórmulas, se puede considerar como colecciones de secuencias unilaterales (por ejemplo, secuencias de un nivel dado de un árbol de prueba de estilo Gentzen) donde algunos secuentes pueden tener elementos compartidos.
La versión básica del cálculo circular en [4] fue acompañada de una " semántica de recursos abstractos " y la afirmación de que esta última era una formalización adecuada de la filosofía de recursos tradicionalmente asociada con la lógica lineal . Basándose en esa afirmación y en el hecho de que la semántica inducía una lógica propiamente más fuerte que la lógica lineal (afín), Japaridze argumentó que la lógica lineal era incompleta como lógica de recursos. Además, argumentó que no solo el poder deductivo, sino también el poder expresivo de la lógica lineal era débil, ya que, a diferencia del cálculo circular, no logró capturar el fenómeno omnipresente de compartir recursos. [5]
La filosofía de los recursos del cálculo circular ve los enfoques de la lógica lineal y la lógica clásica como dos extremos: el primero no permite compartir en absoluto, mientras que en el segundo “todo es compartido que se puede compartir”. A diferencia del cálculo circular, ninguno de los enfoques permite casos mixtos en los que se comparten algunas subfórmulas idénticas y otras no.
Entre las aplicaciones más tarde encontradas del cálculo circular estaba su uso para definir una semántica para una lógica puramente proposicional favorable a la independencia . [6] La lógica correspondiente fue axiomatizada por W. Xu. [7]
Sintácticamente, los cálculos circulares son sistemas de inferencia profundos con la característica única de compartir subfórmulas. Se ha demostrado que esta función aumenta la velocidad de ciertas pruebas. Por ejemplo, se han construido pruebas analíticas de tamaño polinómico para el casillero proposicional. [8] Sólo se han encontrado pruebas analíticas cuasipolinomiales para este principio en otros sistemas de inferencia profunda. [9] En los sistemas de resolución o analíticos de estilo Gentzen, se sabe que el principio de casillero solo tiene pruebas de tamaño exponencial. [10]
Referencias
- ^ G.Japaridze, " Introducción al cálculo circular y semántica de recursos abstractos ". Journal of Logic and Computation 16 (2006), págs. 489–532.
- ^ G.Japaridze, " La domesticación de las recurrencias en la lógica de la computabilidad a través del cálculo circular, Parte I ". Archive for Mathematical Logic 52 (2013), páginas 173-212.
- ^ G.Japaridze, "La domesticación de las recurrencias en la lógica de la computabilidad a través del cálculo circular, Parte II " Archivo de lógica matemática 52 (2013), páginas 213-259.
- ^ G.Japaridze, " Introducción al cálculo circular y semántica de recursos abstractos ". Journal of Logic and Computation 16 (2006), págs. 489–532.
- ^ G.Japaridze, " Cirquent calculus profundized [ enlace muerto ] ". Journal of Logic and Computation 18 (2008), págs. 983–1028.
- ^ G.Japaridze, " De fórmulas a cirquents en lógica de computabilidad ". Logical Methods es Computer Science 7 (2011), Número 2, Documento 1, págs. 1-55.
- ^ W.Xu, " Un sistema proposicional inducido por el enfoque de Japaridze a la lógica IF [ enlace muerto ] ". Logic Journal of the IGPL 22 (2014), páginas 982–991.
- ^ G.Japaridze, " Cirquent calculus profundized [ enlace muerto ] ". Journal of Logic and Computation 18 (2008), págs. 983–1028.
- ^ A. Das, " En el casillero y principios relacionados en la inferencia profunda y los sistemas monótonos ".
- ^ A. Haken, " La intratabilidad de la resolución ". Theoretical Computer Science 39 (1985), págs. 297-308.
Literatura
- M. Bauer, “ La complejidad computacional del cálculo circular proposicional ”. Métodos lógicos en ciencias de la computación 11 (2015), Número 1, Documento 12, págs. 1-16.
- G.Japaridze, “ Introducción al cálculo circular y semántica de recursos abstractos ”. Journal of Logic and Computation 16 (2006), págs. 489–532.
- G.Japaridze, " Cirquent calculus profundized [ enlace muerto ] ". Journal of Logic and Computation 18 (2008), págs. 983–1028.
- G.Japaridze, “ De fórmulas a cirquents en lógica de computabilidad ”. Métodos lógicos en ciencias de la computación 7 (2011), Número 2, Documento 1, págs. 1-55.
- G.Japaridze, “ La domesticación de las recurrencias en la lógica de la computabilidad a través del cálculo circular, Parte I ”. Archivo de Lógica matemática 52 (2013), páginas 173–212.
- G.Japaridze, “La domesticación de las recurrencias en la lógica de la computabilidad a través del cálculo circular, Parte II ” Archivo de lógica matemática 52 (2013), páginas 213–259.
- I. Mezhirov y N. Vereshchagin, Sobre semántica de recursos abstractos y lógica de computabilidad . Journal of Computer and System Sciences 76 (2010), págs. 356–372.
- W.Xu y S.Liu, “ Solidez e integridad del sistema de cálculo circular CL6 para lógica de computabilidad [punto muerto ] ”. Logic Journal of the IGPL 20 (2012), págs. 317–330.
- W.Xu y S.Liu, “ Sistema de cálculo circular CL8S versus sistema de cálculo de estructuras SKSg para lógica proposicional ”. En: Lógica cuantitativa y Soft Computing. Guojun Wang, Bin Zhao y Yongming Li, eds. Singapur, World Scientific, 2012, págs. 144–149.
- W.Xu, " Un sistema proposicional inducido por el enfoque de Japaridze a la lógica IF [ enlace muerto ] ". Logic Journal of the IGPL 22 (2014), páginas 982–991.
- W. Xu, Un sistema de cálculo circular con agrupamiento y clasificación . Revista de lógica aplicada 16 (2016), págs. 37-49.
enlaces externos
- Medios relacionados con el cálculo circular en Wikimedia Commons