INTRODUCCIÓ A LA LOGICA

1.- CÀLCUL DE PORPOSICIONS D' ORDRE 0 (CP0)

CÀLCUL PROPOSICIONAL

CÀLCUL D'ENUNCIATS

-LLENGUATGE DEL CP0

-FORMALITZACIÓ DEL LLENGUATGE NATURAL

-VALIDACIÓ DE RAONAMENTS

2.- TEORIA DE LA DEMOSTRACIÓ

-DEDUCCIÓ NATURAL

-EQUIVALENCIA DEDUCTIVA

-ALGEBRA DE BOOLE

-FORMES NORMALS

3.- DEMOSTRACIÓ AUTOMÀTICA

-RESOLUCIÓ

4.- CÀLCUL DE PREDICATS DE PRIMER ORDRE (CP1)

-PREDICAT

-DOMINI

-LLENGUATGE DEL CP1

-FORMALITZACIÓ DEL LLENGUATGE NATURAL

5.- TEORIA DE LA DEMOSTRACIÓ

-DEDUCCIÓ NATURAL

-EQUIVALENCIA DEDUCTIVA

-FORMES NORMALS

6.- DEMOSTRACIÓ AUTOMÀTICA

-FORMES NORMALS D'SKOLEN

-UNIFICACIÓ

-RESOLUCIÓ

7.- TEORIES

-DEFINICIÓ

-EXEMPLE

1.- CÀLCUL DE PROPOSICIONS DE ORDRE 0 (CP0)

Lògica: preten estudiar quines coses es deriven de quines altres, vol dir validar raonaments a partit d'unes condicions previes que s'accepten.

Matemàtica: aplica processos matemàtics per fer validacions.

Binària: els elements només poden tomar valors d'un conjunt binari.

Elemental: només estudiem lògica binaria del cp0 i del cp1.

LLENGUATGE DEL CP0

En el llenguatge natural (LN) hi han tres tipus d'enunciats:

·Enumeratius o declaratius (apofàntics) vol dir que pertany al grup binari.

·Interrogatius.

·Imperatius.

Un exemple de raonament en LN és el següent:

Quan plou la Mariona porta katiusques.

Avui plou._____________________________

La Mariona porta katiusques.

El llenguatge usat en CP0 es genera a partir d'un alfabet que conté les connectives lògiques, els parèntesis i lletres d'àtoms. El llenguatge generat conté enunicats (fórmules).

En el llenguatge del CP0 intervenen els següents elements:

-Elements de vocabulari (alfabet del CP0) són:

1) Les connectives (" conjunció, " disjunció, ! condicional o si...llavors, ¬ negatiu)

2) Parèntesis ( )

3) Constants: llegit caixa buida o contradicció

llegit caixa plena o tautologia

4) Lletres d'enunciat o proposicionals: P, Q, R, S, T ....

Per tant l'alfabet de la lògica és "={", ", !, ¬, , , P, Q, R ...}

-Elements del llenguatge anomenats fórmules o enunciats:

1) Formules atòmiques o àtoms: és una lletra de proposició una constant. És la formalització d'una frase declarativa que no es pot descompondre en altres frases més simples.

2) Formules ben formades (fbf o wff): són el mínim conjunt P de fórmules tals que:

1- Si A és una fórmula atómica aleshores A " P. Tot àtom és un enunciat.

2- Si A " P aleshores ¬A " P. Si A és un enuciat, aleshores (¬A) també ho és.

3- Si A, B " P aleshores (A"B) " P, (A"B) " P, (A!B) " P.

4- Les fórmules generades segons les regles anterior són les úniques en P.

La simplificació de la notació es fa en dues pasos:

- Es defineixen prioritats: més baixa !, ", ", ¬, ( ) més alta

- Eliminació de parèntesis exteriors i s'eliminan parèntesis interiors quan no hi ha possibilitats de confusió

P"(Q!R), P"Q!R són fórmules ben formades però no diuen el mateix.

Conectors auxiliars:

- O exclusiva. És P o Q però no totes dues a l'hora. Aquesta es pot expresar en funció de les altres i per això quasi no la utilitzem.

P"Q = P"Q = (P"Q) " ¬(P"Q)

- Bicondicional o equivalencia, és el si i només si.

P!!Q = (P!Q) " (Q!P)

Metallenguatge: és un llenguatge usat per descriure un altre llenguatge.

FORMALITZACIÓ DEL LLENGUATGE NATURAL

Al llenguatge natural es distingeixen les proposicions (acte declaratiu amb el qual es diu alguna cosa). Nosaltrs només ens interesa les proposicions apofàntiques (que només prenen valors dintre d'un conjunt bnari):

Joan estima l'Anna Declaren la mateixa cosa , per tant

L'Anna es estimada pel Joan són les mateixes proposicions.

D'una proposició no ens importa la forma de com està escrita sinó el seu contingut, el que ens vol dir.

Formalització: acció de donar estrauctura concreta i realitzable (o efectiva). Formalitzar per nosaltres serà la traducció dels enunciats apofàntics del llenguatge natural segons la sintaxi del CP0.

Classificació dels enunciats o proposicions del llenguatge natural:

-Proposicions atòmiques o simples: quan no te cap connectiva (i, o, si..llavors, negació no)

P= Joan estima l'Anna -> formalització atòmica o proposicional

-Proposicios moleculars simples: construides a base de dues atómiques mitançant les connectives o és una atòmica negada.

Algorisme per a la formalització del llenguatge natural:

1- Identificació de la conectiva.

2- Reescriure l'enunciat segons la forma característica.

3- Identificar les atòmiques components.

4- Formalització de les atòmiques, a cada atòmica diferent se li asigna una lletra.

5- Relacionar les atómiques segons les connectives.

Forma característica: és la forma intrinseca que produeix cada connectiva.

Estructura de les proposicions en llenguatge natural i traducció a CP0.

-Conjunció: (......) i (......)

(La primavera ha arribat) i (els arbres broten)

P " Q

-Disjunció: (......) o (......)

(La radio està avariada) o (l'emissora és dolenta)

R " S

La disjunció pot ser exclusiva com l'exemple, es a dir, que les proposicions es contradiuen, que no poden donar a l'hora. També pot ser inclusiva en la qual s'accepta com a vàlid les dues proposicions. A la lògica nosaltres sempre agafarem la disjunció inclusiva.

(El Roger menja cargols) o (calderetes)

-Condicional: si (......) llavors (.....)

Si (aquesta nit juga l'Stoichkov), (el Barça guanyarà)

P ! Q

-Negació: no (.....); no és el cas que (.....)

No (pujaré a la torre Eiffel) -> ¬P

Mart no és tan proper al Sol com ho és la Terra. Aquest exemple no correspon amb l'esquema, però es pot transformar per:

No (Mart és tan proper al Sol com la Terra)

2.- TEORIA DE LA DEMOSTRACIÓ

L'objectiu de la teoria de la demostració és definir procesos que permetin estudiar quines coses es deriven de quines coses. Definir processos que permetin obtenir conclussions d'unes premisses.

Sistema deductiu: representació formal que permet representar processos de raonament que permet obtenir conclussions a partir de premisses. Els processos de raonament queden definits per:

-Axiomes.

-Regles d'inferència o regla de deducció.

-Mètode de representació.

Per a que això sigui util cal que tinguin tres propietats:

-Sigui correcte o consistent: quan no permet obtenir una fòrmula i la mateixa fòrmula negada.

-Sigui comlet, qualsevol fòrmula vàlida s'ha de poder demostrar que és vàlida.

-Sigui decidible, que espugui definir si un raonament és vàlid o no en un nombre de passes finits.

Conseqëùencia lògica: a partir d'unes premisses es deriva una altra fórmula a partir d'unes regles. Primer cal definir:

·Regles d'inferència: conjunt finit de regles que defineix com s'obtenen fòrmules vàlides a partir d'unes altres vàlides.

·Premisses: fòrmules que et donen com a dades i que no es poden discutir, es a dir, te les donen a priori.

·Deducció: llista de fòrmules o enunciats ordenades tals que o són premisses o són fórmules derivades de les anteriors per aplicació de les regles.

·Demostració: obtenció d'una fórmula B a aprtir d'un conjunt de premisses concretes (A1...An) a partir de processos de deducció.

Una fórmula B és conseqüència lògica d'un conjunt de premisses A1...An si i només si existeix una demostració de B a partir de A1...An. A1...An B.

Un seqüent és A1...An B, l'antecedent és A1...An i el succedent és B. Els seqüents són vàlids si està demostrada si i nomes si el succedent ´s conseqüència de l'anteceent.

DEDUCCIÓ NATURAL

La deducció natural intenta representar de la forma més estricte els predicats del llenguatge natural. Per definir-lo:

1.- Axiomes: no hi ha

2.- Metodologia de representació, procediment o disposició pràctica. S'utilitzen les taules de deducció natural:

nº ordinal	Fòrmules	Regla
21	Només una formula	Regla que ha permés deduir la fórmula

Una subdemostració o demostració subordinada és una demostració dintre d'una altra demostració més gran.

Nº ordre	Fòrmules	Regla
m	A	Hipoteisi (H)

3.- Regles d'inferencia: permeten introduir i eliminar, del procés de demostració, fòrmules amb connectives:

-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

-Iteració: només es pot iterar “cap a dins”. Només d'una demostració a una subdemostració i no pas d'una subdemostració a una demostració.

TEOREMA: és tot enunciat A demostrable sense cap premisa, tmabé es poden anomenar tautologies. Aquest fet es nota per “ A”. Tot teorema és introduïble en qualsevol punt d'una demostració (cosa que es nota amb “T”). Exemples de teoremes són:

1.-Principi d'identitat (PI): A ! A

2.-Principi de no-contradicció(PNC): ¬(A " ¬A)

No acepta una fòrmula i a la vegada las eva negada.

3.-Prinicpi del tercer exclòs (PTE): A " ¬A

No és possible que hi hagi una trercera possibilitat, o la fòrmula o la seva negada.

En particular Ÿ(cert) és un teorema.

REGLES SECUNDÀRIES O DERIVADES

Són passoa de deducció que són equivalents a deduccions més complexes expresables en funció de les regles primitives:

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 3.- Sil-logisme disjuntiu (SD): m A " B n ¬A n+1 B SD m, n 5.- Resolució, versió medieval(RS): m A ! B n ¬A ! B n+1 B"C RS m, n 7.- Regla d'incompatibilitat (IC): m ¬ (A"B) n A n+1 ¬B IC m, n

2.- Sil-logisme hipotetic (SH): m A ! B n B ! C n+1 A ! C SH m, n 4.- Modus tollens (MT): m A ! B n ¬B n+1 ¬A MT m, n 6.- Resolució, versió Genzen-Quine (RS) m ¬A " B n A " C n+1 B " C

EQUIVALENCIES DEDUCTIVES

Un enunciat A és deductivament equivalent a un altre enunciat B si i només si A B i B A i es denota “ A B”.

Prinicpi de substitució: en qualsevol punt d'una deducció es pot substituir un enunciat per un altre que sigui equivalent deductiu seu (cosa que es nota per ED n on n és el número de la línia on està l'enunciat original.

Algunes equivalències deductives:

·¬(A " B) ¬A " ¬B ·¬(A " B) ¬A " ¬B

·¬¬A A ·A ! B ¬B ! ¬A ¬A " B ¬(A " ¬B)

·¬(A ! B) A " ¬B ·A ! (B ! C) B ! (A ! C).

La deducció natural és correcte si només valida seqüents vàlids, completa (si un seqüent és vàlid aleshores existeix una taula de deducció natural que el valida) però en canvi la deducció natural no és decidible.

Inconsistència: quan d'un conjunt de fórmules A1, A2...An es despren qualsevol contradicció contradicció es diu que A1, A2....An són inconsistents, insatisfactibles o contradictoris.

METATEOREMES O TEOREMES DE DEDUCCIÓ

1.- Forma simple: A B ! A!B.

2.- Forma general: A1, A2,...An B ! A1, A2,...An-1 An ! B

3.- A1, A2,...An B ! A1"A2"..."An B

4.- A1, A2,...An B ! A1"A2"..."An ! B

5.- A1, A2,...An B ! A1, A2,...An, ¬B ™ (– representa una contradicció.

ALGEBRA DE BOOLE

Un conjunt B és algebra de Boolesi hian definides dues operacions binàries +, · que compleixen les següents propietats:

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: " (zero) i I (unitat) tals que: a+"=a; a·I=a.

4.-Complementació: per tot a de B existeix una a' tal que: a+a'=I; 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·I = a; a+I = I.

LLEIS DE L'ALGEBRA D'ENUNCIATS

Es considera la opració + com la disjunció lògica " i com · la conjunció ". L'= equival a = o a . Amb aquetes conversions el conjunt B(", ") és una algebra de Boole. " equival a la caixa buida o contradicció Ÿ i I equival a la caixa plena o tautologia . La negació ` equival a ¬ i el condicional A!B equival a ¬A"B.

L'algebra del CP0 es pot considerar un sistema deductiu que permet:

a) simplificar fórmules.

b) demostrar equivalencies deductives.

FORMES NORMALS

En tota algebra de Boole es poden definir dues maneres úniques d'escriure una determinada fórmula, són les formes normals o canòniques.

La forma normal disjuntiva (FND) està representada com una disjunció de conjuncions. (a1"a2"...)"(b1"b2"...)"..."(n1"n2"...).

La forma normal conjuntiva (FNC) està representada com una conjunció de disjuncions (a1"a2"...)"(b1"b2"...)"..."(n1"n2"...).

Qualsevol fórmula del CP0 te una representació en FNC i una FND.

ALGORITME DE CONVERSIÓ EN FN

1.- Eliminar les conectives condicionals:

A!B (A!B) " (B!A)

A!B ¬A"B

2.- Moviment de les negacions (Lleis de De Morgan):

¬(A"B) ¬A " ¬B

¬(A"B) ¬A " ¬B

3.- Aplicar involució: ¬¬A A

4.- Aplica distributivitat i associativitat segons la forma normal desitjada.

3.- DEMOSTRACIÓ AUTOMÀTICA: RESOLUCIÓ

El mètode de resolució és el resultat de mecanitzar i fer sistemàtica la deducció natural. Aquest mètode és correcte, decidible (que donat qualsevol raonament vàlid el mètode troba, en un temps finit, la contradicció) i complet. L'objectiu d'aquest mètode consisteix a fer demostracions per reducció a l'absurd usant una única regla: la resolució.

n A"B {deduit de 1 a n-1}

m ¬A"C {deduit de 1 a n}

m+1 B"C RS n, m. Aquesta part és el resolvent.

Un pas de resolució es quan s'aplica un cop la regla de la resolució. Sigui S un conjunt de cláusules, aleshores un pas de resoució és l'operació d'aplicar la regla de resolució a dues clausules de S i afegir la resolvent a S.

Només és aplicable quan les fórmules estàn representades en forma normal conjuntiva.

Una clàusula és tota disjunció que és conjuntada d'una forma normal conjuntiva, és una fòrmula de la forma C=B1"B2"..."Bn on Bi és un literal entre 1"i"n.

La resolució permet decidir si un conjunt de fórmules del CP0 expresades en FNC és consistent o no. A1, A2,..., An

A1, A2,..., An B és vàlid si i només si A1, A2,..., An, ¬B , aquest mètode se'n diu refutatiu.

A1, A2,..., An, ¬B és vàlid si C1"C2"..."Cn on Ci és una clàusula derivada de les Aj.

El procés de resolució és el següent:

1.- Reescriure les fòrmules en FNC, això s'anomena la causularització.

2.- Aplicar resolució al conjunt de clàusules resultants de les hipòtesis i la negada de la conclusió.

Resolució per saturació de nivells:

P, Q, P"Q!R R " P, Q, P"Q!R, ¬R ‚ " P, Q, (¬P"¬Q"R), ¬R ‚

1. P H

2. Q H nivell 0

3. ¬P"¬Q"R H

4. ¬R H

5. ¬Q"R 1, 3

6. ¬P"R 2, 3 nivell 1

7. ¬P"¬Q 3, 4

8. R 1, 6

9. ¬Q 1, 7

10. R 1, 5 nivell 2

11. ¬P 2, 7

12. ¬Q 4, 5

13. ¬P 4,6

14. ž 1, 11

Graf de resolució: P Q ¬P"¬Q"R ¬R

¬P"¬Q (7)

¬P (11)

Ÿ

Arbre de resolució: és una altra forma de representar el procés de càlcul de deducció per resolució.

ESTRATEGIA DE RESOLUCIÓ

-Simplificació: eliminació de resolvents innecesaris.

·Eliminació de les tautologies: A"¬A

·Eliminació de literals purs. Sigui S un conjunt de cláusules, un literal és pur, si i només si apareix en alguna cláusula i no aparaeix complementat en cap altra cláusula.

·Eliminació de cláusules subsumides: Una cláusula A subsumeix una altra cláusula B si i només si totts els literals de A estan en B.

P"Q subsumeix P"Q"¬R

P"Q"R no susbsumeix P"Q"¬R

P, Q"¬Q, Q, P"¬Q, ¬P"¬Q"R, S"¬T, T"¬R, ¬R œ

1. P H

2. Q"¬Q H tautologia

3. Q H

4. P"¬Q H subsumida per 1

5. ¬P"¬Q"R H

6. S"¬T H literal pur S

7. T"¬R H literal pur T

8. ¬R H

-Estratégies de control: permeten triar cláusules a resoldre i triar la resolvent generada si hi han diverses possibilitats.

· Resolució lineal: inicialment es trien dues cláusules que es resolen, posteriorment sempre es resol la resolvent precedent amb una nova cláusula.

¬P"¬Q"R ¬R

¬P"¬Q P

¬Q Q

ž

Teorema: un conjunt de cláuslues S es insatisfactible si i nomes si existeix un arbre de resolució tal que l'arrel és la cláusula buida.

· Conjunt de suport: un conjunt de suport és un conjunt de cláusules i T és un subconjunt de S aleshores T eés un conjunt de suport de S si i només si el conjunt S-T és satisfactible.

P"Q, ¬P"Q, ¬Q"P P"Q " P"Q, ¬P"Q, ¬Q"P, ¬(P"Q) Ÿ "

P"Q, ¬P"Q, ¬Q"P, ¬P"¬Q Ÿ.

S={ P"Q, ¬P"Q, ¬Q"P, ¬P"¬Q} T={¬P"¬Q}

S-T={ P"Q, ¬P"Q, ¬Q"P}

S'ha d'estudiar si S-T ž.

1. P"Q H ž no es deriva, això implicaque S-T

2. ¬P"Q H žper tant T és un conjunt de

3. ¬Q"P H suport de S-T.

4. Q 1, 2

5. P 1,3

6.

Pas de resolució amb conjunt de suport: pas de resolució on al menys una de les clàusules és del conjunt de suport.

Resoluci´´o amb conjunt de suport és un procés de resolució on cada pas és un pas de resolució amb conjunt de suport. Cada nou resolvent és del conjunt de suport.

Teorema: Si un conjunt de clàusules S amb conjunt de suport T és insatisfactible aleshores sempre existeix un arbre de rsolució amb conjunt de suport tal que l'arrel és la caixa buida.

S={són totes les clàusules}

T={clàusules procedents de la negada del succedent} "¬B.

¬P"¬Q ¬P"Q

¬P P"Q

Q ¬Q"P

P ¬P

ž

Clàusula ordenada : una clàusula en la que els literals estàn ordenats.

L'ordre es defineix de manera posicional tal que el literal de més a l'esquerra és el més petit i el de més a ala dreta el més gran. Un pas de resolució ordenada és un pas de resolució sobre clàusules ordenades tal que sempre es resol el literal de la mateixa posició. Sempre es resol el literal més petit o el més gran.

4.- CÀLCUL DE PREDICATS DE PRIMER ORDRE (CP1)

ELEMENTS DE CP1

-Terme :expressió que designa un subjecte dins d'una proposició o enunciat. Hi han dos tipus de termes :

·Variables :termes que designen un objecte arbitrari del domini, són llocs en blanc en l'expressió d'un predicat ;ón substituïbles per valors (i llavors el predicat es transforma en una proposició). Les variables són quantificables i poden aparèixer més d'una vegada en una fórmula. Cada vegada que hi apareixen diem que hi ocorren o que hi tenen ocurrència.

·Constants :termes que designen un objecte concret del domini. No són quantificables.

-Domini :classe dels objectes admisibles com a valors de les variables. EL domini universal és el conjunt de tots els objectes imaginables, siguin o no siguin reals.

-Predicat :part de la propisició que atribueix una propietat a un subjecte (a un terme). EL predicats són del tipus n-aris. Poden ser unaris (afecten a un sol terme), binaris (afecten a 2 termes), etc. Els predicats zeronaris són de la forma P, Q, R, ..., o sigui lletres de proposició.

-Proposició atomica :un àtom es tota expressió del tipus P(t1,t2,..., tn) on P és un predicat atòmic i t1, t2,..., tn els termes.

La Joana és alta Px= x és alt j= Joana Pj.

-Quantificadors :

El CP1 introdueix el concepte de quantificació, es a dir, de mesura. Els quantificadors permeten indicar a quants termes del domini se'ls atribueix la propietat. Els quantificadors són dos :

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

-Camp d'un quantifcador :part d'una fórmula, les variables de les quals són quantificades.

-Variable lligada i lliure :la variable del camp d'un quantificador que la quantifica és la variable lligada i la variable lliure és la variable no quantificada.

-Fórmula tancada : si totes les variables que hi apareixen són variables lligadas, i això implica que tenim un enunciat.

-Fórmula oberta : si hi apareixen variables lliures.

LLENGUATGE DEL CP1

El llenguatge usat en CP1 es genrat a partir del següent alfabet :

"= {", ", !, ¬, (, ), ", ", P, Q, R,..., a, b, c,..., x, y, z}.

Predicats constants variables

El llenguatge és un conjunt de fórmules den formades (wff) definides per les següents regles de construcció :

-Tot n+1 tuple de la forma P(t1, t2,..., tn) tal que P és un predicat i t1, t2,..., tn són termes, és una fórmula ben formada.

-Si A i B són fórmules ben formades i v és una variable, aleshores tembé són fórmules ben formades les següents expressions :

(¬A), (A"B), (A"B), (A!B), ("v A) I ("v a).

-No hi ha cap altra fórmula ben formada.

Tal com s'ha fet en el CP0 en CP1 convenim a fer el següent :

1. Eliminar els parèntesis exteriors.

2. Associar una prioritat a les conectives i quantificadors, creixent-ment,així :

!, !, " & ", ¬, " & "

3. Simplificar tota expressió del tipus A(t1, t2,..., tn) a At1, t2,...,tn si no hi ha perill de confusió.

FORMALITZACIÓ DEL LLEGNUATGE NATURAL

FORMALITZACIÓ DE PROPOSICIONS MOLECULARS

a) Proposicions globalment quantificades :al menys hi ha un quantificador el camp del qual és troba la fórmula.

Si " ! "x (A!B)

Si " ! "x (A"B)

b) Proposicions no quanitificades globalment :cal detectar la conectiva dominant com en el CP0.

5.- TEORIA DE LA DEMOSTRACIÓ

DEDUCCIÓ NATURAL

Les variables lliures de les premisses designen a un objecte constant del domini. Si una variable està lligada a unes premisses o no ha estat usada mai aleshores designa un objecte arbitrari del domini.

Les regles d'inferència en què es basa la DN del CP1 són les nou regles del CP0 més quatre noves regles referides als dos quantificadors, que són :

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.

"x"y (P(f(y), x) " R(y, h(f(x))) " Q(a, g(b)))

FUNCIONS EN CP1

Podem ampliar la potència expresiva del CP1 afegint la possibilitat de referir-nos a funcions (en el sentit matemàtic) o correspondencies prèviament definides entre objectes del domini D d'interpretació.

Una funció de n paraàmetres s'expresa mitjançant lletres minúscules seguides d'un parèntesi amb els n termes separats per comes.

F(a,x) o f ax ; pare_de (alicia) ; suma (2,3)

Els termes en les funcions són :

- Una constant.

- Una variable.

- Una funció tal que si t1, t2,..., tn són termes i f una funció del CP1 aleshores f(t1, t2,..., tn) també és un terme.

FORMES NORMALS PRENEXA

Es diu que una fòrmula del CP1 està expresada en FNP si consta d'un refix i una matriu tals que :

- El prefix conté escrits en seqüència tots els quantificadors de la fòrmula i nomes els quantifiadors.

- La matriu només es una fomra normal conjuntiva o disjuntiva.

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.

6.-DEMOSTRACIÓ AUTOMÀTICA

FORMES NORMALS D'SKOLEN

Una fórmula està escrita en forma normal d'Skolen (FNS) si :

-Està escrita en FNP

-El prefix no conté quantificadors existencials.

Una forma normal d'Skolen no és quivalent deductiu de la fórmula inicial, en general.

SKOLEMITACIÓ BASICA

Sigui A una fórmula ben formada arbitraria del CP1 :

1.- "x "y Ay ---> "x Af(x).

2.- "x "y Ax ---> "y Aa.

3.- "x Ax ------> Aa.

Quan una fòrmula està escrita en FNP la fòrmula s'Skolen corresponent es calcula recorrent la fórmula d'esquerra a dreta tants cops com quantificadors existencials tingui el prefix. A cada recorregut s'elimina el primer existencial i es substitueix la variable quantificada en tote les ocurrencies per una nova funció d'Sklen que depen de les variables quantificades universalment a l'esquerra de l'existencial eliminat.

"x "y "z "u "v Q(x, y, z, u, y)

"x "z "u "u Q(x, f(x), z, u, f(x))

"x "z "v Q(x, f(x), z, g(x,z), f(x))

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Ó

Un subterme és qulaevol terme que formapart d'un altre terme. Les constants i variables només tenen un subterme que coincideix amb el mateix, en canvi les funcions tenen si mes no dos subtermes, la propia funció i un peràmetre.

Una substitució és una operació per la qual substituïm una variable per una constant, una funció o per una altra variable diferent de la substituida.

A(x, y, b, x) ---->A(f(z), y, b f(z)) fent el canvi de x per f(z) (f(z)/x)

Una composició de susbtitucións és una plicació en seqüència de les substitucions components.

Parell discrepant :siguin t1 i t2 dos termes ben formats arbitraris que tenen a la posició i-ésima els subtermes u1 i u2 tals que u1"u2, es diu que (u1, u2) són una parella discrepant.

Unficicació : dos termes t1 i t2 són unificables respecte de la parella discrepant (u1, u2) si i només si :

1.- u1 o u2 o tots dos termes són variables.

2.- si u1 és variable i no apareix a u2 i si u2 és variable i no apareix a u1.

Dos termes t1 i t2 són unificables si i nomes si són unificables respecte de totes les parelles discrepants. Dos predicats P1 i P2 són unificables si ho són respecte tots els seus termes. Dues instancies d'un mateix predicat P són unificables si ho són respecte de tots els seus subtermes.

P={P1 i P2 dues instancies de Pi,  respresenta la substitució identitat}

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

RESOLUCIÓ

Sigui A, B i C fórmules ben formades del CP1 :C1 = A"B i C2 = ¬A"B

i  la substitució que unifica C1 i C2 respecte de A llavors la resolució es defineix com :

m A " B

n ¬A " C

B " C RS m, n

Resolució : A1, A2,....An, B són fórmules ben formades del CP 1. Les tres afirmacions següents són equivalents :

1.- A1, A2,....An B

2.- A1, A2, ...,An, ¬B Ÿ

3.- Si C1, C2,..., Cm són clausues convenientmentrebatejades procedents de Skolemitzar el sqüent refutat, aleshores :

C1, C2,...., Cm Ÿ

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.

7.-TEORIES

Una teoria de primer ordre està definida per :

1.- Un alfabet ".

2.- Un llenguatge lògic. En el nostre cas el de CP1.

3.- Un conjunt d'axiomes A(un conjuntde fòrmules vàlides per definició)

4.- Un conjunt de regles d'inferencia. En el nostre cas les de CP1.

Els axiomes A s'agrupen en dues categories :

Axiomes lògics : són els del llenguatge lògic sobre el qual es construeix la teoria (CP1).

Axiomes no lògics o propis de la teoria : donats a la mateixa teoria.

Un teorema és tota fòrmula derivable a partir dels axiomes d'una teoria.

TA A la teoria T la fórmula A és un teorema.

CLASSIFICACIÓ DE LES TEORIES

-Teoria incosistent :si a partir de la seva definició es pot derivar A i ¬A, es a dir T A i T ¬A

-Teoria consistent : tota teoria que no és inconsistent.

-Teoria Completa : si resulta que tota fórmula o enunciat o be es un teorema o es el seu negat. Si per tota fórmula A resulta que T A o T ¬A.

-eoria incompleta : existeix alguna fórmula A tal que no T A i T ¬A. A es diu que no es decidible en la teoria T.