Deje que sea cualquier estructura finita. ¿Su teoría de primer orden tiene un rango cuantificador acotado, en el sentido de que hay un tal que para todos con hay un con y ?AA\mathfrak{A} T:=TH(A)T:=TH(A) \mathfrak{T} := \mathfrak{TH}(\mathfrak{A}) q∈Nq∈N q\in\mathbb{N} φ∈Tφ∈T...
¿Cuál es la relación entre el cálculo lambda simplemente escrito y la lógica de orden superior? Bajo Curry-Howard parece que el cálculo lambda simplemente escrito corresponde a la lógica proposicional. ¿Cómo se relaciona con la lógica de orden superior? Según este tutorial de Geuvers:...
Las lógicas condicionales son lógicas que aumentan la implicación lógica tradicional con operadores modales correspondientes a otras nociones de condición (por ejemplo, la condicional causal lee " A causa" B ", o condicionamiento probabilístico" A | B ", que dice" A dado B ").A□→BA◻→BA\;...
Sé que la pregunta "si una fórmula de primer orden tiene un modelo" es indecidible en general.ϕϕ\phi ¿Alguien podría darme un enlace o un libro que dé la respuesta para modelos finitos? Si tengo una fórmula de primer orden , ¿es decidible si ϕ tiene un modelo finito? Estoy bastante seguro de que...
Estoy en posesión de un libro que, inspirado en los Principia Mathematica (PM) de Russell y el positivismo lógico, intenta formalizar un dominio específico determinando axiomas y deduciendo teoremas de ellos. En resumen, intenta hacer por su dominio lo que PM intentó hacer por las matemáticas. Al...
He leído sobre la sustitución hereditaria del cálculo simple de Lambda y del marco lógico con términos y tipos distintos. Me pregunto, ¿hay algún ejemplo de sustitución hereditaria en un sistema de tipo dependiente con una jerarquía universal? es decir, donde
La mayoría de las teorías de tipos que conozco son predicativas, lo que quiero decir que Void : Prop Void = (x : Prop) -> x no está bien tipado en la mayoría de los probadores de teoremas ya que este tipo pi pertenece al mismo universo Propy no es el caso Prop : Prop. Esto los convierte en...
Estoy buscando una técnica general que pueda ayudarme a demostrar no solo que el autómata de Buchi es un modelo más expresivo que LTL, sino que la fórmula específica puede / no puede expresarse en LTL. Por ejemplo, " ocurre al menos en posiciones pares" puede describirse mediante los siguientes...
La lógica monádica de primer orden, también conocida como la clase monádica del problema de decisión, es donde todos los predicados toman un argumento. Se demostró que era decidible por Ackermann, y está NEXPTIME-complete . Sin embargo, problemas como SAT y SMT tienen algoritmos rápidos para...
Estoy traduciendo un libro sobre LISP y, naturalmente, toca algunos elementos del cálculo . Entonces, una noción de extensionalidad se menciona allí junto con algunos modelos de cálculo λ , a saber: P ω y D ∞ (sí, con el infinito en la parte superior). Y se dice que P ω es extensional mientras que...
El teorema de Courcelle establece que cada propiedad de gráfico definible en la lógica monádica de segundo orden se puede decidir en tiempo lineal en gráficos de ancho de árbol acotado . Este es uno de los metateoremas algorítmicos más conocidos. Motivado por el teorema de Courcelle, hice la...
Sé cómo algunas ocurrencias negativas pueden ser definitivamente malas: data False data Bad a = C (Bad a -> a) selfApp :: Bad a -> a selfApp (x@(C x')) = x' x yc :: (a -> a) -> a yc f = selfApp $ C (\x -> f (selfApp x)) false :: False false = yc id Sin embargo, no estoy seguro...
La teoría de tipos de Martin-Löf usa tipos W para definir estructuras inductivas como enteros, listas, etc. Sin embargo, el cálculo de construcciones inductivas no las usa de la misma manera, los tipos inductivos parecen ser más como esquemas de axiomas. ¿Son equivalentes estos dos enfoques...
El problema de representar las variables ligadas en la sintaxis, y en particular el de la sustitución para evitar la captura, es bien conocido y tiene una serie de soluciones: variables nombradas con equivalencia alfa, índices de Bruijn, anonimato local, conjuntos nominales, etc. Pero parece haber...
Un árbol de decisión de lectura única se define de la siguiente manera: y F a l s e son árboles de decisión de una sola lectura.Tr u eTrueTrueFa l s eFalseFalse Si y B son árboles de decisión de lectura única yx es una variable que no ocurre en A y B , entonces ( x ∧ A ) ∨ ( ˉ x ∧ B ) también...
Estoy tratando de entender la lógica lineal para comprender mejor los sistemas de tipo lineal. Sin embargo, cuando leí las reglas, no llego a tener una intuición detrás de él como lo he hecho en la lógica modal - significa un se requiere como en los marcos de Kripke A es necesaria para todos los...
Todos los solucionadores de #SAT que conozco, por ejemplo, RelSat, C2D, solo devuelven el número de instancias satisfactorias. Pero quiero saber cada una de esas instancias? ¿Existe tal solucionador #SAT o cómo debo modificar un solucionador #SAT disponible para hacer
En Complexity Zoo, dice [ 1 ] que, en complejidad descriptiva, PAGPAGP puede definirse mediante tres tipos diferentes de fórmulas, FO ( L FPAG)FO(LFPAG)FO(LFP) que también es FO ( nO ( 1 ))FO(norteO(1))FO(n^{O(1)}) , y también como SO ( HO R N)SO(HORnorte)SO(HORN) . Sin embargo, hay algunas...
La resolución es un esquema para demostrar la insatisfacción de los CNF. Una prueba en resolución es una deducción lógica de la cláusula vacía para las cláusulas iniciales de la CNF. En particular, se puede inferir cualquier cláusula inicial, y de dos cláusulas A ∨ xA∨xA \lor x y B ∨ ¬ xB∨¬xB \lor...
La teoría de tipo constructivo con su interpretación básica bajo la correspondencia de curry howard consiste solo en funciones totales y computables. En la literatura, se ha dicho algo sobre el uso de la "teoría del tipo computacional" para representar la no terminación en los programas...