Preguntas etiquetadas con logic

13
¿Prueba si una prueba arbitraria es circular?

Estaba pensando en pruebas y me encontré con una observación interesante. Por lo tanto, las pruebas son equivalentes a los programas a través del isomorfismo de Curry-Howard, y las pruebas circulares corresponden a una recursión infinita. Pero sabemos por el problema de detención que, en general,...

12
Prueba de tautología con coq

Actualmente tengo que aprender Coq y no sé cómo lidiar con un or: Como ejemplo, tan simple como es, no veo cómo demostrar: Theorem T0: x \/ ~x. Realmente lo agradecería si alguien pudiera ayudarme. Como referencia utilizo esta hoja de trucos . También un ejemplo de una prueba que tengo en...

12
¿Qué es una "contradicción" en la lógica constructiva?

En Fundamentos prácticos para lenguajes de programación , Robert Harper dice Si para que una proposición sea verdadera significa tener una prueba de ello, ¿qué significa que una proposición sea falsa? Significa que tenemos una refutación de ello, lo que demuestra que no se puede probar. Es...

11
¿Hay alguna diferencia entre y ?

Actualmente estoy aprendiendo el cálculo lambda y me preguntaba sobre los siguientes dos tipos diferentes de escribir un término lambda. λxy.xyλxy.xy\lambda xy.xy λx.λy.xyλx.λy.xy\lambda x.\lambda y.xy ¿Hay alguna diferencia en el significado o la forma en que aplica la reducción beta, o esas...

11
Ejemplo de solidez e integridad de inferencia

¿Es correcto el siguiente ejemplo sobre si un algoritmo de inferencia es sólido y completo ? Supongamos que tenemos agujas a, b, c en un pajar, y también tenemos un algoritmo de inferencia diseñado para encontrar agujas. sonido : solo se obtienen las agujas a, byc. Completo : se obtienen las...

11
Inferir tipos de refinamiento

En el trabajo, se me ha encomendado la tarea de inferir cierta información sobre un lenguaje dinámico. Reescribo secuencias de declaraciones en letexpresiones anidadas , así: return x; Z => x var x; Z => let x = undefined in Z x = y; Z => let x = y in Z if x then T else F; Z => if x...

11
Libro introductorio sobre lógica y computación

¿Me puede dar algunas sugerencias sobre un buen libro introductorio (pero completo) sobre Lógica y Computación? Algunos temas confusos que tengo en mente son: Presburger artihm., PA, ZF, ZFC, HOL Teoría de conjuntos, Teoría de tipos Computación de modelado (máquinas de Turing) en diferentes...

10
Término reescritura; Calcular pares críticos

Intenté resolver el siguiente ejercicio, pero me quedé estancado mientras trataba de encontrar todos los pares críticos . Tengo las siguientes preguntas: ¿Cómo sé qué par crítico produjo una nueva regla? ¿Cómo sé que encontré todos los pares críticos? Deje Σ={∘,i,e}Σ={∘,i,e}\Sigma= \left \{...

10
Intuición detrás de la puerta de Hadamard

Estoy tratando de enseñarme sobre computación cuántica, y tengo una comprensión decente del álgebra lineal. Atravesé la puerta NOT, que no estaba tan mal, pero luego llegué a la puerta Hadamard. Y me quedé atrapado. Principalmente porque si bien "entiendo" las manipulaciones, no entiendo lo que...