Tècniques Semàntiques d'Estudi de Validesa Proposicional

Taules de Veritat

Definició 7

Una taula de veritat és una representació tabular del valor d'una fórmula en totes les possibles interpretacions.

Exemple

Calcular el valor de veritat de la fórmula F = p → q ↔ ¬p ∨ q , la taula de veritat consisteix en representar les 4 possibles interpretacions i avaluar-ne la fórmula en elles.

El nombre de possibles interpretacions d'una fórmula F és 2ⁿ on n és el nombre de variables proposicionals de F. Per tant, aquest mètode té una complexitat exponencial que complica la seva utilització per a fórmules complexes.

Arbres Semàntics

Definició 8

Un arbre semàntic és una tècnica similar a les taules de veritat que pot simplificar l'avaluació d'algunes fórmules.

Procediment

Inicialment, es forma el conjunt LP de lletres proposicionals de la fórmula. Es construeix un node inicial de l'arbre que es prendrà com a node actual i s'aplica el següent procediment:

1. S'intenta avaluar la fórmula en el node actual.
2. Si és possible assignar a F un valor {Veritat, Fals} s'etiqueta el node amb el valor assignat i es finalitza el tractament del node actual.
3. En cas contrari:
1. Es selecciona la primera lletra proposicional p del conjunto LP.
2. S'esborra p de LP.
3. Es construeixen dues branques, una corresponent a p interpretat amb valor Veritat (identificada com a p) i l'altra corresponent a p amb valor Fals (identificada com a ¬p).
4. es repeteix el procediment per a cadascun dels dos nous nodes.

Definició 9

Els nodes de l'arbre semàntic en els que el conjunto de significats atribuïts fins a ells fan Fals la fórmula, s'anomenen nodes d'errada i els que la fan Verita, nodes d'encert.

Exemple

Donada la fórmula (p → q) → (¬p → ¬q). Seleccionant els literals per ordre alfabètic, s'obté el següent arbre semàntic:

Observem-ne que no ha estat necessari avaluar les interpretacions p = V, q = V i p = V, q = F.

NOTA: Per simplificació, s'anotarà a partir d'ara V com a Veritat i F com a Fals

Demostració per Contradicció

Procediment

Per a demostrar que una fórmula F és vàlida per contradicció es realitza el següent:

1. Es suposa que existeix una interpretació I tal que V_I(F) = F i s'intenten calcular els diversos valors de la fórmula.
2. Si s'arriba a una contradicció, aleshores ∄ I V_I(F) = F ⇒ ∀I V_I(F) = V ⇒ F és vàlida.
3. En cas contrari ∃ I V_I(F) = F ⇒ F no és vàlida.

Aquest tipus de demostracions es sol representar etiquetant la fórmula amb valor F i avaluant-ne els possibles valors fins que s'arribi a la contradicció. Per a poder assegurar que F és vàlida s'ha d'arribar a contradicció per totes les alternatives. Si no s'arriba a contradicció per alguna alternativa es pot dir que F no és vàlida.

Exemples

a) Volem demostrar la validesa de la fórmula: ¬p ∨ ¬q → ¬(p ∧ q)

Suposem la fórmula no vàlida. S'arriba a contradicció (en vermell), per tant la fórmula és vàlida.

b) Volem demostrar la transitivitat de l'equivalència lògica. És a dir que: (A ↔ B, B ↔ C) ⇒ (A ↔ C). Per fer-ho hi haurà prou amb demostra que la fórmula: (A ↔ B) ∧ (B ↔ C) → (A ↔ C) és vàlida. En aquesta demostració apareixen dues alternatives i la fórmula és vàlida perquè s'arriba a contradicció per totes dues. Suposem la fórmula no vàlida.

Resolució Proposicional

El mètode de resolució és un algorisme fàcilment mecanitzable proposat per J.A. Robinson el 1965. L'entrada de l'algorisme no és una fórmula, sinó un conjunt de cláusules i l'algorisme comprova si són insatisfacibles. Abans de presentar l'algorisme de resolució, es defineix què és una clàusula i com transformar una fórmula en un conjunt de clàusules mitjançant les formes normals.

Formes normals

Definició 10

Una fórmula F és una conjunció si és de la forma F₁ ∧ F₂ ∧ ··· ∧ F_n, amb n ≥ 0

Definició 11

Una fórmula F és una disjunció si és de la forma F₁ ∨ F₂ ∨ ··· ∨ F_n, amb n ≥ 0

Definició 12

Un literal és una proposició (p) o una proposició negada (¬p)

Definició 13

Una fórmula F és en Forma Normal Conjuntiva (FNC) si és una conjunció de la forma: F₁ ∧ F₂ ∧ ... ∧ F_n

On cada F_i és una disjunció de literals. Es representa per:

Exemple: La següent fórmula és en FNC: (¬p ∨ q) ∧ (¬p ∨ r ∨ ¬s) ∧ p

Definició 14

Un fórmula F és en Forma Normal Disjuntiva (FND) si és una disjunció de la forma: F₁ ∨ F₂ ∨ ... ∨ F_n

On cada F_i és una conjunció de literals. Es representa per:

Exemple: La següent fórmula és en FND: (p ∧ ¬q ∧ r) ∨ ¬p ∨ (r ∧ ¬s)

Observem que la fórmula (¬p) és a la vegada en FNC i FND.

Teorema 5

Tota fórmula de la lògica de proposicions pot ser transformada en una fórmula lògicament equivalent a ella en FNC o FND.

Demostració:

La demostració consisteix en indicar els passos de l'algorisme de transformació a forma normal conjuntiva. Donat que aquests passos mantenen l'equivalència i donat que l'equivalència acompleix la propietat transitiva, la fórmula resultant és equivalent a la fórmula original. Per a demostrar formalment que l'algorisme acaba, es requereix l'estudi de sistemes de re-escriptura de termes que pot consultar-se a [Abramsky, 92]. Els passos de transformació són:

1. Eliminar la connectiva ↔:
• A ↔ B ≡ (A → B) ∧ (B → A)
2. Eliminar la connectiva →:
• A → B ≡ (¬A ∨ B)
3. Utilitzar les lleis de De Morgan introduint negacions fins que afectin als literals:
• ¬(A ∧ B) ≡ ¬A ∨ ¬B)
• ¬(A ∨ B) ≡ ¬A ∧ ¬B)
4. Eliminar les negacions múltiples:
• ¬¬A ≡ A
5. Aplicar propietats distributives per eliminar les possibles conjuncions (disjuncions) dins de disjuncions (conjuncions) obtenint-ne FNC o FND:
• A ∧ (B ∨ C) ≡ (A ∧ B) ∨ (A ∧ C)
• A ∨ (B ∧ C) ≡ (A ∨ B) ∧ (A ∨ C)

Donat que les fórmules resultants d'aplicar cadascun dels passos anteriors mantenen l'equivalència, la fórmula obtinguda serà equivalent a la fórmula original.

En moltes ocasions s'hi afegeixen altres tres passos per a simplificar-ne la fórmula obtinguda:

Simplificació

1. Eliminar conjuncions (disjuncions) afegint-ne un literal i el seu oposat:
• (p ∧ ¬p ∧ X) ∨ Y ≡ Y
• (p ∨ ¬p ∨ X) ∧ Y ≡ Y
2. Eliminar literals repetits:
• (p ∧ p) ≡ p
• (p ∨ p) ≡ p
3. Eliminar subsumpcions. Una subsumpció es produeix quan una conjunció (o disjunció) C és inclosa en altra D. Aleshores s'elimina la clàusula D:
• (A ∨ B) ∧ A ≡ A
• (A ∧ B) ∨ A ≡ A

Exemple

Transformar la fórmula ¬(p → q) ↔ p ∨ r a FNC:

Definició 15

Una clàusula és una disjunció de literals.

Definició 16

Una fórmula està en Forma Clausal si s'expressa com a un conjunt de clàusules.

La transformació d'una fórmula en FNC a Forma Clausal és immediata substituint les connectives per comes i englobant les disjuncions entre claus.

Exemple

La fórmula (¬p ∨ q) ∧ (¬p ∨ q ∨ ¬r) ∧ (p) en FNC equival a {¬p ∨ q, ¬p ∨ q ∨ ¬r, p} en Forma Clausal

Definició 17

Una clàusula sense literals s'anomena clàusula buida, es representa per π i el seu valor és sempre igual a F.

Definició 18

Una clàusula amb, com a molt, un literal positiu s'anomena clàusula Horn. Una clàusula Horn serà de la forma: A ∨ ¬B₁ ∨ ¬B₂ ∨ ··· ∨ ¬B_n

Si n = 0, s'anomena fet, si no existeix literal positiu (no existeix A) aleshores s'anomena objectiu i, finalment, si n > 0 i existeix literal positiu, s'anomena regla.

Forma normal negativa (FNN)

Definició

• Si F és atòmica, aleshores F i ¬F són FNN.
• Si F i G són FNN, aleshores (F ∧ G ) i (F ∨ G ) també ho són.

Exemples

• (¬p ∨ q) ∧ (¬q ∨ p) és FNN
• (p → q) ∧ (q → p) no és FNN
• ¬(p ∧ q) no és FNN

Transformació a FNN

L'objectiu és: donada una fórmula F , obtenir-ne una altra en forma normal negativa G tal que F ≡ G.

Es seguirà, ordenadament, el procediment fnn(F) següent:

1. Eliminar equivalències: p ↔ q ≡ (p → q) ∧ (q → p)
2. Eliminar implicacions: p → q ≡ ¬p ∨ q
3. Interioritzar negacions:
• ¬(p ∧ q) ≡ ¬p ∨ ¬q
• ¬(p ∨ q) ≡ ¬p ∧ ¬q
• ¬¬p ≡ p
• ¬(¬(p ∨ q)) ≡ p ∨ q
• ¬((¬p) ∨ q) ≡ p ∧ ¬q

Exemples

• fnn(p ↔ q) = (¬p ∨ q) ∧ (¬q ∨ p)
• fnn((p ∨ (¬q)) → r ) = (¬p ∧ q) ∨ r
• fnn((p ∧ (q → r)) → s) = ((¬p ∨ (q ∧ ¬r)) ∨ s)

Propietats

• fnn(F) és FNN
• fnn(F) ≡ F

Forma normal conjuntiva (FNC)

Disjuncions esteses

• Si F és un literal, aleshores F és una disjunció estesa.
• Si F i G són disjuncions esteses, aleshores (F ∨ G) també ho és.

Exemples

• ¬p ∨ (q ∨ ¬r) és una disjunció estesa.
• ¬p ∨ (q ∧ ¬r) no és una disjunció estesa.

Fórmules en FNC

• Si F és una disjunció estesa, aleshores F és FNC.
• Si F i G són FNC, aleshores (F ∧ G) també ho és.

Exemple

Ambdues són equivalents, però una és FNC i l'altra no:

• (¬p ∨ q) ∧ (¬q ∨ p) és FNC.
• (¬p ∨ q) ∧ (q → p) no és FNC.

Transformació en FNC

L'objectiu és: donada una fórmula F, obtenir-ne una altra en FNC G tal que F ≡ G

Es seguirà, ordenadament, el procediment fnc(F) següent:

1. Transformació a FNN.
2. Interiorització de les disjuncions:
• p ∨ (q ∧ r) ≡ (p ∨ q) ∧ (p ∨ r)
• (p ∧ q) ∨ r ≡ (p ∨ r) ∧ (q ∨ r)

Exemples

• fnc(p ∧ (q → r)) = p ∧ (¬q ∨ r)
• fnc(¬(p ∧ (q → r))) = (¬p ∨ q) ∧ (¬p ∨ ¬r)
• fnc(¬(p ↔ r)) = (((p ∨ r) ∧ (p ∨ ¬p)) ∧ ((¬r ∨ r) ∧ (¬r ∨ ¬p)))

Propietats

• fnc(F) és una FNC.
• fnc(F) ≡ F

Forma normal disjuntiva (FND)

Conjuncions esteses

• Si F és un literal, aleshores F és una conjunció estesa.
• Si F i G són conjuncions esteses, aleshores (F ∧ G) també ho és.

Exemples

• ¬p ∧ (q ∧ ¬r) és una conjunció estesa.
• ¬p ∨ (q ∧ ¬r) no és una conjunció estesa.

Fórmules en FND

• Si F és una conjunció estesa, aleshores F està en FND.
• Si F i G estan en FND, aleshores (F ∨ G) també ho està.

Exemples

• (¬p ∧ q) ∨ (¬q ∧ p) està en FND.
• (¬p ∧ q) ∨ (q → p) no està en FND.

Transformació en FND

L'objectiu és: donada una fórmula F, obtenir-ne una altra en FND G tal que F ≡ G

Es seguirà, ordenadament, el procediment fnd(F) següent:

1. Transformació a FNN
2. Interiorització de les conjuncions:
• p ∧ (q ∨ r) ≡ (p ∧ q) ∨ (p ∧ r)
• (p ∨ q) ∧ r ≡ (p ∧ r) ∨ (q ∧ r)

Exemples

• fnd(p ∧ (q → r)) = (p ∧ ¬q) ∨ (p ∧ r)
• fnd(¬(p ∧ (q → r))) = (¬p ∨ (q ∧ ¬r))

Propietats

• fnd(F) és una forma normal disjuntiva.
• fnd(F) ≡ F

Algorisme de resolució proposicional

L'algorisme es basa en una regla d'inferència senzilla i, a la vegada, de gran potència: la regla de resolució. Donat que s'utilitza una sola regla, l'algorisme és fàcil d'analitzar i implementar.

La idea del principi de resolució és simple: Si es sap que s'acompleix: "P ó Q" i també se sap que s'acompleix "no P ó R" aleshores es pot deduir que s'acomplirà "Q ó R".

Exemple

Si es té: "Guanya ó Perd ó Empata" i "Si Guanya aleshores dona una Festa o Va de Viatge". Es pot deduir que: "ó Perd ó Empata ó dona una Festa ó va de Viatge".

Formalitzat com:

• Premissa 1: G ∨ P ∨ E
• Premissa 2: G → F ∨ V ≡ ¬G ∨ F ∨ V
• Conclusió (inferència de la regla de resolució): P ∨ E ∨ F ∨ V

Definició 19

Donades dues clàusules C₁ i C₂ tals que existeixi un literal L de forma que L ⋲ C₁ i ¬L ⋲ C₁ , es denomina resolvent de C₁ i C₂ respecte a L, a la clàusula: R_L(C₁,C₂) = (C₁ – {L}) ∪ (C₂ – {¬L}

Es diu aleshores que C₁ i C₂ són clàusules resolubles.

Teorema 6 (Consistència de la regla de resolució)

El resolvent de dues clàusules és conseqüència lògica d'elles. És a dir: {C₁,C₂} ⇒ R(C₁, C₂)

Demostració

Es demostra per contradicció.

Sigui C₁ = L ∨ L₁₁ ∨ L₁₂ ∨ ··· ∨ L_1m i C₂ = ¬L ∨ L₂₁ ∨ L₂₂ ∨ ··· ∨ L_2n

El resolvent de C₁ i C₂ respecte a L serà: R_L(C₁,C₂) = L₁₁ ∨ L₁₂ ∨ ··· ∨ L_1m ∨ L₂₁ ∨ L₂₂ ∨ ··· ∨ L_2n

Pel teorema 2, provar que {C₁,C₂} ⇒ R(C₁,C₂) és equivalent a provar que C₁ ∧ C₂ ⇒ R_L(C₁,C₂) és vàlida.

Suposem que existeix una interpretació que la fa F, l'assignació de valors serà:

(L ∨ L₁₁ ∨ L₁₂ ∨ ··· ∨ L_1m) ∧ (¬L ∨ L₂₁ ∨ L₂₂ ∨ ··· ∨ L_2n) → (L₁₁ ∨ L₁₂ ∨ ··· ∨ L_1m ∨ L₂₁ ∨ L₂₂ ∨ ··· ∨ L_2n)

Assignació que ens porta a una contradicció. Per tant la fórmula no pot ser F i serà sempre V, és a dir: la fórmula és Vàlida.

Teorema 7

Donades dues clàusules C₁ i C₂, pertanyents a un conjunt C i resolubles respecte a un literal L, aleshores tindrem que C ≡ C ∪ R_L(C₁,C₂)

Demostració

Sigui C = C₁ ∧ C₂ ∧ ··· ∧ C_n aleshores el conjunt C ∪ R_L(C₁,C₂) serà: C₁ ∧ C₂ ∧ ··· ∧ C_n ∧ R_L(C₁,C₂).

La demostració consisteix a provar que la fórmula: C₁ ∧ C₂ ∧ ··· ∧ C_n ↔ C₁ ∧ C₂ ∧ ··· ∧ C_n ∧ R_l(C₁,C₂) és vàlida.

Es té en compte el teorema 6 i es demostra per contradicció.

Teorema 8

Si el resolvent de dues clàusules C₁ i C₂, pertanyents a un conjunt C és la clàusula buida, aleshores C és insatisfacible.

Demostració

Es demostra en primer lloc que el conjunt C és equivalent a F:

Finalment es demostra que qualsevol fórmula equivalent a F és insatisfacible.

A partir dels teoremes anteriors, es defineix l'algorisme de resolució que comprovarà si un conjunt de clàusules es insatisfacible:

Procediment de l'algorisme de resolució proposicional

• Entrada: Un conjunt de clàusules C
• Sortida: Detecta si C és insatisfacible

Passos:

1. Buscar dues clàusules C₁ i C₂ ⋲ C tals que existeixi un literal L que acompleixi que L ⋲ C₁ i ¬ ⋲ C₂
2. Si es troben:
3. Calcular R_L(C₁,C₂) i afegir al conjunt C
4. Si R_L(C₁,C₂) = ∅ aleshores SORTIR indicant que C és insatisfacible
5. Si no, tornar a 1
6. Si no es troben: SORTIR indicant que C no és insatisfacible

Exemple

Sigui C el següent conjunt de clàusules: {p, ¬p ∨ q, ¬r, ¬p ∨ ¬q ∨ r} es pot demostrar que C és insatisfacible per resolució. Par a fer-ho:

• Es resol la tercera clàusula ( ¬r ) amb la quarta ( ¬p ∨ ¬q ∨ r ), obtenint-ne ¬p ∨ ¬q
• Es resol ara la clàusula anterior amb la segona clàusula ( ¬p ∨ q ) obtenint-ne: ¬p
• Es resol ara la clàusula anterior amb la primera clàusula ( p ) i s'arriba a la clàusula buida ∅
• Per tant, C es insatisfacible

Teorema 9

Un raonament de la forma: P₁ , P₂ , ···, P_n ⇒ Q és correcte sí i només sí el conjunt de clàusules:

{ P^c₁, P^c₂, ···, P^c_n, ¬Q^c } es insatisfacible.

Cada P^c_i és el resultat de transformar la premissa P_i a forma clausal.

I aleshores, ¬Q_c és el resultat de transformar la negació de la conclusió a forma clausal.

Demostració

Exemple

Per a estudiar si el raonament { p ∧ q → r ∧ s, p → ¬s } ⇒ ¬p ∨ ¬q es correcte per resolució, es necessari transformar cada premissa a forma clausal i afegir-ne el resultat de transformar la negació de la conclusió a forma clausal.

El conjunt obtingut serà: { ¬p ∨ ¬q ∨ r, ¬p ∨ ¬q ∨ s, ¬p ∨ ¬s, p, q }.

Aplicant l'algorisme de resolució:

• Es resol la segona clàusula ( ¬p ∨ ¬q ∨ s) amb la tercera ( ¬p ∨ ¬s), obtenint-ne: ¬p ∨ ¬q
• Es resol ara la clàusula anterior amb la quarta clàusula (p) obtenint-ne: ¬q
• Es resol ara la clàusula anterior amb la cinquena i s'arriba a la clàusula buida: ∅

Donat que s'arriba a la clàusula buida, el conjunt de clàusules és insatisfacible i el raonament és correcte.

Demostració de la completud de l'algorisme de resolució

Es presenten les idees generals de la demostració de la completud de l'algorisme de resolució proposicional. Una demostració formal requereix tècniques que van més enllà d'aquest treball [Fitting, 96].

Exemple

Sigui el conjunt de clàusules C = { p, ¬p ∨ q, ¬r, ¬p ∨ ¬q ∨ ¬r }.

Per a construir l'arbre semàntic per a C es recorda que un conjunt de clàusules equival a una FNC, en aquest cas: p ∧ (¬p ∨ q) ∧ (¬r) ∧ (¬p ∨ ¬q ∨ ¬r).

En la següent figura es mostra l'arbre semàntic corresponent, marcant la clàusula F en els nodes d'errada:

Lema 1

Si un conjunt de clàusules és insatisfacible, aleshores l'arbre semàntic és finit i limitat per nodes d'errada, s'anomena, en aquest cas, arbre d'errada.

Lema 2

Cada node d'errada n fa F al menys a una de les clàusules del conjunt que serà la clàusula associada a n.

Lema 3

La clàusula C associada a un node d'errada n conté un subconjunt dels complements dels literals que apareixen a la branca que va des de l'arrel de l'arbre semàntic fins a n.

Demostració

Donat que la clàusula C fa F el node n, tots els seus literals han de tenir assignat un valor en la interpretació parcial corresponent a n. A més, el valor d'aquests literals ha de ser F (donat que C és una disjunció). El valor assignat ha de ser doncs el complementari.

Definició 20

S'anomena node d'inferència a un node de l'arbre semàntic els fills del qual són nodes d'errada.

Lema 4

En un arbre d'errada, excepte que només tingui un node, ha d'existir al menys un node d'inferència.

Demostració

Donat que l'arbre d'errada és finit i les branques es desenvolupen de dues en dues, necessàriament tindrem un últim node desenvolupat amb dos fills.

Lema 5

Si l'arbre semàntic d'un conjunt de clàusules és d'errada i conté un sol node, aleshores aquest conjunt conté la clàusula buida.

Lema 6

Un node d'inferència i indica un pas de resolució de les clàusules associades als seus dos fills. El resolvent d'aquestes clàusules és F pel node i i, ocasionalment, per algun dels seus antecessors.

Demostració

En un node d'inferència i qualsevol, es tindrà un esquema com el següent:

• Donat que el node i no fa F a C_j i la única cosa que canvia en el node j respecte a i és el valor de p, la clàusula C_j ha de contenir el literal ¬p (complementat per tal de que sigui F).
• Per la mateixa raó, la clàusula C_k ha de contenir el literal p (sense complementar per tal de que sigui F).

Per tant: C_j i C_k són resolubles respecte a p. L'esquema serà:

En el node j, C_j pren valor F, per tant Reste_C_j prendrà també valor F, com Reste_C_j no conté el literal p també prendrà valor F en el node i

De la mateixa forma, Reste_C_k prendrà valor F en el node i. Per tant, R_p(C_j, C_k) = Reste_C_j ⋁ Reste_C_k C prendrà valor F en el node i, és a dir, el node i, és un node d'errada per al resolvent de C_j i C_k

De vegades, pot ocórrer que el resolvent sigui F també per algun dels pares del node d'inferència, com exemple, consideris el conjunt de clàusules { p, ¬p ⋁q, ¬r, ¬p ⋁ r }, l'arbre semàntic, junt amb els resolvents seria:

El resolvent dels nodes 6 i 7 és ( ¬p) que fa F al node 4 però també fa F al seu antecessor, el node 2.

Teorema 10 (Completud de l'algorisme de resolució proposicional)

Si un conjunt de clàusules és insatisfacible aleshores, aplicant l'algorisme de resolució, s'arriba a la clàusula buida.

Demostració

El nou arbre seguirà sent insatisfacible però contindrà menys nodes. Repetint el procés s'arribarà a un arbre semàntic amb un sol node que correspondrà a la clàusula buida { Lema 5 }. Quedant demostrat que s'arriba a la clàusula buida per resolució.

Estratègies de resolució

El mètode de resolució és un algorisme no determinista ja que poden trobar-se múltiples formes d'assolir la clàusula buida en un conjunt insatisfacible. Molts cops, seguint un determinat camí s'assolirà la clàusula buida amb molts menys passos de resolució que per un altre camí.

Durant el desenvolupament de l'algorisme és necessari respondre les següents preguntes: Quines dues clàusules es seleccionen? i sobre quins literals es fa la resolució?

Les diferents estratègies de resolució tracten de respondre a ambdues preguntes de forma que es mantingui la completud (si el conjunt és insatisfacible, assolir la clàusula buida) de manera eficient.

Un dels desavantatges de la utilització de les regles de resolució sense cap restricció consisteix en que es poden seleccionar clàusules en les que el seu resolvent no sigui útil en el camí de cerca de la clàusula buida. S'observa que molts cops els resolvents són redundants o no aporten cap utilitat per a la cerca. A continuació es mencionen un seguit d'estratègies que serviran per a eliminar el treball inútil.

Estratègies d'esborrat

Una estratègia d'esborrat serà una tècnica en la qual s'eliminen un seguit de clàusules abans de que siguin utilitzades. Si aquestes clàusules no van a aportar res per a la cerca de la clàusula buida, la seva eliminació permetrà un estalvi computacional.

Eliminació de clàusules amb literals purs

Definició 21

Un literal és pur sí i només sí no existeix un literal complementari a ell en el conjunt de clàusules.

Una clàusula que contingui un literal pur és inútil en la cerca de la clàusula buida, donat que el literal pur no podrà ser eliminat mai mitjançant resolució. Per tant, una estratègia d'esborrat consisteix en l'eliminació de clàusules con literals purs.

Exemple

Sigui el conjunt C = { ¬p ∨ ¬q ∨ r, ¬p ∨ s, ¬q ∨ s, p, q, ¬r, } és insatisfacible, tanmateix, per a demostrar-ho, es poden ignorar la segona i la tercera clàusules, donat que ambdues contenen el literal pur s.

Eliminació de tautologies

Definició 22

Una tautologia és una clàusula que conté el mateix literal en la seva forma directa i inversa. ^[1]

Exemple

La clàusula p ∨ ¬q ∨ r ∨ ¬p és una tautologia.

La presència o absència de tautologies en un conjunt de clàusules no afecta la condició de satisfacibilitat del conjunt. Un conjunt de clàusules romandrà satisfacible independentment de que se li afegeixin tautologies. De la mateixa manera, un conjunt de clàusules insatisfacible ho seguirà sent encara que s'elimini totes les seves tautologies. És possible, per tant, eliminar les tautologies d'un conjunt de clàusules per a que no intervinguin en el procés de cerca sense alterar-ne la satisfacibilitat del conjunt.

Eliminació de Subsumpcions

Definició 23

Una clàusula C subsumeix a una clàusula D sí i només sí tot literal de C pertany també a D, és a dir: C ⊆ D.

Exemple

La clàusula p ∨ ¬q subsumeix a la clàusula p ∨ ¬q ∨ r.

Per la llei d'absorció, un conjunt de clàusules en el que s'eliminin totes les clàusules subsumides serà equivalent al conjunt original. Les clàusules subsumides poden ser, per tant, eliminades.

Es necessari observar que, durant el desenvolupament del procés de resolució, es poden generar resolvents de clàusules que siguin tautologies o clàusules subsumides. Les estratègies d'esborrat hauran de comprovar tant el conjunt de clàusules original com els diferents resolvents generats en cada resolució.

Resolució unitària

Definició 24

Un resolvent unitari és un resolvent en el qual al menys un dels pares és una clàusula unitària (amb un sol literal).

Una estratègia de resolució unitària és una aplicació de l'algorisme de resolució en la qual tots els resolvents són unitaris.

Exemple

Sigui C = { p ∨ q, ¬p ∨ r, ¬q ∨ r, ¬r, } . A continuació s'aplicarà l'estratègia de resolució unitària, per a fer-ho, es seleccionen sempre dues clàusules resolubles tals que una d'elles tingui un literal.

Observis que els resolvents generats són un subconjunt dels que es podrien generar mediant la resolució sense restriccions. Per exemple, les clàusules 1 i 2 podrien haver-se seleccionat per a obtenir q ∨ r . Tanmateix ni aquesta clàusula ni els seus descendents podran ser generats perquè cap de les clàusules que la generen és unitària.

Els procediments de resolució basats en resolució unitària són senzills d'implementar i, normalment, bastant eficients. Observis que si una clàusula és resolta amb una clàusula unitària, el seu resolvent té menys literals que la clàusula original. D'aquesta manera els procediments segueixen una cerca directa cap a la clàusula buida (∅) guanyant en eficiència.

Malauradament, els procediments d'inferència basats en resolució unitària no són, en general, complerts. Per exemple, el conjunto C = { p ∨ q, ¬p ∨ q, p ∨ ¬q, ¬p ∨ ¬q } es insatisfacible, però la resolució unitària no trobarà la clàusula buida perquè cap de les clàusules és unitària.

Per altra banda, restringint-ne el format de clàusules a clàusules Horn (clàusules amb un literal positiu com a màxim) es pot demostrar que si un conjunto de clàusules Horn és insatisfacible, aleshores s'arribarà a la clàusula buida aplicant l'estratègia de resolució unitària.

Resolució d'entrada

Definició 25

Un resolvent d'entrada és un resolvent en el qual al menys un dels pares és una clàusula del conjunt original d'entrada.

Una estratègia de resolució d'entrada es una aplicació de l'algorisme de resolució en la qual tots els resolvents són d'entrada.

Exemple

Sigui C = { p ∨ q, ¬p ∨ r, ¬q ∨ r, ¬r, } . A continuació s'aplicarà l'estratègia de resolució d'entrada, per a fer-ho, es seleccionen sempre dues clàusules resolubles tals que una d'elles pertany al conjunt original d'entrada.

Es pot demostrar que la resolució unitària i la resolució d'entrada tenen el mateix poder d'inferència en el sentit de que si amb una estratègia es pot assolir la clàusula buida, amb l'altra també.

Una conseqüència de l'anterior és que la resolució d'entrada és complerta per a clàusules Horn, però incomplerta en general. Com a contraexemple, es pot prendre el de l'apartat anterior.

Resolució lineal

La resolució lineal (també coneguda com a resolució amb filtrat d'avantpassats) és una lleugera generalització de la resolució d'entrada. S'escull una clàusula inicial o clàusula cap C₀ i es forma una cadena de resolvents R₀ , R₁ , R₂ ,···, R_n on:

• R₀ = C₀
• R_i+1 = R(R_i, C_i) tal que C_i ⋲ C ó C_i = R_j (j ≤ i)

La resolució lineal pren el nom de l'aspecte lineal que presenten les inferències realitzades. Una resolució lineal comença amb una clàusula del conjunt inicial i produeix una cadena lineal de resolucions com la que es mostra en la figura pel conjunt de clàusules: C = { p ∨ q, ¬p ∨ q, p ∨ ¬q, ¬p ∨ ¬q }

Observis que cada resolvent, després del primer, s'obté del resolvent anterior i d'alguna altra clàusula del conjunt.

La resolució lineal evita moltes resolucions inútils centrant-se en cada pas en els avantpassats d'una clàusula i en els elements del conjunt inicial.

Els resultats obtinguts aplicant resolució per a una determinada clàusula cap es poden mostrar en forma d'arbre de resolució. L'arrel de l'arbre és la clàusula cap i es formen els nodes descendents segons les clàusules amb les que es pot resoldre. L'arbre de resolució per a l'exemple anterior seria:

En la figura es representen les resolucions indicant el nombre de la clàusula i el literal pel que es resol. A cada resolvent se li assigna un nou nombre. Observis que poden existir camins infinits (el camí més a l'esquerra), camins que porten a tautologies i camins d'èxit que assoleixen la clàusula buida.

Es pot demostrar que la resolució lineal es complerta. Per a qualsevol conjunt de clàusules insatisfacibles, aplicant resolució lineal, s'assoleix la clàusula buida.

Com a conseqüència del següent teorema, no sempre és necessari provar amb totes les clàusules del conjunt inicial com a clàusula cap.

Teorema 110

Si un conjunt de clàusules S es satisfacible i S ∪ C es insatisfacible, aleshores es troba la clàusula buida mitjançant resolució lineal prenent com a clàusula cap una clàusula del conjunto C.

El teorema anterior té aplicació a l'estudi dels raonaments, en els quals les premisses són, en general, satisfacibles. Si al afegir-ne les clàusules resultants de negar la conclusió el conjunto resultant és insatisfacible (i el raonament és correcte) aleshores, segons el teorema anterior hi ha prou amb provar com a clàusula cap amb les que resultaren de negar la conclusió.

Resolució ordenada

La resolució ordenada o selectiva és una estratègia de resolució molt restrictiva en la qual cada clàusula es pren com a un conjunt de literals ordenats. La resolució només es realitza amb el primer literal de cada clàusula. Els literals del resolvent mantenen l'ordre de les clàusules pare amb els literals del pare positiu (la clàusula que contenia el literal pel que es resol afirmant) seguits dels literals del pare negatiu (la clàusula que contenia el literal pel que es resol negant).

Exemple

Sigui C = { p ∨ q, ¬p ∨ r, ¬q ∨ r, ¬r, } . A continuació s'aplicarà l'estratègia de resolució d'entrada, per a fer-ho, es seleccionen sempre dues clàusules resolubles tals que una d'elles pertany al conjunt original d'entrada.

La clàusula 5 es l'únic resolvent ordenat entre les clàusules 1 i 4. Les clàusules 1 i 3 no resolen donat que els seus literals complementaris no són els primers. Per la mateixa raó tampoc resolen les clàusules 2 i 4 ni les clàusules 3 i 4. Un cop generada la clàusula 5, resol amb la clàusula 3 per a produir la clàusula 6, la qual resol amb la clàusula 4 per a produir la clàusula buida.

La resolució ordenada es la més eficient (a l'exemple, s'obté la clàusula buida en el tercer pas de resolució). Desafortunadament, la resolució ordenada no és complerta. Però s'ha demostrat que la resolució ordenada sí és complerta per a clàusules Horn.

Els principals sistemes de demostració automàtica basats en el principi de resolució (por exemple, els sistemes Prolog) utilitzen una combinació de les dues últimes estratègies restringides a conjunts de clàusules Horn ^[2].

 

Jordi Coll Vera - 2020