n lo gica Programacio

Curso 200405

Tema 9: Formalizaci on en Prolog de la l ogica proposicional

Jos e A. Alonso Jim enez

Jose-Antonio.Alonso@cs.us.es http://www.cs.us.es/jalonso

Dpto. de Ciencias de la Computaci on e Inteligencia Articial

Universidad de Sevilla

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.1

Sintaxis de la l ogica proposicional

x

Alfabeto proposicional:
u u

s mbolos proposicionales. conectivas l ogicas: (negaci on), (conjunci on), (disyunci on), (condicional), (equivalencia). s mbolos auxiliares: ( y ).

F ormulas proposicionales:
u u

s mbolos proposicionales F , (F G), (F G), (F G), (F G)

.
x

Eliminaci on de par entesis:

u u u

Eliminaci on de par entesis externos. Precedencia: , , , Asociatividad: y asocian por la derecha

Cc Ia
Formalizaci on en Prolog de la l ogica proposicional 9.2

PL 200405

Sintaxis de la l ogica proposicional

x

Sintaxis en Prolog Usual Prolog - & v => <=>

Declaraci on de operadores:
:::::op(610, op(620, op(630, op(640, op(650, fy, xfy, xfy, xfy, xfy, -). &). v). =>). <=>). % % % % % negaci on conjunci on disyunci on condicional equivalencia

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.3

Valores de verdad
x

Valores de verdad:
u

1: verdadero y 0: falso

Def. de valor de verdad:

u

valor de verdad(?V) si V es un valor de verdad. valor_de_verdad(0). valor_de_verdad(1).

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.4

Funciones de verdad
x

Funciones i i i 1 1 0 1 0 1 0 0
u

de verdad: j ij ij ij ij 1 1 1 1 1 0 0 1 0 0 1 0 1 1 0 0 0 0 1 1

funci on de verdad(+Op, +V1, +V2, -V) si Op(V1,V2)=V. funci on de verdad(+Op, +V1, -V) si Op(V1)) = V funci on_de_verdad(v, 0, 0, 0) :- !. funci on_de_verdad(v, _, _, 1). funci on_de_verdad(&, 1, 1, 1) :- !. funci on_de_verdad(&, _, _, 0). funci on_de_verdad(=>, 1, 0, 0) :- !. funci on_de_verdad(=>, _, _, 1). funci on_de_verdad(<=>, X, X, 1) :- !. funci on_de_verdad(<=>, _, _, 0). funci on_de_verdad(-, funci on_de_verdad(-, 1, 0). 0, 1).
Formalizaci on en Prolog de la l ogica proposicional 9.5

PL 200405

Cc Ia

Valor de una f ormula

x

Representaci on de las interpretaciones

u u

Listas de pares de variables y valores de verdad Ejemplo: [(p,1),(r,0),(u,1)]

Def. del valor de una f ormula en una interpretaci on

u u

valor(+F, +I, -V) se verica si el valor de la f ormula F en la interpretaci on I es V Ejemplos: ?- valor((p v q) & (-q v r),[(p,1),(q,0),(r,1)],V). V = 1 ?- valor((p v q) & (-q v r),[(p,0),(q,0),(r,1)],V). V = 0

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.6

Valor de una f ormula

u

Def. de valor: valor(F, I, V) :memberchk((F,V), I). valor(-A, I, V) :valor(A, I, VA), funci on_de_verdad(-, VA, V). valor(F, I, V) :functor(F,Op,2), arg(1,F,A), arg(2,F,B), valor(A, I, VA), valor(B, I, VB), funci on_de_verdad(Op, VA, VB, V).

% F =..[Op,A,B],

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.7

Interpretaciones de una f ormula

x

I interpretaci on principal de F syss I es una aplicaci on del conjunto de los s mbolos proposicionales de F en el conjunto de los valores de verdad. C alculo de las interpretaciones principales:
u

ormula(+F,-L) se verica si L es el conjunto de las interpretaciones interpretaciones f principales de la f ormula F. Ejemplo ?- interpretaciones_f ormula((p v q) & (-q v r),L). L = [[ (p, 0), (q, 0), (r, 0)], [ (p, 0), (q, 0), (r, 1)], [ (p, 0), (q, 1), (r, 0)], [ (p, 0), (q, 1), (r, 1)], [ (p, 1), (q, 0), (r, 0)], [ (p, 1), (q, 0), (r, 1)], [ (p, 1), (q, 1), (r, 0)], [ (p, 1), (q, 1), (r, 1)]]

ormula: Def. de interpretaciones f interpretaciones_f ormula(F,U) :findall(I,interpretaci on_f ormula(I,F),U).

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.8

Interpretaciones de una f ormula

x

Interpretaci on de una f ormula:

u u

interpretaci on f ormula(?I,+F) se verica si I es una interpretaci on de la f ormula F. Ejemplo: ?- interpretaci on_f ormula(I,(p v q) & (-q v r)). I = [ (p, 0), (q, 0), (r, 0)] ; I = [ (p, 0), (q, 0), (r, 1)] ; I = [ (p, 0), (q, 1), (r, 0)] ; I = [ (p, 0), (q, 1), (r, 1)] ; I = [ (p, 1), (q, 0), (r, 0)] ; I = [ (p, 1), (q, 0), (r, 1)] ; I = [ (p, 1), (q, 1), (r, 0)] ; I = [ (p, 1), (q, 1), (r, 1)] ; No

ormula: Def. de interpretaci on f interpretaci on_f ormula(I,F) :s mbolos_f ormula(F,U), interpretaci on_s mbolos(U,I).

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.9

Interpretaciones de una f ormula

x

S mbolos de una f ormula

u

s mbolos f ormula(+F,?U) se verica si U es el conjunto ordenado de los s mbolos proposicionales de la f ormula F. Ejemplo: ?- s mbolos_f ormula((p v q) & (-q v r), U). U = [p, q, r] ormula Def. de s mbolo f s mbolos_f ormula(F,U) :s mbolos_f ormula_aux(F,U1), sort(U1,U). s mbolos_f ormula_aux(F,[F]) :atom(F). s mbolos_f ormula_aux(-F,U) :s mbolos_f ormula_aux(F,U). s mbolos_f ormula_aux(F,U) :arg(1,F,A), arg(2,F,B), s mbolos_f ormula_aux(A,UA), s mbolos_f ormula_aux(B,UB), union(UA,UB,U).
Cc Ia

% F =..[_Op,A,B],

PL 200405

Formalizaci on en Prolog de la l ogica proposicional

9.10

Interpretaciones de una f ormula

x

Interpretaci on de una lista de s mbolos:

u

mbolos(+L,-I) se verica si I es una interpretaci on de la lista de interpretaci on s s mbolos proposicionales L. Ejemplo: ?- interpretaci on_s mbolos([p,q,r],I). I = [ (p, 0), (q, 0), (r, 0)] ; I = [ (p, 0), (q, 0), (r, 1)] ; I = [ (p, 0), (q, 1), (r, 0)] ; I = [ (p, 0), (q, 1), (r, 1)] ; I = [ (p, 1), (q, 0), (r, 0)] ; I = [ (p, 1), (q, 0), (r, 1)] ; I = [ (p, 1), (q, 1), (r, 0)] ; I = [ (p, 1), (q, 1), (r, 1)] ; No

Def. de interpretaci on s mbolos interpretaci on_s mbolos([],[]). interpretaci on_s mbolos([A|L],[(A,V)|IL]) :valor_de_verdad(V), interpretaci on_s mbolos(L,IL).

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.11

Modelo de una f ormula

x

La interpretaci on I es un modelo de la f ormula F si el valor de F en I es verdadero. Comprobaci on de modelo de una f ormula:

u

es modelo f ormula(+I,+F) se verica si la interpretaci on I es un modelo de la f ormula F. Ejemplos: ?- es_modelo_f ormula([(p,1),(q,0),(r,1)], (p v q) & (-q v r)). Yes ?- es_modelo_f ormula([(p,0),(q,0),(r,1)], (p v q) & (-q v r)). No

Def. de es modelo f ormula: es_modelo_f ormula(I,F) :valor(F,I,V), V = 1.

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.12

C alculo de los modelos de una f ormula

x

C alculo de los modelos principales de una f ormula:

u u

modelo f ormula(?I,+F) se verica si I es un modelo principal de la f ormula F. Ejemplo: ?- modelo_f ormula(I,(p v q) & (-q v r)). I = [ (p, 0), (q, 1), (r, 1)] ; I = [ (p, 1), (q, 0), (r, 0)] ; I = [ (p, 1), (q, 0), (r, 1)] ; I = [ (p, 1), (q, 1), (r, 1)] ; No

Def. de modelo f ormula: modelo_f ormula(I,F) :interpretaci on_f ormula(I,F), es_modelo_f ormula(I,F).

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.13

C alculo de los modelos de una f ormula

u

modelos f ormula(+F,-L) se verica si L es el conjunto de los modelos principales de la f ormula F. Ejemplo: ?- modelos_f ormula((p v q) & L = [[ (p, 0), (q, 1), (r, [ (p, 1), (q, 0), (r, [ (p, 1), (q, 0), (r, [ (p, 1), (q, 1), (r, (-q v r),L). 1)], 0)], 1)], 1)]]

Def. de modelos f ormula modelos_f ormula(F,L) :findall(I,modelo_f ormula(I,F),L).

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.14

Satisfacibilidad
x

Una f ormula es satisfacible si tiene modelo e insatisfacible si no lo tiene. Comprobaci on de satisfacibilidad:

u u

es satisfacible(+F) se verica si la f ormula F es satisfacible. Ejemplos: ?- es_satisfacible((p v q) & (-q v r)). Yes ?- es_satisfacible((p & q) & (p => r) & (q => -r)). No

Def. de es satisfacible: es_satisfacible(F) :interpretaci on_f ormula(I,F), es_modelo_f ormula(I,F).

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.15

Contramodelo de una f ormula

x

Un contramodelo principal de F es una interpretaci on principal de F que no es modelo de F . C alculo de contramodelos:

u

contramodelo f ormula(?I,+F) se verica si I es un contramodelo principal de la f ormula F. Ejemplos: ?- contramodelo_f ormula(I, p <=> q). I = [ (p, 0), (q, 1)] ; I = [ (p, 1), (q, 0)] ; No ?- contramodelo_f ormula(I, p => p). No

ormula: Def. de contramodelo f contramodelo_f ormula(I,F) :interpretaci on_f ormula(I,F), \+ es_modelo_f ormula(I,F).

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.16

Validez. Tautolog as
x

F es v alida (o tautolog a) si todas las interpretaciones son modelos de F. Comprobaci on de tautolog as:
u u

es tautolog a(+F) se verica si la f ormula F es una tautolog a. Ejemplos: ?- es_tautolog a((p => q) v (q => p)). Yes ?- es_tautolog a(p => q). No

Def. de es tautolog a: es_tautolog a(F) :\+ contramodelo_f ormula(_I,F).

Denici on alternativa: es_tautolog a_alt(F) :\+ es_satisfacible(-F).

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.17

Interpretaciones de conjuntos
x

Una interpretaci on principal de un conjunto de f ormulas es una aplicaci on del conjunto de sus s mbolos proposicionales en el conjunto de los valores de verdad. C alculo de las interpretaciones principales de un conjunto de f ormulas:
u

interpretaciones conjunto(+S,-L) se verica si L es el conjunto de las interpretaciones principales del conjunto S. Ejemplo: ?- interpretaciones_conjunto([p => q, q=> r],U). U = [[ (p, 0), (q, 0), (r, 0)], [ (p, 0), (q, [ (p, 0), (q, 1), (r, 0)], [ (p, 0), (q, [ (p, 1), (q, 0), (r, 0)], [ (p, 1), (q, [ (p, 1), (q, 1), (r, 0)], [ (p, 1), (q, 0), 1), 0), 1), (r, (r, (r, (r, 1)], 1)], 1)], 1)]]

Def. de interpretaciones conjunto: interpretaciones_conjunto(S,U) :findall(I,interpretaci on_conjunto(I,S),U).

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.18

Interpretaciones de conjuntos
u

interpretaci on conjunto(?I,+S) se verica si I es una interpretaci on del conjunto de f ormulas S. Ejemplo: ?- interpretaci on_conjunto(I,[p I = [ (p, 0), (q, 0), (r, 0)] I = [ (p, 0), (q, 0), (r, 1)] I = [ (p, 0), (q, 1), (r, 0)] I = [ (p, 0), (q, 1), (r, 1)] I = [ (p, 1), (q, 0), (r, 0)] I = [ (p, 1), (q, 0), (r, 1)] I = [ (p, 1), (q, 1), (r, 0)] I = [ (p, 1), (q, 1), (r, 1)] No => q, q=> r]). ; ; ; ; ; ; ; ;

Def. de interpretaci on conjunto: interpretaci on_conjunto(I,S) :s mbolos_conjunto(S,U), interpretaci on_s mbolos(U,I).

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.19

Interpretaciones de conjuntos
x

C alculo de los s mbolos de un conjunto de f ormulas:

u

s mbolos conjunto(+S,?U) se verica si U es el conjunto ordenado de los s mbolos proposicionales del conjunto de f ormulas S. Ejemplo: ?- s mbolos_conjunto([p => q, q=> r],U). U = [p, q, r]

Def. de s mbolos conjunto: s mbolos_conjunto(S,U) :s mbolos_conjunto_aux(S,U1), sort(U1,U). s mbolos_conjunto_aux([],[]). s mbolos_conjunto_aux([F|S],U) :s mbolos_f ormula(F,U1), s mbolos_conjunto_aux(S,U2), union(U1,U2,U).
Cc Ia

PL 200405

Formalizaci on en Prolog de la l ogica proposicional

9.20

Modelo de un conjunto de f ormulas

x

La interpretaci on I es un modelo del conjunto de f ormulas S si I es modelo de todas las f ormulas de S . Comprobaci on de modelo de un conjunto de f ormulas
u

es modelo conjunto(+I,+S) se verica si la interpretaci on I es un modelo del conjunto de f ormulas S. Ejemplos: ?- es_modelo_conjunto([(p,1),(q,0),(r,1)], [(p v q) & (-q v r),q => r]). Yes ?- es_modelo_conjunto([(p,0),(q,1),(r,0)], [(p v q) & (-q v r),q => r]). No

Def. de es modelo conjunto: es_modelo_conjunto(_I,[]). es_modelo_conjunto(I,[F|S]) :es_modelo_f ormula(I,F), es_modelo_conjunto(I,S).

Cc Ia

PL 200405

Formalizaci on en Prolog de la l ogica proposicional

9.21

C alculo de modelos de conjuntos

x

C alculo de los modelos principales de conjuntos de f ormulas

u

modelo conjunto(?I,+S) se verica si I es un modelo principal del conjunto de f ormulas S. Ejemplo: ?- modelo_conjunto(I,[(p v q) & I = [ (p, 0), (q, 1), (r, 1)] I = [ (p, 1), (q, 0), (r, 1)] I = [ (p, 1), (q, 1), (r, 1)] No (-q v r),p => r]). ; ; ;

Def. de modelo conjunto: modelo_conjunto(I,S) :interpretaci on_conjunto(I,S), es_modelo_conjunto(I,S).

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.22

C alculo de modelos de conjuntos

u

modelos conjunto(+S,-L) se verica si L es el conjunto de los modelos principales del conjunto de f ormulas S. Ejemplo: ?- modelos_conjunto([(p v q) L = [[ (p, 0), (q, 1), (r, [ (p, 1), (q, 0), (r, [ (p, 1), (q, 1), (r, & (-q v r),p => r],L). 1)], 1)], 1)]]

Def. de modelos conjunto: modelos_conjunto(S,L) :findall(I,modelo_conjunto(I,S),L).

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.23

Consistencia de un conjunto
x

Un conjunto de f ormulas es consistente si tiene modelo e inconsistente en caso contrario. Comprobaci on de consistencia:
u

consistente(+S) se verica si el conjunto de f ormulas S es consistente e inconsistente(+S), si es inconsistente. Ejemplos: ?- consistente([(p v q) & (-q v r),p => r]). Yes ?- consistente([(p v q) & (-q v r),p => r, -r]). No

Def. de consistente e inconsistente: consistente(S) :modelo_conjunto(_I,S), !. inconsistente(S) :\+ modelo_conjunto(_I,S).

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.24

Consecuencia l ogica
x

La f ormula F es consecuencia l ogica del conjunto de f ormulas S (S |= F ) si todos los modelos de S son modelos de F . (S |= F ) syss todas las interpretaciones principales de S {F } que son modelos de S tambi en son modelos de F . Comprobaci on de consecuencia l ogica:
u

ormula F es consecuencia del conjunto de es consecuencia(+S,+F) se verica si la f f ormulas S. Ejemplos: ?- es_consecuencia([p => q, q => r], p => r). Yes ?- es_consecuencia([p], p & q). No

Def. de es consecuencia: es_consecuencia(S,F) :\+ contramodelo_consecuencia(S,F,_I).

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.25

Consecuencia l ogica
u

contramodelo consecuencia(+S,+F,?I) se verica si I es una interpretaci on principal de S {F} que es modelo del conjunto de f ormulas S pero no es modelo de la f ormula F. Ejemplos: ?- contramodelo_consecuencia([p], p & q, I). I = [ (p, 1), (q, 0)] ; No ?- contramodelo_consecuencia([p => q, q=> r], p => r, I). No

Def. de contramodelo consecuencia: contramodelo_consecuencia(S,F,I) :interpretaci on_conjunto(I,[F|S]), es_modelo_conjunto(I,S), \+ es_modelo_f ormula(I,F).

Denici on alternativa de es consecuencia:

es_consecuencia_alt(S,F) :inconsistente([-F|S]).

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.26

Ejemplo: veraces y mentirosos

x

El problema de los veraces y los mentirosos:

u

Enunciado: En una isla hay dos tribus, la de los veraces (que siempre dicen la verdad) y la de los mentirosos (que siempre mienten). Un viajero se encuentra con tres isle nos A, B y C y cada uno le dice una frase A dice B y C son veraces syss C es veraz B dice Si A y B son veraces, entonces B y C son veraces y A es mentiroso C dice B es mentiroso syss A o B es veraz Determinar a qu e tribu pertenecen A, B y C.

Representaci on: a, b y c representan que A, B y C son veraces -a, -b y -c representan que A, B y C son mentirosos

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.27

Ejemplo: veraces y mentirosos

u

Idea: las tribus se determinan a partir de los modelos del conjunto de f ormulas correspondientes a las tres frases. ?- modelos_conjunto([a <=> b <=> c <=> L). L = [[ (a, 1), (b, 1), (c, (b & c <=> c), (a & c => b & c & -a), (-b <=> a v b)], 0)]]

Soluci on: A y B son veraces y C es mentiroso.

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.28

Ejemplo: El problema de los animales

x

El problema de los animales

u

Enunciado: Disponemos de una base de conocimiento compuesta de reglas sobre clasicaci on de animales y hechos sobre caracter sticas de un animal. Regla 1: Si un animal es ungulado y tiene rayas negras, entonces es una cebra. Regla 2: Si un animal rumia y es mam fero, entonces es ungulado. Regla 3: Si un animal es mam fero y tiene pezu nas, entonces es ungulado. Hecho 1: El animal tiene es mam fero. Hecho 2: El animal tiene pezu nas. Hecho 3: El animal tiene rayas negras. Demostrar a partir de la base de conocimientos que el animal es una cebra.

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.29

Ejemplo: El problema de los animales

u

Soluci on: ?- es_consecuencia( [es_ungulado & tiene_rayas_negras => es_cebra, rumia & es_mamifero => es_ungulado, es_mamifero & tiene_pezugnas => es_ungulado, es_mamifero, tiene_pezugnas, tiene_rayas_negras], es_cebra). Yes

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.30

Ejemplo: Problema de los trabajos

x

El problema de los trabajos

u

Enunciado: Juan, Sergio y Carlos trabajan de programador, ingeniero y administrador (aunque no necesariamente en este orden). Juan le debe 1000 euros al programador. La esposa del administrador le ha prohibido a su marido pedir dinero prestado (y este le obedece). Sergio est a soltero. Determinar el trabajo de cada uno. Representaci on: cp (Carlos es programador) ci (Carlos es ingeniero) ca (Carlos es administrador) jp (Juan es programador) ji (Juan es ingeniero) ja (Juan es administrador) sp (Sergio es programador) si (Sergio es ingeniero) sa (Sergio es administrador).

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.31

Ejemplo: Problema de los trabajos

u

Soluci on:

modelos_conjunto( [jp v ji v ja, % Juan es programador, ingeniero o administrador sp v si v sa, % Sergio es programador, ingeniero o administrador cp v ci v ca, % Carlos es programador, ingeniero o administrador % No hay m as de un programador: (jp & -sp & -cp) v (-jp & sp & -cp) v (-jp & -sp & cp), % No hay m as de un ingeniero: (ji & -si & -ci) v (-ji & si & -ci) v (-ji & -si & ci), % No hay m as de un administrador: (ja & -sa & -ca) v (-ja & sa & -ca) v (-ja & -sa & ca), % Juan le debe 1000 pesetas al programador [Luego, Juan no es el programador]: -jp, % La esposa del administrador le ha prohibido a su marido pedir dinero % prestado (y este le obedece) [Luego, Juan no es el administrador]: -ja, % Sergio est a soltero [Luego, no es el adminitrador]: -sa], L). L = [[(ca,1),(ci,0),(cp,0), (ja,0),(ji,1),(jp,0), (sa,0),(si,0),(sp,1)]].
u

Conclusi on: Carlos es administrador, Juan es ingeniero y Sergio es programador.

Cc Ia
Formalizaci on en Prolog de la l ogica proposicional 9.32

PL 200405

Ejemplo: El problema de los cuadrados

x

El problema de los cuadrados

u

Enunciado: Existe nueve s mbolos proposicionales que se pueden ordenar en un cuadrado. Se sabe que existe alguna letra tal que para todos los n umeros las f ormulas son verdaderas (es decir, existe una la de f ormulas verdaderas). El objetivo de este ejercicio demostrar que para cada n umero existe una letra cuya f ormula es verdadera (es decir, en cada columna existe una f ormula verdadera). a1 b1 c1 a2 b2 c2 a3 b3 c3 & a2 & a3) v & b2 & b3) v & c2 & c3) v b1 v c1) & v b2 v c2) & v b3 v c3)).
Formalizaci on en Prolog de la l ogica proposicional 9.33

Soluci on: ?- es_tautolog a((a1 (b1 (c1 => (a1 (a2 (a3 Yes

PL 200405

Cc Ia

Ejemplo: Problema del coloreado

x

El problema del coloreado del pent agono (con dos colores)

u

Enunciado: Demostrar que es imposible colorear los v ertices de un pent agono de rojo o azul de forma que los v ertices adyacentes tengan colores distintos. Representaci on: 1, 2, 3, 4, 5 representan los v ertices consecutivos del pent agono ri (1 i 5) representa que el v ertice i es rojo ai (1 i 5) representa que el v ertice i es azul

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.34

Ejemplo: Problema del coloreado

u

Soluci on: ?- inconsistente( [% El v ertice i (1 <= i <= 5) es azul o rojo: a1 v r1, a2 v r2, a3 v r3, a4 v r4, a5 v r5, % Un v ertice no puede tener dos colores: a1 => -r1, r1 => -a1, a2 => -r2, r2 => -a2, a3 => -r3, r3 => -a3, a4 => -r4, r4 => -a4, a5 => -r5, r5 => -a5, % Dos v ertices adyacentes no pueden ser azules: -(a1 & a2), -(a2 & a3), -(a3 & a4), -(a4 & a5), -(a5 & a1), % Dos v ertices adyacentes no pueden ser rojos: -(r1 & r2), -(r2 & r3), -(r3 & r4), -(r4 & r5), -(r5 & r1)]). Yes

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.35

Ejemplo: Problema del coloreado

x

El problema del coloreado del pent agono (con tres colores)

u

Enunciado: Demostrar que es posible colorear los v ertices de un pent agono de rojo, azul o negro de forma que los v ertices adyacentes tengan colores distintos. Soluci on:

?- modelo_conjunto(I, [% El v ertice i (1 <= i <= 5) azul, rojo o negro: a1 v r1 v n1, a2 v r2 v n2, a3 v r3 v n3, a4 v r4 v n4, a5 v r5 v n5, % Un v ertice no puede tener dos colores: a1 => -r1 & -n1, r1 => -a1 & -n1, n1 => -a1 a2 => -r2 & -n2, r2 => -a2 & -n2, n2 => -a2 a3 => -r3 & -n3, r3 => -a3 & -n3, n3 => -a3 a4 => -r4 & -n4, r4 => -a4 & -n4, n4 => -a4 a5 => -r5 & -n5, r5 => -a5 & -n5, n5 => -a5 & & & & & -r1, -r2, -r3, -r4, -r5,

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.36

Ejemplo: Problema del coloreado

% Dos v ertices adyacentes no pueden ser azules: -(a1 & a2), -(a2 & a3), -(a3 & a4), -(a4 & a5), -(a5 & a1), % Dos v ertices adyacentes no pueden ser rojos: -(r1 & r2), -(r2 & r3), -(r3 & r4), -(r4 & r5), -(r5 & r1), % Dos v ertices adyacentes no pueden ser negros: -(n1 & n2), -(n2 & n3), -(n3 & n4), -(n4 & n5), -(n5 & n1)]). I = [ (a1,0),(a2,0),(a3,0),(a4,0),(a5,1), (n1,0),(n2,1),(n3,0),(n4,1),(n5,0), (r1,1),(r2,0),(r3,1),(r4,0),(r5,0)].
u

Conclusi on: colorear el v ertice 1 de rojo, el 2 de negro, el 3 de rojo, el 4 de negro y el 5 de azul.

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.37

Ejemplo: Problema del palomar

x

El problema del palomar

u

Enunciado: Cuatro palomas comparten tres huecos. Demostrar que dos palomas tienen que estar en la misma hueco. Representaci on: pihj (i= 1, 2, 3, 4 y j= 1, 2, 3) representa que la paloma i est a en la hueco j.

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.38

Ejemplo: Problema del palomar

u

Soluci on:

?- inconsistente([ % La paloma i est a en alguna hueco: p1h1 v p1h2 v p1h3, p2h1 v p2h2 v p2h3, p3h1 v p3h2 v p3h3, p4h1 v p4h2 v p4h3, % No hay dos palomas en la hueco 1: -p1h1 v -p2h1, -p1h1 v -p3h1, -p1h1 v -p4h1, -p2h1 v -p3h1, -p2h1 v -p4h1, -p3h1 v -p4h1, % No hay dos palomas en la hueco 2: -p1h2 v -p2h2, -p1h2 v -p3h2, -p1h2 v -p4h2, -p2h2 v -p3h2, -p2h2 v -p4h2, -p3h2 v -p4h2, % No hay dos palomas en la hueco 3: -p1h3 v -p2h3, -p1h3 v -p3h3, -p1h3 v -p4h3, -p2h3 v -p3h3, -p2h3 v -p4h3, -p3h3 v -p4h3]). Yes

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.39

Ejemplo: Problema de los rect angulos

x

El problema de los rect angulos

u

Enunciado: Un rect angulo se divide en seis rect angulos menores como se indica en la gura. Demostrar que si cada una de los rect angulos menores tiene un lado cuya medida es un n umero entero, entonces la medida de alguno de los lados del rect angulo mayor es un n umero entero.
A C F D E B

Representaci on base: la base del rect angulo mayor es un n umero entero altura: la altura del rect angulo mayor es un n umero entero base x: la base del rect angulo X es un n umero entero altura x: la altura del rect angulo X es un n umero entero

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.40

Soluci on: altura_b, altura_d, altura_f,

?- es_consecuencia( [base_a v altura_a, base_b v base_c v altura_c, base_d v base_e v altura_e, base_f v base_a <=> base_c, base_a & base_d => base_f, base_f & base_a => base_d, base_f & base_d => base_a, base_d & base_e => base_b, base_b & base_d => base_e, base_b & base_e => base_d, base_a & base_b => base, base & base_a => base_b, base & base_b => base_a, base_a & base_d & base_e => base & base_a & base_d => base & base_a & base_e => base & base_d & base_e => base_f & base_e => base, base & base_f => base_e, base & base_e => base_f,

base, base_e, base_d, base_a,

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.41

Ejemplo: Problema de los rect angulos

altura_d & altura_f altura_e & altura_d altura_e & altura_f altura_a & altura_c altura & altura_a altura & altura_a altura & altura_c altura_b & altura_d altura & altura_b altura & altura_b altura & altura_d altura_b & altura_e altura & altura_b altura & altura_e base v altura). Yes => altura_e, => altura_f, => altura_d, & altura_f => & altura_c => & altura_f => & altura_f => & altura_f => & altura_d => & altura_f => & altura_f => => altura, => altura_e, => altura_b],

altura, altura_f, altura_c, altura_a, altura, altura_f, altura_d, altura_b,

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.42

Ejemplo: Problema de las 4 reinas

x

El problema de las 4 reinas

u

Enunciado: Calcular las formas de colocar 4 reinas en un tablero de 4x4 de forma que no haya m as de una reina en cada la, columna o diagonal. Representaci on: cij (1 i, j 4) indica que hay una reina en la la i columna j.

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.43

Ejemplo: Problema de las 4 reinas

u

Soluci on:

?- modelos_conjunto([ % En cada fila hay una reina: c11 v c12 v c13 v c14, c21 v c22 v c23 v c24, c31 v c32 v c33 v c34, c41 v c42 v c43 v c44, % Si en una casilla hay reina, entonces no hay m as c11 => (-c12 & -c13 & -c14) & (-c21 & -c31 & -c41) c12 => (-c11 & -c13 & -c14) & (-c22 & -c32 & -c42) c13 => (-c11 & -c12 & -c14) & (-c23 & -c33 & -c43) c14 => (-c11 & -c12 & -c13) & (-c24 & -c34 & -c44) c21 => (-c22 & -c23 & -c24) & (-c11 & -c31 & -c41) c22 => (-c21 & -c23 & -c24) & (-c12 & -c32 & -c42) & (-c13 & -c31), c23 => (-c21 & -c22 & -c24) & (-c13 & -c33 & -c43) & (-c14 & -c32 & -c41), c24 => (-c21 & -c22 & -c23) & (-c14 & -c34 & -c44) c31 => (-c32 & -c33 & -c34) & (-c11 & -c21 & -c41) c32 => (-c31 & -c33 & -c34) & (-c12 & -c22 & -c42) & (-c14 & -c23 & -c41),

reinas en & (-c22 & & (-c21 & & (-c31 & & (-c23 & & (-c32 & & (-c11 &

sus l neas: -c33 & -c44), -c23 & -c34), -c22 & -c24), -c32 & -c41), -c43 & -c12), -c33 & -c44)

& (-c12 & -c34) & -c13 & (-c33 & -c42), & -c42 & (-c13 & -c22), & (-c21 & -c43)

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.44

Ejemplo: Problema de las 4 reinas

c33 => (-c31 & & (-c24 c34 => (-c31 & c41 => (-c42 & c42 => (-c41 & c43 => (-c41 & c44 => (-c41 & L), -c32 & -c34) & -c42), -c32 & -c33) -c43 & -c44) -c43 & -c44) -c42 & -c44) -c42 & -c43) & (-c13 & -c23 & -c43) & (-c11 & -c22 & -c44) & & & & & (-c14 (-c11 (-c12 (-c13 (-c14 & & & & & -c24 -c21 -c22 -c23 -c24 & & & & & -c44) -c31) -c32) -c33) -c34) & & & & & (-c12 (-c14 (-c31 (-c21 (-c11 & & & & & -c23 -c23 -c24 -c32 -c22 & & & & & -c43), -c32), -c33), -c34), -c33)],

L = [[(c11,0),(c12,0),(c13,1),(c14,0),(c21,1),(c22,0),(c23,0),(c24,0), (c31,0),(c32,0),(c33,0),(c34,1),(c41,0),(c42,1),(c43,0),(c44,0)], [(c11,0),(c12,1),(c13,0),(c14,0),(c21,0),(c22,0),(c23,0),(c24,1), (c31,1),(c32,0),(c33,0),(c34,0),(c41,0),(c42,0),(c43,1),(c44,0)]]

u

Conclusi on: Gr acamente los modelos son

R R R R R R
Formalizaci on en Prolog de la l ogica proposicional 9.45

R R

PL 200405

Cc Ia

Ejemplo: Problema de Ramsey

x

El problema de Ramsey
u

Enunciado: Probar el caso m as simple del teorema de Ramsey: entre seis personas siempre hay (al menos) tres tales que cada una conoce a las otras dos o cada una no conoce a ninguna de las otras dos. Representaci on: 1,2,3,4,5,6 representan a las personas pij (1 i < j 6) indica que las personas i y j se conocen.

Soluci on: ellas: v (p12 v (p13 v (p23 v (p24 v (p35

?- es_tautolog a( % Hay 3 personas que se conocen entre (p12 & p13 & p23) v (p12 & p14 & p24) (p13 & p14 & p34) v (p13 & p15 & p35) (p14 & p16 & p46) v (p15 & p16 & p56) (p23 & p26 & p36) v (p24 & p25 & p45) (p34 & p35 & p45) v (p34 & p36 & p46)
PL 200405

& & & & &

p15 p16 p24 p26 p36

& & & & &

p25) p36) p34) p46) p56)

v v v v v

(p12 (p14 (p23 (p25 (p45

& & & & &

p16 p15 p25 p26 p46

& & & & &

p26) p45) p35) p56) p56)

v v v v v
9.46

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

Ejemplo: Problema de Ramsey

% Hay (-p12 (-p12 (-p13 (-p13 (-p14 (-p23 (-p23 (-p24 (-p34 (-p35 Yes 3 & & & & & & & & & & personas tales -p13 & -p23) v -p15 & -p25) v -p14 & -p34) v -p16 & -p36) v -p16 & -p46) v -p24 & -p34) v -p26 & -p36) v -p26 & -p46) v -p35 & -p45) v -p36 & -p56) v que cada una (-p12 & -p14 (-p12 & -p16 (-p13 & -p15 (-p14 & -p15 (-p15 & -p16 (-p23 & -p25 (-p24 & -p25 (-p25 & -p26 (-p34 & -p36 (-p45 & -p46 desconoce a las otras dos: & -p24) v & -p26) v & -p35) v & -p45) v & -p56) v & -p35) v & -p45) v & -p56) v & -p46) v & -p56)).

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.47

Ejemplos: Comparaci on
x

Comparaci on de la resoluci on de los problemas: Problema S mbolos Inferencias Tiempo mentirosos 3 646 0.00 animales 6 4,160 0.00 trabajos 9 71,044 0.07 cuadrados 9 56,074 0.06 pent agono 3 15 117,716 0.13 palomar 12 484,223 0.50 rect angulos 14 1,026,502 1.08 4 reinas 16 15,901,695 19.90 Ramsey 15 29,525,686 44.27

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.48

Bibliograf a
x

Alonso, J.A. y Borrego, J. Deducci on autom atica (Vol. strucci on l ogica de sistemas l ogicos) (Ed. Kronos, 2002) www.cs.us.es/~jalonso/libros/da1-02.pdf
u

1:

Con-

Cap. 3: Elementos de l ogica proposicional

BenAri, M. Mathematical Logic for Computer Science (2nd ed.) (Springer, 2001)
u

Cap. 2: Propositional Calculus: Formulas, Models, Tableaux

Fitting, M. First-Order Logic and Automated Theorem Proving (2nd ed.) (Springer, 1995) Nerode,A. y Shore, R.A. Logic for Applications (Springer, 1997)

PL 200405

Cc Ia

Formalizaci on en Prolog de la l ogica proposicional

9.49