DEDUCCIÓN NATURAL 28/03/2017

DEDUCCIÓN NATURAL

La deducción natural es una aproximación a la teoría de la demostración en la que se busca capturar la manera en que las personas razonan naturalmente al construir demostraciones matemáticas. En vez de contar con unos pocos axiomas a los que se aplican unas pocas reglas de inferencia, la deducción natural propone vaciar la lista de axiomas y ampliar la de reglas de inferencia, introduciendo dos reglas para cada constante lógica: una para introducirla y otra para eliminarla. Una demostración se construye partiendo de supuestos y aplicando las reglas para llegar a la conclusión deseada

¿PARA QUE SIRVE?

La deducción natural sirve para intentar demostrar que un razonamiento es correcto (``para comprobar la validez de un secuente'', dice la teoría). Ejemplo:

Yo te digo: ``En verano hace calor, y ahora estamos en verano, por eso hace calor''. Tú te pones a hacer cálculos, y respondes ``Vale, puedo demostrar que el razonamiento que has hecho es correcto''. Para eso sirve la deducción natural.

No siempre es tan fácil: ``si suspendes una asignatura, la tienes que repetir. Si no estudias, la suspendes. Supongamos que no la repites. Entonces, o la estudias, o la suspendes, o las dos cosas a la vez''. Este razonamiento es válido y se puede demostrar con la deducción natural.

Fíjate que no tienes que creerte ni entender lo que te cuente. Por ejemplo, yo te digo: ``Los tiristores son pequeños y divertidos; un garbanzo no es pequeño, así que no es un tiristor''. Aunque no sepas de qué hablo o te parezca que es mentira o es una idiotez (que lo es), tienes que estar totalmente seguro de que el razonamiento es correcto.

O sea, que, dada una suposición ``si pasa esto entonces pasa esto otro'', la deducción natural permite decir ``sí, así es''. En lenguaje lógico: si te dan un secuente ATB puedes acabar concluyendo que es l= (válido). Entonces se escribe Al=B (A tiene como consecuencia a B).

¿COMO OPERA?

Se pide demostrar la validez de  T l- S donde T (se lee gamma) es un grupo de fórmulas separadas por comas, y S es una sola fórmula.

Partimos de que todas las fórmulas de T son ciertas, y, mediante 9 reglas concretas, podemos ir descubriendo qué más cosas son ciertas. Nuestra intención es ver que S es cierta; una vez conseguido ya podemos acabar.

A veces no podremos sacar verdades de ningún lado, y habrá que hacer suposiciones: ``bueno, no estoy seguro de que A ∧B sea cierto siempre, pero si se cumple C, seguro que lo es''. Entonces ya hemos descubierto otra cosa cierta: que  C ⇒A ∧B.

Como ves, siempre hay que pensar hacia dónde queremos llegar, porque de otra forma podríamos adivinar un montón de cosas que son ciertas pero que no nos están pidiendo. Por ejemplo, con  A ∨B, ¬Al- B tenemos que llegar a que es cierto B. Podemos descubrir que 

¬(A ∧ B), A ∨ B ∨ C, (A ∨ B) ⇒¬A, y muchas más cosas, pero lo que nos interesa es B y ya está. O sea, que si no vas por el camino correcto, te puedes hacer un lío.

EJEMPLOS:

Ejemplo 1

Demostrar mediante deducción natural

          P(c),

          ∀x[P(x) → ¬Q(x)] 

          l- ¬Q(c)

Solución:

          1 P(c)                                    Premisa

          2 ∀x[P(x) → ¬Q(x)]               Premisa 

          3 P(c) → Q(c)                        E ∀ 2

          4 Q(c)                                    E → 3, 1

Ejemplo 2

Demostrar mediante deducción natural 

          ∀x[P(x) → ¬Q(x)],

          ∀xP(x)  

          l-∀x¬Q(x)

 Solución:

          1 ∀x[P(x) → ¬Q(x)]                   Premisa 

          2 ∀xP(x)                                    Premisa 

          3 par´ametro x0                          Supuesto 

          4 P(x0) → ¬Q(x0)                      E ∀ 1, 3 

          5 P(x0)                                      E ∀ 2, 3 

          6 Q(x0)                                      E → 4, 5 

          7 ∀x¬Q(x)                                  I ∀ 3 − 6

Ejemplo 3

Demostrar mediante deducción natural

          ∀xP(x) 

          l-∃xP(x) 

Solución:

          1 ∀xP(x)                              Premisa 

          2 P(x0)                                E ∀ 1 

          3 ∃xP(x)                              I ∃ 2

Read More

RESOLUCIÓN PROPOSICIONAL

RESOLUCIÓN PROPOSICIONAL


Sabemos que Σ |= p si y solo si Σ ∪ {¬ p } es inconsistente.
¿Como verificamos si Σ ∪ {¬ p } es inconsistente?

• El método basado en tablas de verdad es demasiado lento. 
• Necesitamos un método alternativo que no construya tablas de verdad.

Reducción a clausulas

Notación: Una clausula es una disjuncion de literales. 

Ejemplo: p ∨ ¬q ∨ ¬r. 

Una formula p esta en CNF si es de la forma C1 ∧ C2 ∧ · · · ∧ Cn, donde cada Ci es una clausula. Podemos representar p como {C1, C2, . . . , Cn}. ¿Por que? 

Notación: También usamos ≡ para denotar equivalencia entre conjuntos de formulas

Reducción a clausulas

Toda formula es equivalente a un conjunto de clausulas. 

Ejemplo:

(p ∨ q) → r ≡ ¬(p ∨ q) ∨ r

≡ (¬p ∧ ¬q) ∨ r 

≡ (¬p ∨ r) ∧ (¬q ∨ r) 

≡ {¬p ∨ r, ¬q ∨ r}

Entonces: Nos basta con resolver el problema de satisfacibilidad para conjuntos de clausulas. 

La regla de resolución 

¿Como verificamos si un conjunto de clausulas es inconsistente? 

Sabemos que Σ es inconsistente si y solo si Σ |= p, donde p es una contradicción cualquiera.

Entonces: Fijamos una contradicción y lo que hacemos es verificar si Σ |= .

Notación: Decimos que es la clausula vacía porque una clausula sin literales no es satisfacible.

La regla de resolución 

Para verificar que Σ |= no queremos usar valuaciones, queremos usar alguna regla sintáctica.

Notación: Si l = p, entonces ¯l = ¬p, y si l = ¬p, entonces ¯l = p.

Dado: clausulas C1, C2, C3, C4 y literal l. 

Regla de resolución: 

                                       C1 ∨ l ∨ C2

                                       C3 ∨ ¯l ∨ C4 

                                __________________

                                  C1 ∨ C2 ∨ C3 ∨ C4

La regla es correcta: {C1 ∨ l ∨ C2, C3 ∨ ¯l ∨ C4} |= C1 ∨ C2 ∨ C3 ∨ C4

La regla de resolución:Ejemplo 

Ejemplo:

                                         ¬ p ∨ q 

                                         ¬ q ∨ r

                                     ___________

                                         ¬ p ∨ r

Tenemos que: {¬ p ∨ q, ¬ q ∨ r} | = ¬ p ∨ r

La regla de resolución: Casos particulares

Algunos casos particulares de la regla de resolución: 

                                     C 1 ∨ l ∨ C2 

                                       i 

                                 ______________

                                       C 1 ∨ C2 

Read More

TABLEAUX

TABLEAUX

cuadros semántica es un sistema de deducción que también establece estructuras que permiten la representación y la deducción formal del conocimiento. cuadros semántica es el más adecuado para las implementaciones en equipos. El método de cuadros semántica fue inventado por los estudiosos de la lógica holandés 

Un cuadro semántico en la logica proposicional es una secuencia de fórmulas construidas de acuerdo con ciertas reglas y generalmente tiene la forma de un árbol. Los elementos básicos que componen este árbol se definen a continuación.

Definición (elementos básicos de un cuadro semántica) 

Los elementos básicos de un cuadro semántico en la lógica de proposiciones se definen por la composición de los elementos:

• El alfabeto de la lógica de proposiciones;
• El conjunto de fórmulas lógicas proposicionales
• Un conjunto de reglas de inferencia.

El cuadro semántica contiene reglas de deducción sólo, que definen el motor de inferencia, lo que permite la deducción del conocimiento. Las normas se especifican a continuación.

Definición (reglas de inferencia del cuadro semántica) 

A y B son dos fórmulas de la lógica de proposiciones. Las reglas de inferencia de la lógica de proposiciones cuadro semántica son R ₁ , ..., R ₉ se muestra a continuación.

El método de prueba en los cuadros se realiza utilizando el método de la negación o absurdo. Por lo tanto, para muestrear un Fórmula A, se considera inicialmente su negación ¬ A. A continuación, el cuadro semántica asociada con ¬ A se construye. Debido a este hecho, este sistema también se denomina como un sistema de impugnación. El cuadro semántica se construye a partir ¬A usando las reglas de inferencia cuya aplicación se descompone ¬A fórmula fórmulas parciales.

En general, la aplicación de una regla para un cuadro se hace teniendo en cuenta cualquiera de las fórmulas. Sin embargo, una buena heurística en la construcción del cuadro se aplicará inicialmente reglas que no se bifurcan el árbol. Se aplican las reglas preferiblemente R ₁ , R ₅ , R ₇ y R ₈ .

La construcción de un cuadro semántica se define de forma recursiva como sigue.

Ejemplo 1

Este es un tableau para 8x9yPxy. 1. 8x9yPxy 2. 9yPcy 3. Pcd γ1 δ2 Notas La lÌnea 2 se obtuvo de la lÌnea 1 usando la γ-regla ëde 8xA(x) se deduce A(t) para cualquier tÈrmino cerrado tí. AquÌ, A(x) era ë9yPxyí. Decidimos que t fuese una constante, c. (PodrÌamos haber usado cualquier otro tÈrmino cerrado.) La lÌnea 3 se obtuvo de la lÌnea 2 aplicando la δ-regla ëde 9yA(y ) se deduce A(c) donde c es una constante nuevaí. AquÌ, A(y ) era Pcy. Usamos la constante nueva d. No podÌamos haber usado c porque ya habÌa sido previamente usada en la rama

Ejemplo 2

otro tableau para 8x9yPxy PodrÌamos haber seguido aplicando las reglas: 1. 8x9yPxy 2. 9yPcy 3. Pc 4. 9yPdy 5. 9yPfcady 6. Pde 7. Pfcadb γ1 δ2 γ1 γ1 δ4 δ5 Notas. AquÌ hemos introducido d, e y b como par·metros de PAR en las lÌneas 3, 6 y 7, mientras que c y fcad son tÈrminos de L PAR . Paramos cuando todas las ramas est·n cerradas, pero si una rama no se cierra no sabemos si es que no puede cerrarse o que no hemos acertado con el par·metro adecuado. 

Los tableaux sirven para demostrar teoremas 

Procedimiento refutativo El calculo de tablea es de naturaleza refutativa, se basa en la b˙squeda de un contraejemplo. Por ello negamos la conclusiÛn de lo que queremos demostrar y explicitamos la contradicciÛn que de ello se deriva. Como en LP, deÖnimos el concepto de prueba, tanto de teoremas lÛgicos, como de teoremas a partir de hipÛtesis. En particular: 

1 Sea A una sentencia. Escribimos ` A si existe un tableau cerrado para :A. 

2 Sea A una sentencia y Γ un conjunto de sentencias. Escribimos Γ ` A si existe un tableau cerrado para Γ [ f:Ag. Esto es, una refutaciÛn de Γ [ f:Ag.

Estrategias de aplicacion

1 Aplicar antes las reglas proposicionales que las de primer orden. 

2 y para las primeras usad las estrategias conocidas. Primero las reglas α que las β y entre ellas siempre primero las que cierren ramas. En otro caso, la fÛrmula m·s compleja. 

3 Entre las reglas con cuantiÖcadores aplicar antes las reglas δ que las γ

Tableaux con variables libres

 A continuación presentamos un método de tableaux con variables libres para LPO en el u. que las fórmulas de clase Gamma introducen variables libres, en lugar de términos básicos. Estas variables son instanciadas a la hora de cerrar una rama, usando algún algoritmo de unificación sintáctica, 

El sistema de tableaux con variables libres está compuesto por las anteriores reglas cv,¡3 y por las nuevas ‘y’,3’. Para 3’, supondremos además que la signatura extendida E también contiene infinitos símbolos de función de Skolem, para cualquier andad, a” 

1. Regla ‘y’. Añadimos un nuevo nodo a la rama donde se emicuentra la fórmula Gamma, sustituyendo la variable universalmente cuantificada por una variable libre y, nueva en el tableau: -‘Bxy u. -‘y[y/x]

2. Regla 3’. Añadimos un nuevo nodo a la rama donde se encuentra la fórmula Delta, si sustituyendo la variable existencialmente cuantificada por el término f(xj ,...,x~), donde f es un símbolo de Skolem, nuevo en el tableau, y las variables xj, ,, son a las variables libres que aparecen en la rama: Bxy y[f(xs r)/x] 

Definición 2.4.4 (Cierre de máxima generalidad) Un tableau con variables libres ‘F y ramas Bm,... ,Bk está cerrado si existe un conjunto unificable de ecuaciones de átomos fyi 4’i, .. ,yk 4’~}, donde y~ y -‘4’~ son dos literales que aparecen en .B~, 1 < < k

Read More

MÉTODO ANALÓGICO 07/03/2017

Método Analógico

Juan Carlos Gomez Sanchez

cod:20162578095

5 software para realizar tablas de verdad

Anallogica:

Aplicación para generar tablas de verdad - o tablas lógicas.

Anallogica es una aplicación diseñada para generar tablas lógicas a partir de proposiciones lógicas, verificar equivalencias o valores lógicos inversos.

Es posible guardar los resultados en archivos de texto(*.txt),en planillas de calculo (*.csv para abrir con excel y office) y en un binario propio del programa.

El programa admite hasta 15 variables diferentes, lo que en combinaciones serían más de 32.000 posibilidades.

Asimismo Anallogica muestra los reemplazos realizados paso a paso para el análisis, una función especial para estudiantes.

Multisim:

En el Convertidor Lógico en Multisim se pueden realizar varias transformaciones de un circuito o señal digital. Puede crear una tabla de verdad o expresión Booleana a partir de un circuito digital o bien producir un circuito desde una tabla de verdad o expresión Booleana.

GKMap:

software libre disponible para linux y windows: http://sourceforge.net/projects/gkmap/

Para instalar este programa en ubuntu debemos compilarlo a partir del código fuente, ya de paso explicamos cómo hacer para instalar aplicaciones por este método:

WinLogiLab:

Es Freeware,WinLogiLab se compone de un conjunto de tutoriales que utiliza alumnos proporcionado datos de entrada, para llevar a cabo los pasos iniciales para el diseño digital de circuitos lógicos combinatorios y secuenciales.

Boole-Deusto:

Freeware, también muy bueno!, no sólo podemos simplificar funciones mediante los mapas de Karnaugh, si no que podemos representar la función algebraica mediante compuertas lógicas:

Read More