Admisibilidad de la Regla de Sustitución en Sistemas de Prueba Cíclica

Información Básica

• ID del Artículo: 2510.14749
• Título: Admisibilidad de la Regla de Sustitución en Sistemas de Prueba Cíclica
• Autores: Kenji Saotome, Koji Nakazawa (Universidad de Nagoya)
• Clasificación: cs.LO (Lógica)
• Fecha de Publicación: 16 de octubre de 2025
• Enlace del Artículo: https://arxiv.org/abs/2510.14749

Resumen

Este artículo investiga la cuestión de la admisibilidad de la regla de sustitución en sistemas de prueba cíclica. La regla de sustitución complica el análisis teórico e incrementa el costo computacional de la búsqueda de pruebas, ya que cada secuente puede ser la conclusión de una instancia de la regla de sustitución; por lo tanto, la admisibilidad es deseable tanto desde perspectivas teóricas como prácticas. Aunque en sistemas no cíclicos la admisibilidad se demuestra típicamente mediante transformaciones de prueba locales, tales transformaciones pueden destruir la estructura cíclica y no pueden aplicarse directamente. Investigaciones previas sugieren que la regla de sustitución probablemente no es admisible en CLKIDω, el sistema de prueba cíclica de lógica de primer orden con predicados inductivos. Este artículo demuestra que en presencia de la regla de corte, la regla de sustitución es admisible en CLKIDω. Nuestro enfoque consiste en desplegar pruebas cíclicas en formas infinitas, elevar la regla de sustitución y luego reintroducir aristas para construir pruebas cíclicas sin la regla de sustitución. Si se restringe la sustitución para no introducir símbolos de función, el resultado se extiende a una clase más amplia de sistemas, incluyendo CLKIDω sin corte y sistemas de prueba cíclica para lógica de separación.

Contexto de Investigación y Motivación

Definición del Problema

Las pruebas cíclicas son extensiones de árboles de prueba tradicionales que introducen estructuras cíclicas para razonar sobre predicados definidos inductivamente. La regla de sustitución $\frac{\Gamma \vdash \Delta}{\Gamma[\theta] \vdash \Delta[\theta]}$ (Subst) se introduce en muchos sistemas de prueba cíclica para ayudar en la construcción de estructuras cíclicas.

Importancia del Problema

1. Perspectiva Teórica: La regla de sustitución siempre es aplicable, lo que complica el análisis de pruebas
2. Perspectiva Práctica: La aplicación sin restricciones de la regla de sustitución incrementa el costo computacional, ya que muchas sustituciones pueden aplicarse en cada paso

Limitaciones de Métodos Existentes

En sistemas de prueba no cíclicos, la admisibilidad de la regla de sustitución se logra típicamente en dos fases:

1. Fase de Elevación: Mover la regla de sustitución hacia arriba
2. Fase de Eliminación: Eliminar la regla de sustitución en los axiomas

Sin embargo, en sistemas de prueba cíclica, este enfoque enfrenta dificultades fundamentales:

• La fase de elevación puede destruir la relación brote-compañero (bud-companion relationship)
• La fase de eliminación no puede eliminar la sustitución en los brotes

Motivación de la Investigación

Brotherston 1 planteó la pregunta de si la regla de sustitución es admisible en CLKIDω, sugiriendo que en el caso general, al menos en configuraciones sin corte, probablemente no sea admisible. Este artículo tiene como objetivo resolver este problema abierto.

Contribuciones Principales

1. Resultado Teórico Principal: Demuestra que en presencia de la regla de corte, la regla de sustitución es admisible en CLKIDω
2. Resultados Extendidos: Cuando se restringe la sustitución a sustituciones atómicas (que no introducen símbolos de función de aridad positiva), el resultado se extiende a CLKIDω sin corte
3. Generalización de Aplicaciones: El resultado se aplica a otros sistemas de prueba, como sistemas de prueba cíclica para lógica de separación
4. Método Novedoso: Propone una estrategia de eliminación de tres pasos mediante despliegue infinito, elevación de sustitución y reconstrucción cíclica

Explicación Detallada del Método

Definición de la Tarea

Dada una prueba Pr+ en CLKIDω que contiene la regla de sustitución, construir una prueba Pr- que no contiene la regla de sustitución, de modo que ambas prueben el mismo secuente.

Arquitectura del Método Principal

El proceso de eliminación consta de dos fases principales:

1. Eliminación de Sustituciones Compuestas

Definiciones:

• Sustitución Atómica: Sustituye variables por variables y constantes
• Sustitución Compuesta: Sustituye variables por términos que contienen símbolos de función de aridad positiva

Método: Eliminar sustituciones compuestas mediante la siguiente transformación:

Γ ⊢ Δ
────────────────────────── (Subst)
Γ[x₁:=t₁,...,xₙ:=tₙ] ⊢ Δ[x₁:=t₁,...,xₙ:=tₙ]

Transformar en una combinación de la regla de corte, reglas de igualdad y reglas de cuantificador existencial, conservando finalmente solo sustituciones atómicas.

2. Eliminación de Sustituciones Atómicas

Esta es la innovación central, que comprende tres pasos:

Paso 1: Despliegue Cíclico

• Desplegar la prueba cíclica Pr_var+ en una prueba infinita Pr^ω
• Definir mapeo f^ω: Seq(Pr^ω) → Seq(Pr_var+) que asocia ocurrencias de secuentes

Paso 2: Elevación de Sustitución

• Construir recursivamente prueba LKIDω Pr^ω_d que no contiene la regla de sustitución dentro de profundidad d
• Utilizar la propiedad de aplicación de sustitución (substitution-application property)

Paso 3: Reconstrucción Cíclica

• Construir prueba previa CLKIDω Pr- a partir de Pr^ω_d
• Seleccionar brotes y compañeros, asegurando la condición de traza global

Puntos de Innovación Técnica

1. Clausura de Sustitución Parcial (Partial-substitution Closure)

Definición 10: Dada una colección de sustituciones Θ y un conjunto de variables X, la clausura de sustitución parcial Cps(Θ,X) es el conjunto mínimo que satisface:

• Θ ⊆ Cps(Θ,X)
• Para θ∈Cps(Θ,X) y x,y∈X: θx→y ∈ Cps(Θ,X)
• Para θ₁,θ₂∈Cps(Θ,X): θ₁θ₂ ∈ Cps(Θ,X)

Propiedad Clave: Cuando se restringe a sustituciones atómicas, la clausura de sustitución parcial es finita.

2. Propiedad de Aplicación de Sustitución (Substitution-application Property)

Definición 11: Una regla (R) satisface la propiedad de aplicación de sustitución si para cualquier instancia de regla y sustitución atómica θ, existe una instancia de aplicación de sustitución correspondiente que preserva las trazas.

Lema 4: CLKIDω y LKIDω satisfacen la propiedad de aplicación de sustitución.

3. Preservación de la Condición de Traza Global

Asegurar que la prueba reconstruida satisface la condición de traza global mediante el concepto de caminos correspondientes:

Definición 12: Para un camino (eᵢ) en Pr-, definir el camino correspondiente (e'ⱼ) en Pr_var+, de modo que cada traza infinita de progreso se preserve.

Configuración Experimental

Este artículo es trabajo puramente teórico sin experimentos en el sentido tradicional. La verificación se realiza mediante:

Verificación Teórica

1. Prueba Constructiva: Demostrar la admisibilidad mediante construcción explícita de algoritmos
2. Análisis de Contraejemplos: Analizar casos donde la admisibilidad no se satisface bajo restricciones
3. Extensión de Sistemas: Verificar la aplicabilidad de resultados en otros sistemas

Análisis de Ejemplos

El artículo proporciona ejemplos concretos de transformación de pruebas:

• Figura 1: Prueba cíclica que contiene la regla de sustitución
• Figura 3: Prueba infinita después del despliegue
• Demostración de cómo eliminar la regla de sustitución de la prueba cíclica de N(x) ⊢ E(x)∨O(x)

Resultados Experimentales

Resultados Teóricos Principales

Teorema 2 (Admisibilidad de la Regla de Sustitución en CLKIDω): Si Γ ⊢ Δ es demostrable en CLKIDω, entonces también es demostrable en CLKIDω sin (Subst).

Teorema 3 (Resultado Fuerte para Sustituciones Atómicas): Si Pr es una prueba de Γ ⊢ Δ en CLKIDω y Θ(Pr) contiene solo sustituciones atómicas, entonces existe una prueba sin (Subst) que contiene solo las reglas que aparecen en Pr.

Resultados Extendidos

Teorema 4 (Admisibilidad en Sistemas sin Corte): En CLKIDω^- (CLKIDω sin corte), la regla de sustitución atómica es admisible.

Teorema 5 (Aplicación en Lógica de Separación): La regla de sustitución es admisible tanto en CSLω como en CSLω^-.

Hallazgos Teóricos

1. Papel Crítico de la Regla de Corte: La eliminación de sustituciones compuestas requiere la regla de corte
2. Universalidad de Sustituciones Atómicas: La eliminación de sustituciones atómicas se aplica a una clase más amplia de sistemas
3. Restricción de Símbolos de Función: La presencia de símbolos de función es un obstáculo clave para la admisibilidad

Trabajo Relacionado

Direcciones Principales de Investigación

1. Teoría de Prueba Cíclica: Trabajo pionero de Brotherston y otros 1,4,6
2. Búsqueda de Pruebas: Investigación para evitar búsqueda heurística de hipótesis inductivas 2,3,5,11,12
3. Lógica de Separación: Aplicaciones de prueba cíclica en lógica de separación 2,7,9

Relación de Este Artículo con Trabajo Relacionado

• Resuelve el problema abierto planteado por Brotherston 1
• Extiende el trabajo de Kimura y otros 7 a configuraciones más generales
• Proporciona base teórica para búsqueda de pruebas

Ventajas de Este Artículo

1. Primera Demostración: Primera prueba rigurosa de la admisibilidad de la regla de sustitución en CLKIDω
2. Innovación Metodológica: Propone nuevas técnicas de eliminación aplicables a estructuras cíclicas
3. Amplia Aplicabilidad: Los resultados se aplican a múltiples sistemas relacionados

Conclusiones y Discusión

Conclusiones Principales

1. En CLKIDω con la regla de corte, la regla de sustitución es admisible
2. Cuando se restringe a sustituciones atómicas, el resultado se extiende a sistemas sin corte
3. El resultado se aplica a otros sistemas importantes como lógica de separación

Limitaciones

1. Dependencia de la Regla de Corte: La eliminación de sustituciones compuestas requiere la regla de corte
2. Restricción de Símbolos de Función: El resultado completamente general requiere excluir símbolos de función
3. Complejidad de Construcción: El proceso de construcción de pruebas es relativamente complejo

Direcciones Futuras

1. Conjunto de Reglas Mínimo: Investigar el conjunto mínimo de reglas que permite la eliminación de la regla de sustitución en presencia de símbolos de función
2. Eliminación de Corte: Estudiar la propiedad de eliminación de corte en sistemas de prueba cíclica mediante la introducción de reglas adicionales
3. Complejidad Computacional: Analizar la complejidad computacional de la eliminación de la regla de sustitución

Evaluación Profunda

Fortalezas

1. Importancia Teórica: Resuelve un importante problema abierto en el campo
2. Innovación Metodológica: Propone nuevas técnicas aplicables a estructuras cíclicas
3. Rigor: La prueba es rigurosa y constructiva
4. Amplia Aplicabilidad: Los resultados se aplican a múltiples sistemas relacionados
5. Claridad de Presentación: Los detalles técnicos se presentan de manera clara y comprensible

Debilidades

1. Limitaciones de Practicidad: La dependencia de la regla de corte limita las aplicaciones prácticas
2. Complejidad: El proceso de transformación de pruebas es relativamente complejo
3. Completitud: En configuraciones sin corte aún hay restricciones

Impacto

1. Contribución Teórica: Proporciona base teórica importante para la teoría de prueba cíclica
2. Valor Práctico: Proporciona mayor flexibilidad para implementaciones de búsqueda de pruebas
3. Extensibilidad: El método puede ser aplicable a otros sistemas relacionados

Escenarios de Aplicación

1. Demostración Automática de Teoremas: Mejorar la eficiencia de búsqueda de pruebas cíclicas
2. Verificación de Programas: Aplicaciones en marcos de verificación como lógica de separación
3. Investigación Teórica: Proporciona base para investigación teórica adicional en prueba cíclica

Referencias Bibliográficas

El artículo cita 19 referencias relacionadas, incluyendo principalmente:

1. Trabajo pionero de Brotherston en prueba cíclica
2. Investigación sobre aplicaciones de prueba cíclica en lógica de separación
3. Trabajo relacionado en búsqueda automática de pruebas
4. Investigación fundamental en eliminación de corte y teoría de prueba

Este artículo realiza contribuciones importantes a la teoría de prueba cíclica, resolviendo un problema abierto importante mediante técnicas innovadoras, sentando las bases para desarrollo adicional en el campo.