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