PROLOG

1-) INSTALAR PROLOG ✔

2-) APRENDER A USAR ✔

3-) ¿QUE ES PROLOG?

Prolog es un lenguaje de programación lógica cuya primera versión fue desarrollada a principios de la década de 1970 por Colmerauer en la universidad de Marsella. Contrariamente a otros lenguajes de programación basados es estructuras de control y definición de funciones para calcular resultados, Prolog está orientado a la especificación de relaciones para responder consultas. En ese sentido Prolog es similar a un sistema de base de datos, aunque en el contexto de la inteligencia artificial se prefiere hablar de bases de conocimiento, enfatizando la complejidad estructural de los datos y de las deducciones que se pueden obtener de ellos.

Por ejemplo, para especificar la relación el padre de X es Y, se crea una base de conocimiento con hechos expresados mediante un predicado padre(X,Y) de la siguiente manera:

padre(juan,pedro).
padre(josé,pedro).
padre(maría,pedro).
padre(pedro,pablo).
padre(ana,alberto).
...

Esto es muy parecido a crear una tabla en una base de datos, sólo que cada caso se  especifica mediante una cláusula independiente terminada por '.' . Si además se quiere incorporar conocimiento sobre la madre, se puede proceder de la misma manera agregando por ejemplo:

madre(juan,ana).
madre(josé,ana).
madre(maría,ana).
madre(pedro,juanita).
madre(ana,julia).
...

En prolog todas las cláusulas terminan con el delimitador '.' . Las cláusulas de consulta se interpretan como ecuaciones lógicas y pueden incluir variables. Por ejemplo:

?- padre(maría,pablo).

No
?- padre(ana,alberto).

Yes
?- padre(maría,X).

X = pedro ;

No
?- padre(X,Y).

X = juan
Y = pedro ;

X = josé
Y = pedro ;

X = maría
Y = pedro ;

X = pedro
Y = pablo ;

X = ana
Y = alberto ;

No

EJEMPLO:

% La sintaxis es factorial(N, F) -> Factorial de N es F (el resultado se guarda en F)factorial(0, 1).factorial(1, 1).factorial(N, F) :- N>0, N1 is N - 1, factorial(N1, F1), F is N * F1. %el factorial se llama recursivamente dejando el resultado en F

4-) ¿CUAL ES LA RELACIÓN ENTRE PROLOG Y LÓGICA PREDICADOS?

Algoritmo de búsqueda
********************

Un query consise en una conjunción de predicados que Prolog debe
demostrar que es verdadero, mostrando además las restricciones bajo
las cuales se cumple.

Ejemplo 1:

1.- member(2,[1,2,3]).

  Se considera (A): no unifica
  Se considera (B): unifica con X=2, L=[2,3]
  Se insertan las condiciones de (B) en la lista de metas reemplazando
  la variables pro las restricciones.

  2.- member(2,[2,3]).

    Se considera (A): unifica con X=2, L=[3].
    Como no hay condiciones => exito.
    El interprete arroja yes.

Read More

FORMA NORMAL DE SKOLEM 02/05/2017

1. Formula Normal de Skolem

1. Definición de una FNS: Una formula de la lógica de primer orden se considera expresada en forma normal de Skolem si su forma normal prenexa solamente contiene cuantificadores universales. Una fórmula puede ser Skolemizada, lo que implica que sus cuantificadores existenciales son suprimidos, produciendo una nueva fórmula equisatisfactible con respecto a la original.
2. 
   
3. Como encontrar la FNS: Para encontrar la forma normal de Skolem de una fórmula es la eliminación de los cuantificadores existenciales, esta eliminación es conocida como skolemización. Las reglas básicas para realizar la skolemización son 3
4. 1- Si un cuantificador existencial no se encuentra dentro del ámbito de ningún cuantificador universal, se sustituye la variable cuantificada existencialmente por una constante Por ejemplo, puede ser cambiado a P(c),
5. 2: Si un cuantificador existencial se encuentra dentro del ámbito de un cuantificador universal, se ha de sustituir la variable cuantificada existencialmente por una función de la variable cuantificada universalmente y se elimina el cuantificador existencial. Por ejemplo, la fórmula no está en forma normal de Skolem porque ella contiene un cuantificador existencial
6. 3: Si un cuantificador existencial se encuentra dentro del ámbito de más de un cuantificador universal se sustituirá la variable cuantificada existencialmente por una función de todas las variables afectadas por estos cuantificadores universales y se elimina el cuantificador existencial.
7. 
   
8. Ejemplo para encontrar FNS
9. Uso de la skolemización Uno de los usos de la skolemización es aplicarlo en el método de resolución de la lógica de predicados que se basa en:
10. 1. Una única regla: la de resolución. 
11. 2. Una única estrategia: la reducción al absurdo. 
12. 3. La utilización de la forma normal de Skolem (FNS) con la matriz en forma normal conjuntiva(FNC ). 
13. 4. La utilización del replanteamiento de la última decisión para garantizar la sistematicidad.
14. 5. El cálculo de sustituciones y el algoritmo de unificación.

sustitución:

1. Si un cuantificador existencial no se encuentra dentro del ámbito de ningún cuantificador universal, se sustituye la variable cuantificada existencialmente por una constante que aún no haya sido utilizada y el cuantificador existencial es eliminado. La constante utilizada no puede volver a ser reutilizada. Por ejemplo, ${\displaystyle \exists xP(x)}$ puede ser cambiado a P(c), donde c es una nueva constante.
2. Si un cuantificador existencial se encuentra dentro del ámbito de un cuantificador universal, se ha de sustituir la variable cuantificada existencialmente por una función de la variable cuantificada universalmente y se elimina el cuantificador existencial. La función no puede haber sido utilizada previamente ni podrá utilizarse posteriormente. Por ejemplo, la fórmula ${\displaystyle \forall x\exists y\forall z.P(x,y,z)}$ no está en forma normal de Skolem porque ella contiene un cuantificador existencial ${\displaystyle \exists y}$. La skolemización reemplaza ${\displaystyle y}$ con ${\displaystyle f(x)}$, donde ${\displaystyle f}$ es una nuevo símbolo de función, y elimina la cuantificación existencial sobre ${\displaystyle y}$. La fórmula resultante es ${\displaystyle \forall x\forall z.P(x,f(x),z)}$. El término Skolem ${\displaystyle f(x)}$ contiene ${\displaystyle x}$ pero no ${\displaystyle z}$ porque el cuantificador a ser eliminado ${\displaystyle \exists y}$ está en el ámbito de ${\displaystyle \forall x}$ pero no en el ámbito de ${\displaystyle \forall z}$; debido a que la fórmula está en forma normal prenexa, esto es equivalente a decir que, en la aparición de los cuantificadores, ${\displaystyle x}$ precede ${\displaystyle y}$ mientras ${\displaystyle z}$ no. La fórmula obtenida por esta transformación es satifactible si y solo si la fórmula original lo es.
3. Si un cuantificador existencial se encuentra dentro del ámbito de más de un cuantificador universal se sustituirá la variable cuantificada existencialmente por una función de todas las variables afectadas por estos cuantificadores universales y se elimina el cuantificador existencial. La función no puede haber sido utilizada previamente ni podrá utilizarse posteriormente

conjunto de diferencias:

unificación algoritmo:

Sabemos que “Una fórmula F es satisfacible sii FNS(F) es satisfacible” y que “FNS(F) existe siempre para cualquier fórmula F”, luego podemos trabajar exclusivamente con fórmulas en forma normal de Skolem. 

Para trabajar más cómodamente con fórmulas en FNS utilizaremos la forma clausular

La mayoría de procedimientos de prueba operan por refutación. Estas pruebas se aplican a formulas en una forma denominada forma clausal. 

Cláusula: Una cláusula es una disyunción finita de cero o más literales. Cuando la cláusula está compuesta de un solo literal diremos que es una cláusula unitaria. C = L1∨…∨Ln, Li(1≤i ≤n) literal 

La forma clausular de una fórmula F, FC(F), es el conjunto de cláusulas de la FNS(F). 

La forma clausular se entiende como la conjunción de las cláusulas, cuyas variables están todas ellas ligadas universalmente. 

Read More

VARIABLE LIBRE Y LIGADA 25/04/2017

VARIABLE LIBRE Y LIGADA

Variable libre: Es una variable de la cual no se conoce su tipo ni su valor. Este tipo de variable no interviene ni en las proposiciones ni en los predicados. 

Variable ligada: Son las variables que no son libres. Una variable ligada está determinada por una definición anterior, que le asigna un valor. A partir de ello se pueden formular proposiciones en donde intervengan variables ligadas. 

-Debemos distinguir entre variables que son cuantificadas y las que no lo son; y saber con precisión cuál cuantificador controla en una expresión o una o varias variables.

Definición:

La expresión a la cual el cuantificador se aplica es el dominio del cuantificador; y una ocurrencia de una variable individual x está ligada  si aparece como  o  o dentro del dominio de un o . Cualquier otro tipo de ocurrencia de una variable es una ocurrencia libre.

Definición:
Inductiva conjunto de VL(A) conjunto de variables libres de A.
1. Si A es atómica VL(A):= conjunto de todas las variables que aparecen en un A.
2. Si A es ¬B entonces VL(A):= VL(B)
3. Si A es (B*C) donde * es cualquier conectivo binario, entonces VL(A):= VL(B) U VL(C)
4. Si A es B o B entonces VL(A):= VL(B) - {x}
    Si  es una proposición; sino es una forma proposicional.
Ejemplo:
                                         

Equivalencias
    Sentencia
            
 
    Significado
    a) Todos son verdaderos 
     b) Al menos uno es verdadero 
     c) Todos son falsos 
     d) Al menos uno es falso 
     e) No todos son verdaderos 
     f) Ninguno es verdadero 
     g) No todos son falsos 
     h) Ninguno es falso 
 

a) Si existe un ganador, entonces ninguno otro es ganador.

 


Si está determinada una posición, nadie más tiene esa posición.
b) El producto de dos números reales es un número real.



Para ningún par de números reales el producto no es real.

• El orden cuantificador iguales no importa
• El orden sí importa cuando los cuantificadores son diferentes

c) 
 En los enteros para todo x existe algún y talque x+y=5. Verdadero.
 Existe algún y talque para cualquier x x+y=5. Falso 
 
Negaciones
    Sentencia
           
    Negación
        

Equivalencias Lógicas.

•Definición: Dos formas proposicionales P y Q se dicen lógicamente equivalentes, y se escribe P ≡ Q, si sus tablas de verdad coinciden.

Nota:
Esto equivale a decir que P ↔ Q es una tautología; así, P ≡ Q es lo
mismo que decir P ⇔ Q.

EJEMPLO:

El programa está bien escrito y bien documentado.
El programa está bien documentado y bien escrito.

• LEYES DE MORGAN•

1. ~ (p ∨ q) ≡~ p∧ ~ q –  A continuación se muestra en su tabla correspondiente:

• TRANSPOSICION O CONTRARECIPROCO•

•Definición: La contrarrecíproca o trasposición de una proposición
condicional p → q es la proposición  ~q →~p
Teorema: La proposición condicional p → q y su contrarrecíproca
~q →~p son lógicamente equivalentes. A continuación se muestra en su tabla correspondiente:

• ELIMINACION DE CONDICIONALES•

P → Q ≡~P ∨ Q     – A continuación se muestra en su tabla correspondiente:

LEYES DE LA LÓGICA

• Leyes de absorción:

P ∨ (P ∧ Q) ≡ P
P ∧ (P ∨ Q) ≡ P
• P ∨ (P ∧ Q) ≡ (P ∧ V ) ∨ (P ∧ Q) Ley de identidad
• P ∧ (V ∨ Q) Ley distributiva
• P ∧ V Ley de dominación
• P Ley de identidad

Read More

LÓGICA DE PREDICADOS 04/04/2017

LÓGICA DE PREDICADOS 

SINTAXIS:

-TÉRMINOS: representan objetos del dominio 

-CONSTANTES: representan un objeto individual en concreto notación: cadenas de caracteres, comienzan en mayúsculas.

NOTACIÓN: cadenas de caracteres, comienzan en mayúsculas

ejemplo: Juan; Mi coche;...

-FUNCIONES: representan (implícitamente) un objeto individual que esta relacionado con los n objetos que participan en la función

NOTACIÓN: símbolo de función (cadena, comienza con mays.) con aridad n+n argumentos (términos) entre paréntesis

ejemplo: Padre de (Juan); Hijo de (Pedro; Ana); Coseno (45)...

-VARIABLES: representan objetos sin indicar cuales 

-PREDICADOS: representan una propiedad de un termino (si aridad 1) o relaciones entre K términos (variables, constantes, funciones) entre paréntesis.

-ÁTOMOS: formulas bien formadas (f. b. f.) compuestas por un único predicado 

-LITERALES: Átomo o negación de un átomo.

ejemplos: Asesina (Juan; x); Es_alto (Juan);Vive_con (Juan;Padre_de(Juan));...

CREACIÓN F. B. F. (formulas bien formadas)

Una fórmula bien formada –designada FBF- es una cadena de símbolos formada según reglas precisas. Una FBF es una forma enunciativa, llamada también forma proposicional o simplemente proposición. Definición: Una fórmula bien formada del cálculo proposicional se define mediante las siguientes reglas:

1) Una variable proposicional aislada es una FBF. 2) Si p es una FBF, entonces (~p) es una FBF. 4) Una cadena de símbolos es una FBF, si y sólo si resulta de un número finito de aplicaciones de las reglas 1, 2 y 3. "Una fórmula bien formada puede ser: tautología (identidad lógica), contradicción o contingencia (ecuación lógica)". Aunque el sistema de puntuación básico usado consiste de paréntesis ( ), corchetes [ ] y llaves { }; todos ellos pueden reducirse sólo al uso de paréntesis. Pero, si bien se reduce el número de símbolos, los paréntesis abundarían de tal manera que sería imposible responder si hay paréntesis redundantes o paréntesis incompletos. Esta puntuación representa una dificultad añadida para determinar si una fórmula está bien formada. Para solucionar este problema Lukasiewiks propuso una notación libre de paréntesis denominada notación polaca o notación prefija. En el caso general, a una FBF en la que intervengan n variables de enunciado diferente (siendo n cualquier número natural) le corresponderá una función de verdad de n argumentos, y la tabla de verdad tendrá 2n filas, una para cada una de las posibles combinaciones de valores de verdad para las variables de enunciado. Nótese además que existen funciones de verdad distintas de n argumentos, que corresponden a las maneras posibles de disponer los 1’s y los 0’s en la última columna de una tabla de verdad de 2n filas. Esta claro que el número de formas enunciativas que se pueden construir utilizando n variables de enunciados es infinito, así que formas enunciativas distintas pueden corresponder a una misma función de verdad. Una FBF es una tautología si toma el valor de verdad bajo cada una de las posibles asignaciones de valores de verdad a las variables de enunciado que aparecen en ella. Una FBF es una contradicción si toma el valor de verdad 0 bajo cada una de las posibles asignaciones de valores de verdad a las variables de enunciado que aparecen en ella.

 

Read More

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