En lógica matemática , las pruebas focalizadas son una familia de pruebas analíticas que surgen a través de la búsqueda de pruebas dirigida a un objetivo, y son un tema de estudio en la teoría de pruebas estructurales y la lógica reductiva. Forman la definición más general de la búsqueda de pruebas dirigida a un objetivo , en la que alguien elige una fórmula y realiza reducciones hereditarias hasta que el resultado cumple alguna condición. El caso extremo en el que la reducción solo termina cuando se alcanzan los axiomas forma la subfamilia de pruebas uniformes . [1]
Se dice que un cálculo secuencial tiene la propiedad de enfoque cuando las pruebas enfocadas están completas para alguna condición de terminación. Para el Sistema LK , el Sistema LJ y el Sistema LL, las pruebas uniformes son pruebas enfocadas donde a todos los átomos se les asigna polaridad negativa. [2] Se ha demostrado que muchos otros cálculos secuenciales tienen la propiedad de enfoque, en particular los cálculos secuenciales anidados de las variantes clásica e intuicionista de las lógicas modales en el cubo S5 . [3] [4]
En el cálculo secuencial para una lógica intuicionista , las pruebas uniformes pueden caracterizarse como aquellas en las que la lectura ascendente realiza todas las reglas de la derecha antes que las de la izquierda. Normalmente, las pruebas uniformes no están completas para la lógica, es decir, no todas las secuencias o fórmulas demostrables admiten una prueba uniforme, por lo que se consideran fragmentos donde están completos, por ejemplo, el fragmento hereditario de Harrop de la lógica intuicionista . Debido al comportamiento determinista, la búsqueda de pruebas uniformes se ha utilizado como el mecanismo de control que define el paradigma del lenguaje de programación de la programación lógica . [1] Ocasionalmente, la búsqueda de pruebas uniformes se implementa en una variante del cálculo secuencial para la lógica dada donde la gestión del contexto es automática, aumentando así el fragmento para el que se puede definir un lenguaje de programación lógica. [5]
El principio de enfoque se clasificó originalmente a través de la desambiguación entre conectivos sincrónicos y asincrónicos en lógica lineal , es decir, conectivos que interactúan con el contexto y aquellos que no, como consecuencia de la investigación sobre programación lógica . Ahora son un ejemplo cada vez más importante de control en lógica reductiva y pueden mejorar drásticamente los procedimientos de búsqueda de pruebas en la industria. La idea esencial del enfoque es identificar y fusionar las opciones no deterministas en una prueba, de modo que una prueba pueda verse como una alternancia de fases negativas (donde las reglas invertibles se aplican con entusiasmo) y fases positivas (donde las aplicaciones de las otras reglas están confinadas y controladas). [3]
Según las reglas del cálculo secuencial, las fórmulas se clasifican canónicamente en una de dos clases llamadas positivas y negativas ; por ejemplo, en LK y LJ la fórmula es positiva. La única libertad es sobre los átomos, a los que se les asigna una polaridad libremente. Para las fórmulas negativas, la demostrabilidad es invariante bajo la aplicación de una regla derecha; y, dualmente, para las fórmulas positivas la demostrabilidad es invariante bajo la aplicación de una regla izquierda. En cualquier caso, se pueden aplicar con seguridad las reglas en cualquier orden a las subfórmulas hereditarias de la misma polaridad.
En el caso de una regla derecha aplicada a una fórmula positiva, o una regla izquierda aplicada a una fórmula negativa, se pueden obtener consecuentes inválidos; por ejemplo, en LK y LJ no hay prueba de que el consecuente comience con una regla derecha. Un cálculo admite el principio de enfoque si, cuando un reducto original era demostrable, entonces los reductos hereditarios de la misma polaridad también lo son. Es decir, uno puede comprometerse a centrarse en la descomposición de una fórmula y sus subfórmulas de la misma polaridad sin pérdida de completitud.
A menudo se demuestra que un cálculo secuencial tiene la propiedad de enfoque al trabajar en un cálculo relacionado donde la polaridad controla explícitamente qué reglas se aplican. Las demostraciones en tales sistemas se encuentran en fases enfocadas, no enfocadas o neutrales, donde las dos primeras se caracterizan por la descomposición hereditaria; y la última por forzar una elección de enfoque. Uno de los comportamientos operativos más importantes que puede experimentar un procedimiento es el retroceso , es decir, volver a una etapa anterior en el cálculo donde se hizo una elección. En sistemas enfocados para la lógica clásica e intuicionista, el uso del retroceso se puede simular mediante pseudocontracción.
Sea y denoten cambio de polaridad, el primero haciendo que una fórmula sea negativa, y el segundo positiva; y llamemos neutra a una fórmula con una flecha. Recordemos que es positivo, y consideremos el consecuente polarizado neutro , que se interpreta como el consecuente real . Para consecuentes neutros como este, el sistema enfocado obliga a uno a hacer una elección explícita de en qué fórmula enfocarse, denotada por . Para realizar una búsqueda de pruebas lo mejor es elegir la fórmula de la izquierda, ya que es positivo, de hecho (como se discutió anteriormente) en algunos casos no hay pruebas donde el enfoque esté en la fórmula de la derecha. Para superar esto, algunos cálculos enfocados crean un punto de retroceso tal que enfocarse en la derecha produce , que todavía es como . La segunda fórmula de la derecha puede eliminarse solo cuando la fase enfocada ha terminado, pero si la búsqueda de pruebas se atasca antes de que esto suceda, el consecuente puede eliminar el componente enfocado y así regresar a la elección, por ejemplo, debe tomarse como ya que no se puede hacer ninguna otra inferencia reductiva. Esta es una pseudocontracción ya que tiene la forma sintáctica de una contracción a la derecha, pero la fórmula real no existe, es decir, en la interpretación de la prueba en el sistema enfocado, el consecuente solo tiene una fórmula a la derecha.
