Filosofía
Logica. Regles d'inferencia (ILO)
REGLES D'INFERENCIA (ILO)
| -Introducció de " m A {derivada de les anterior} n B n+1 A"B I " m, n -Introducció " m A m+1 A"B I " m B= fòmula arbitaria vàlida -Introducció ! m A H n B n+1 A!B I ! m, n | -Eliminació de " m A"B m+1 A E " m -Eliminació " m A"B m+1 A H n C n+1 B H p C p+1 C E " m, n, p PC m, n, p -Eliminació ! (modus ponens MP!m, n) m A n A!B n+1 B E ! m, n |
| -Introducció ¬ (reducció a l'absurd) m A H n B p ¬B q ¬A I ¬ m, n, p RA ¬ m, ,n, p | -Eliminació ¬ (doble negació) m ¬¬A m+1 A E ¬ m Dn m |
REGLES SECUNDÀRIES O DERIVADES
| 1.- Quodlibet sequitur, o eliminació feble de la negació (QS): m A n ¬A n+1 B QS m, n On B és una fòrmula arbitraria | A H ¬A H ¬B H A IT 1 ¬A IT 2 ¬¬B I ¬ 3, 4, 5 B E¬6 |
| 2.- Sil-logisme hipotetic (SH): m A ! B n B ! C n+1 A ! C SH m, n | A!B H B!C H A H B E! 1,3 C E!2, 4 A!C I! 3, 5 |
| 3.- Sil-logisme disjuntiu (SD): m A " B n ¬A n+1 B SD m, n | A"B H ¬A H A H ¬A IT 2 B QS 3, 4 B H B IT 6 B E" 1, 5, 7 |
| 4.- Modus tollens (MT): m A ! B n ¬B n+1 ¬A MT m, n | A!B H ¬B H A H B E! 1, 3 ¬B IT 2 ¬A I¬ 3, 4, 5 |
| 5.- Resolució, versió medieval(RS): m A ! B n ¬A ! B n+1 B " C RS m, n | A!B H ¬A!C H A"¬A T A H B E! 1, 4 B"C I" 5 ¬A H C E! 2, 7 B"C I" 8 B"C E" 3, 6, 9 |
| 6.- Resolució, versió Genzen-Quine (RS) m ¬A " B n A " C n+1 B " C | ¬A"B H A"C H ¬A H A H ¬A IT 3 B"C QS 4, 5 C H B"C I" 7 B"C PC 2, 6, 8 B H B"C I"10 B"C PC 1, 9, 11 |
| 7.- Regla d'incompatibilitat (IC): m ¬(A"B) n A n+1 ¬B IC m, n | ¬(A"B) H A H B H A"B I" 2, 3 ¬(A"B) IT 1 ¬B I¬ 3, 4, 5 |
FORMALITZACIÓ
-Conujunció: (A) i (B) __! A"B
-Disjunció: (A) o (B) __! A"B
-Negació no/ no es el cas que (A) __! ¬A
-Condicional:
·de suficiencia: A ! B
Si (A) aleshores (B);
Es suficient (A) per (B);
Si (A), (B);
Quan (A) aleshores (B).
·de necesitat: B ! A
Cal (a) per (B);
Es necesari (A) per (B);
Només (A) quan (B);
Només si (A) passa (B).
· d'exclusió: ¬B ! A
(A) llevat que (B);
(A) excepte quan (B).
DEDUCCIÓ NATURAL
Regles pràctiques:
1.- A"B C ; processos per cassos sobre A i B.
2.- A A"B ; intentar derivar A o B.
3.- A B!C ; fer una subordinada amb B com hipotesis.
4.- A B"C ; derivar B i derivar C.
5.- A ¬B ; reducció a l'absurd per hipotesis de B.
6.- Quan tot falla aplicar 5 fent com la hipotesis que tenim la egada d'allò que es vol obtenir.
ALGEBRA DE BOOLE
1.-Commutativa: a"b = b"a; a"b = b"a.
2.-Distributiva: a"(b"c) = (a"b) " (a"c); a"(b"c) = (a"b) " (a"c).
3.-Existeix neutre: a"=a; a"=a.
4.-Complementació: a"¬a=; a"a=.
5.-Idempotència: a"a = a; a"a = a.
6.-Asociativitat: a"(b"c) = (a"b)"c; a"(b"c) = (a"b)"c.
7.-Absorció: a"(b"a) = a; a"(b"c) = a.
8.-Involució: ¬¬a= a.
9.-Lleis de De Morgan: ¬(a"b) = ¬a"¬b; ¬(a"b) = ¬a"¬b.
10.-Infim: a"ÿ =ÿ; a"ÿ = a.
11.-Suprem: a" = a; a" = .
RESOLUCIÓ
A1, A2,..., An B sii A1, A2,..., An, ¬B sii C1, C2,..., Cm
1.- Gnerar un arbre
2.- mentre no trobar i resten arbres fer
generar següent arbre
fmentre
si trobada ! C1,..., Cm inconsistents ; A1,..., An b
¬trobada ! C1,..., Cn consistent ;A1,..., An B
fsi
Metodologia mecànica :
1.- Formalitzar el problema.
2.- Clausularització del seqüent.
3.- Simplificació inicial (tautologies,literals purs i subsumpció).
4.- Estudi de la consistencia de les hipotesis
5.- si premises consistents llavors
validació del seqüent usant, com a conjunt de suport les clausules provinents de ¬B.
fsi
REGLES D'INFERENCIA DEL CP1
| 1.-Introducció de l'existencial n At n+1 "x Ax I " n t és qualsevol | 2.-Eliminació de l'existencial n "x Ax n+1 Aa E " n Sempre que a sigui una constant nova n "x Ax p At q B q+1 B E " n, p, q t és un terme arbitrari tal que no apareix ni fora de la subdemostració ni en la fòrmula B |
| 3.- Introducció de l'universal n Au n+1 "x Ax I " n u és una variable tal que no apareix lliure en cap premisa | 4.-Eliminació de l'universal n "x Ax n+1 At E " n t és qualsevol terme |
Metodologia Pràctica de DN en CP1 :
-Eliminar els quantificadors de les premises
-Aplicar regles del CP0 suposant que els valors de les variables estàn fixats fins arribar a la conclusió sense quantificadors.
-Introducció dels quantificadors.
FORMALITZACIÓ
·Universal o generalitzador (") :inidica que tots els elements del domini verifiquen un propietat. La forma característica simple es :
Per tot element del domini, x, es verifica Px. "xPx
Aquest quantificador es pot representar en llenguatge natural per :
Per tot, per a cada, cada, tot, qualsevol, ect.
La forma característica general és :
Per tot element del domini, x, es verifica que si Px aleshores es verifica Qx. "x (Px ! Qx).
·Existencial o particularitzador (") :indica que un determinat terme verifica un predicat concret. La forma característica simple es :
Hi ha al menys un element del domini, x, tal que verifica Px.
Aquest quantificador es pot representar en llenguatge natural per :
Existeix, per a algún, hi ha algún, algún, etc.
La forma carcaterística general és :
Hi ha al menys algún element del domini, x, tal que verifica Px i Qx. "x(Px " Qx).
FORMA NORMAL PRENEXA
El procediment pel qual es pot passar d'una fòrmula qualsevol a la seva FNPC o FNPD equivalent és :
Eliminació de ! i ! aplicant els equivalents deductius.
Moure la conectiva ¬ fins que afecti només als àtoms, aplicant les lleis de DeMorgan.
Rebatejar variables si cal :cambiar el nom de les variables que amb el mateix simbol estàn quantificades més d'una vegada.
Moure quantificadors a l'esquerra.
Repetir els passos anteriors tantes vegades com calgui fins obtenir la FNPC o FNPD.
EQUIVALENCIES DEDUCTIVES
Les fórmules del CP1 no són algebra de Boole per tant no s poden aplicar l'associativitat, distributivitat, etc. Però tenen altres propietats :
"x "y Axy "y"x Axy
"x "y Axy "y"x Axy
¬"x Ax "x ¬Ax
¬"x Ax "x ¬Ax
A!"x Bx "x (A!Bx)
A!"x Bx "x (A!Bx)
"x Ax!B "x (Ax!B)
"x Ax!B "x (Ax!B)
Rebateig de variables : "x Ax " "x Bx "x"y (Ax " By)
"x Ax " "x Bx "x"y (Ax " By)
FORMES D'SKOLEN
L'algorisme per generar la FNS per una fórmula A arbitraria del CP1 és el següent :
Tancar A existencialment.
Eliminar els quantificadors redundants.
Rebateig de variables.
Eliminació de condicional i bidireccional.
Moure negacions de manera que afecti als àtoms.
(Opcional) Mure quantificadors a la dreta.
Skolemització : eliminació dels existencials.
Avançar els universals a l'esquerra.
Escriure la matriu en FNC
Simplificació de la matriu, si cal.
UNIFICACIÓ
Algoritme unificació (p1, p2, )
si P1=P2 ---> retorna ()
sino determinar primer parell discrepant <t1, t2>
si t1 és variable i no ocorre en t2 --> unificació (P1(t2/t1), P2(t2/t1), " (t2/t1))
sino t2 és variable i no ocorre en t1 --> unificació (P1(t1/t2),P2(t1/t2), " (t1/t2))
sino retorna (no unificable) ;
fsi
fsi
falgoritme
ESTRATEGIES DE RESOLUCIÓ EN CP 1
Estrategies de simpificació :
1.- Regla del literal pur. Tota clausula amb un literal pur no cal considerar-la.
2.- Tautologies. Les clausules que contenen tautologies no cal considerar-les. Pxy " ¬Pxy tautologia Px " ¬Pu no tautologia.
3.- Subsumpció : Les clausules subsumides per altres clasusules no cal considerar-les. Una clausula subsumeix a una altra si i nomes si la clausule que subsumeix és unificable amb la clausula subsumida
Estrategies de control :
1.- Reducció lineal.
2.- Arbre binari amb clausula troncal la resolvent del pas anterior.
3.- Resolució ordenada (literal de l'esquerra o de la dreta).
4.- Resolució amb conjunt de suport. Donat un conjunt de clausules, si troben un subconjunt consistent (no es dedueix la caixa buida) llavors el conjunt de suport és el conjunt total de clausules excepte aquest subconjunt consistent.
3
Descargar
| Enviado por: | Alberto Seco |
| Idioma: | catalán |
| País: | España |
Todos los derechos reservados.