es bien sabido que el cálculo μ modalμμ\mu es una de las lógicas temporales más expresivas para expresar las propiedades de los árboles / gráficos, y que CTL * es estrictamente menos expresivo que el cálculo .μμ\mu Aquí me gustaría pedir un ejemplo de fórmula de cálculo , tan simple como sea...
Cerrado. Esta pregunta está fuera de tema . Actualmente no está aceptando respuestas. ¿Quieres mejorar esta pregunta? Actualice la pregunta para que sea sobre el tema para el intercambio teórico de pila de informática. Cerrado hace 7 años . ¿Cómo...
Tengo dificultades para comprender la prueba de una fuerte normalización para el cálculo de las construcciones. Trato de seguir la prueba en el documento de Herman Geuvers "Una prueba corta y flexible de Normalización Fuerte para el Cálculo de Construcciones". Puedo seguir bien la línea principal...
Vi que algunas personas usan la notación de Krivine para la aplicación de funciones cuando presentan la sintaxis para el cálculo . Por ejemplo, el λ -term λ f . λ x . λ y . f x y (con la convención normal de que la aplicación de función se asocia a la izquierda, por lo que en realidad significa que...
Estoy buscando la complejidad de la satisfacción de una fórmula o de una fórmula ∃ x 1 , ... , x m ∀ y 1 , ... , y n , ϕ donde ϕ es la fórmula de la forma: ϕ : = ϕ ∧ ϕ | ¬ ϕ | ϕ∀ y1, ... , ynorte, ∃ x1, ... , xmetro, ϕ∀y1,…,yn,∃x1,…,xm,ϕ\forall y_1, \dots,y_n, \exists x_1,\dots,x_m, \phi∃ x1, ......
Esta pregunta es esencialmente la pregunta que hice en Mathoverflow. La lógica monádica de segundo orden (MSO) es lógica de segundo orden con cuantificación sobre predicados unarios. Es decir, cuantificación sobre conjuntos. Hay varias lógicas de MSO que son fundamentales para las estructuras...
Feto, si no has oído hablar de él, puedes leerlo aquí . Utiliza un sistema de 'matrices de llamadas' y 'gráficos de llamadas' para encontrar todos los 'comportamientos de recursividad' de llamadas recursivas en una función. Para mostrar que una función termina, muestra que todos los comportamientos...
Los sistemas tipificados más dependientes tienen unas condiciones de positividad estrictas para los tipos inductivos. ¿Alguien sabe un ejemplo donde la violación de la condición conduce a la inconsistencia en el
Sabemos por el teorema de Church que determinar la satisfacción de primer orden es indecidible en general, pero existen varias técnicas que podemos usar para determinar la satisfacción de primer orden. Lo más obvio es buscar un modelo finito. Sin embargo, hay una serie de declaraciones en la lógica...
Estoy tratando de entender los conceptos de tipos universales y existenciales, pero en todas partes veo intuiciones lógicas u operativas (o implementaciones) (por ejemplo, el libro TAPL de B. Pierce), que, bueno ... es bueno , pero me gustaría ver las definiciones (donde las vemos como conjuntos),...
¿Alguien sabe de algún trabajo en la semántica de juegos para predicados coinductores? Un predicado coinductivo es aquel en el que el predicado en sí se llama en el cuerpo del predicado, y estamos tomando el significado del predicado como el mayor punto fijo de la definición subyacente. Dicho...
¿Cuáles son las mejores referencias para el autoestudio en DATALOG? Estoy particularmente interesado en el poder expresivo, los resultados de complejidad, los métodos de evaluación, las extensiones de DATALOG con negación, etc. ¿Hay libros o documentos que cubran todo
Estoy buscando trabajo en sistemas que sean similares a los secuenciantes de orden superior de K. Dosen ("Sistemas secuenciales para lógica modal", JSL 50 ). El único trabajo que conozco es el reciente trabajo de Iemhoff y Metcalfe ("Teoría de la prueba de reglas admisibles", Annals of Pure and...
Estoy escribiendo un modelo de juguete , y estoy en el punto en que es hora de implementar la traducción de autómatas LTL a Buchi. Por una variedad de razones obvias, deseo que el algoritmo sea simple :) por ejemplo, quiero que el código permanezca extremadamente claro y conciso durante el mayor...
La pregunta es si es posible modelar en lógica lineal dos modos de acceso a un recurso. Sé que son posibles dos modos de recursos, es decir: !r⊢!r⊢!r \vdash r está infinitamente disponible r solo está disponible una vez r⊢r⊢r \vdash \quad Pero, ¿y si no quiero decidir si r es infinita o solo una...
Aunque L.Berman demostró que el problema de verificar o falsificar cualquier declaración de primer orden sobre números reales que usa la suma y la comparación pero no la multiplicación está en EXPSPACE. ¿Se le ha mostrado cuánto tiempo o espacio necesitaría para verificar o falsificar cualquier...
Estoy tratando de desarrollar algunas nociones de un cálculo de diferencia entre una máquina ideal de Turing ideal concebida por un desarrollador (por ejemplo, lo que sea que pretenda un desarrollador de software), llámelo y las máquinas que representan el software que realmente se diseñó y...
Soy nuevo en el estudio de sistemas de reescritura como estudiante de doctorado de primer año. Me gustaría proponer un curso de temas especiales sobre la teoría de la reescritura, y quiero asegurarme de no dejar de lado ninguna de las fuentes originales. Tengo una copia de Barendregt y Terese como...
Estoy buscando el documento original donde Hoare (o alguien más, supongo) discute la terminación (corrección total). O cualquier otro trabajo inicial sobre la terminación de la lógica "vainilla" de Hoare (supongo que con eso me refiero a un HL para un lenguaje de juguete tipo C). He echado un...
He encontrado esta aplicación web que te permite generar un teorema gratuito para un tipo dado. Los teoremas generados cuantifican sobre tipos y relaciones sobre estos tipos. Estos teoremas (fórmulas) son teoremas de qué teoría / sistema lógico? ¿Cómo se relaciona este sistema con la teoría de la...