REGLES D'INFERENCIA (ILO) −Eliminació de " m A"B −Introducció de " m+1 A E " m m A {derivada de les anterior} −Eliminació " nB m A"B n+1 A"B I " m, n m+1 A H −Introducció " nC mA n+1 B H m+1 A"B I " m pC B= fòmula arbitaria vàlida p+1 C E " m, n, p −Introducció ! PC m, n, p mAH −Eliminació ! (modus ponens MP!m, n) nB mA n+1 A!B I ! m, n n A!B n+1 B E ! m, n −Introducció ¬ (reducció a l'absurd) mAH

−Eliminació ¬ (doble negació)

nB

m ¬¬A

p ¬B

m+1 A E ¬ m

q ¬A I ¬ m, n, p

Dn m

RA ¬ m, ,n, p REGLES SECUNDÀRIES O DERIVADES 1.− Quodlibet sequitur, o eliminació feble de la negació (QS): mA

•AH • ¬A H • ¬B H • A IT 1 • ¬A IT 2 1

n ¬A

• ¬¬B I ¬ 3, 4, 5 • B E¬6

n+1 B QS m, n On B és una fòrmula arbitraria 2.− Sil−logisme hipotetic (SH): mA!B nB!C n+1 A ! C SH m, n 3.− Sil−logisme disjuntiu (SD): mA"B n ¬A n+1 B SD m, n 4.− Modus tollens (MT): mA!B n ¬B n+1 ¬A MT m, n 5.− Resolució, versió medieval(RS): mA!B n ¬A ! B n+1 B " C RS m, n

6.− Resolució, versió Genzen−Quine (RS) m ¬A " B nA"C n+1 B " C

7.− Regla d'incompatibilitat (IC):

• A!B H • B!C H •AH • B E! 1,3 • C E!2, 4 • A!C I! 3, 5 • A"B H • ¬A H •AH • ¬A IT 2 • B QS 3, 4 •BH • B IT 6 • B E" 1, 5, 7 • A!B H • ¬B H •AH • B E! 1, 3 • ¬B IT 2 • ¬A I¬ 3, 4, 5 • A!B H • ¬A!C H • A"¬A T •AH • B E! 1, 4 • B"C I" 5 • ¬A H • C E! 2, 7 • B"C I" 8 • B"C E" 3, 6, 9 • ¬A"B H • A"C H • ¬A H •AH • ¬A IT 3 • B"C QS 4, 5 •CH • B"C I" 7 • B"C PC 2, 6, 8 •BH • B"C I"10 • B"C PC 1, 9, 11 • ¬(A"B) H •AH 2

m ¬(A"B) nA

•BH • A"B I" 2, 3 • ¬(A"B) IT 1 • ¬B I¬ 3, 4, 5

n+1 ¬B IC m, n 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.

3

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.

4

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 2.−Eliminació de l'existencial n "x Ax n+1 Aa E " n 1.−Introducció de l'existencial n At n+1 "x Ax I " n t és qualsevol

Sempre que a sigui una constant nova n "x Ax p At qB 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Ó

5

·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)

6

"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 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. 7

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

8