63 artículos
El artículo presenta Apply2Isar, una herramienta que convierte automáticamente los guiones de prueba procedimentales en estilo "apply" de Isabelle/HOL a pruebas declarativas estructuradas en Isar, combinando la rapidez de exploración de los primeros con la legibilidad y robustez de los segundos.
El artículo demuestra que la brecha entre el tamaño mínimo de un circuito booleano y el de una fórmula en la base AIG es siempre 0 o 1, estableciendo que el uso compartido de puertas solo es necesario cuando hay al menos variables esenciales y que, cuando la brecha es 1, surge exclusivamente de un único nodo con fan-out 2.
Este artículo propone los conceptos de autómata de paso y máquina de Turing de paso (STM) como extensiones naturales de los modelos tradicionales que permiten ejecutar un paso de acciones atómicas sin órdenes parciales, llenando así el vacío existente entre la máquina de Turing y los autómatas concurrentes.
Este artículo documenta cómo la formalización en el asistente de pruebas interactivo Lean reveló un error en el teorema principal de un influyente artículo de 2006 sobre la estabilidad del potencial del modelo de dos dobletes de Higgs, marcando el primer hallazgo de un error no trivial en física mediante este método.
Este artículo introduce la teoría de categorías enriquecidas con seminormas dilatadas como un marco unificador para los límites centrales, estableciendo un teorema central abstracto que generaliza resultados clásicos como la ley de los grandes números y deriva un nuevo teorema para variedades simplécticas con aplicaciones en mecánica estadística.
Este artículo demuestra que la lógica de equipos inquisitiva y la lógica inquisitiva de primer orden poseen un poder expresivo que supera al de la lógica de primer orden, permitiendo a sus fórmulas abiertas y ciertas oraciones expresar propiedades no definibles en este último, como la finitud.
Este trabajo desarrolla un marco teórico de especificaciones GSOS abstractas para lenguajes de orden superior, representando su semántica operacional mediante transformaciones dinaturales llamadas leyes GSOS de orden superior puntuadas, lo que permite demostrar resultados generales de composicionalidad aplicables a sistemas como el cálculo SKI y el cálculo lambda.
Este artículo propone un marco de razonamiento abductivo basado en la consistencia que integra las predicciones de múltiples modelos preentrenados mediante reglas lógicas para mitigar la degradación del rendimiento en entornos novedosos, logrando mejoras significativas en precisión y recall frente a enfoques individuales y de conjunto estándar.
Este artículo presenta GRAMPUS, un lenguaje basado en teoría de tipos modales graduados que utiliza grados temporales para especificar formalmente y semánticamente los programas de pulsos de microondas necesarios para controlar computadoras cuánticas de qubits superconductores.
El artículo demuestra que el Problema de Skolem es decidible en anillos conmutativos finitamente generados de característica positiva, estableciendo un algoritmo para determinar si una sucesión de recurrencia lineal contiene un término nulo y probando que su conjunto de ceros es una unión finita de conjuntos -normales.
Este trabajo presenta algoritmos basados en CDCL para la Enumeración de Modelos Ponderados (WME), integrando propagación, poda y análisis de conflictos ponderados en marcos de retroceso cronológico y no cronológico para abordar consultas de enumeración selectiva guiadas por pesos.
Este artículo presenta una formalización constructiva de los Sistemas de Reescritura Abstracta en Agda, que elimina la lógica clásica en pruebas estándar, refina los criterios de terminación y confluencia y demuestra su aplicabilidad mediante la formalización del cálculo lambda.
Este artículo presenta la formalización en Lean 4 de varios teoremas tipo Farkas sobre cuerpos ordenados linealmente y extiende la teoría de dualidad en la optimización lineal al caso en que algunos coeficientes pueden tomar valores infinitos.
El artículo demuestra que la compacidad de una estructura relacional finita de ancho uno es demostrable en ZF, mientras que la compacidad de estructuras de mayor ancho implica la existencia de conjuntos no medibles en el espacio tridimensional.
Este artículo presenta una reformulación topológica de la mereogeometría de Tarski mediante el asistente de pruebas Coq, completando su formalización en lambda-MM al demostrar la correspondencia entre clases mereológicas y conjuntos abiertos regulares, lo que permite derivar un espacio topológico completo con la propiedad de Hausdorff y reducir el sistema axiomático original.
Este trabajo propone un enfoque neuro-simbólico que integra modelos de lenguaje grandes con solucionadores de restricciones para generar automáticamente lemas auxiliares, logrando resolver aproximadamente un 25% más de tareas de prueba con definiciones inductivas que las herramientas actuales.
Este artículo presenta el concepto de cambio de modelo para conceptos de lógica descriptiva, distinguiendo entre expulsión, recepción y revisión, y demuestra que la revisión no es simplemente una combinación de las otras dos operaciones, proporcionando además resultados sobre su compatibilidad en las lógicas EL y ALC.
El artículo introduce el concepto de "explicación" entre modelos probabilísticos como un tipo específico de espansión en la categoría , demostrando que estas explicaciones se componen mediante construcciones de pullback y que todo modelo probabilístico localmente finito posee una explicación clásica canónica y precisa, lo que permite una representación functorial de tales teorías.
El artículo presenta LTLGuard, una herramienta modular que combina la generación de modelos de lenguaje compactos con verificación simbólica ligera para traducir requisitos informales en especificaciones de lógica temporal lineal (LTL) correctas y sin conflictos.
Este artículo demuestra que, aunque la auto-certificación acotada en máquinas de Turing falla debido a la sobrecarga temporal, el límite de Scott de la cadena ascendente generada por la iteración de este proceso converge a un punto fijo mínimo que representa una computación no acotada capaz de capturar completamente el comportamiento de parada, redefiniendo así el problema de la parada como una deferral continua de la diagonalización.