PDF de programación - Tema 14: Formalización en Prolog de la lógica proposicional - Lógica informática (2015–16)

PD Tema 14: Formalización en Prolog de la lógica proposicional

Lógica informática (2015–16)

Tema 14: Formalización en Prolog de la lógica proposicional

José A. Alonso Jiménez
Andrés Cordón Franco
María J. Hidalgo Doblado

Grupo de Lógica Computacional

Departamento de Ciencias de la Computación e I.A.

Universidad de Sevilla

1 / 34

PD Tema 14: Formalización en Prolog de la lógica proposicional

Tema 14: Formalización en Prolog de la lógica
proposicional

1. Sintaxis de la lógica proposicional

2. Semántica de la lógica proposicional

2 / 34

PD Tema 14: Formalización en Prolog de la lógica proposicional

Sintaxis de la lógica proposicional

Tema 14: Formalización en Prolog de la lógica
proposicional

1. Sintaxis de la lógica proposicional

2. Semántica de la lógica proposicional

3 / 34

PD Tema 14: Formalización en Prolog de la lógica proposicional

Sintaxis de la lógica proposicional

Sintaxis de la lógica proposicional

Sintaxis en Prolog

=>
Declaración de operadores:

&

Usual
Prolog

¬ ∧ ∨ → ↔
-
<=>

v

:- op(610, fy,
-).
:- op(620, xfy, &).
:- op(630, xfy, v).
:- op(640, xfy, =>).
:- op(650, xfy, <=>).

% negación
% conjunción
% disyunción
% condicional
% equivalencia

4 / 34

PD Tema 14: Formalización en Prolog de la lógica proposicional

Semántica de la lógica proposicional

Tema 14: Formalización en Prolog de la lógica
proposicional

1. Sintaxis de la lógica proposicional

2. Semántica de la lógica proposicional

Satisfacibilidad
Validez. Tautologías
Consistencia de un conjunto de fórmulas
Consecuencia lógica

5 / 34

PD Tema 14: Formalización en Prolog de la lógica proposicional

Semántica de la lógica proposicional

Satisfacibilidad

Tema 14: Formalización en Prolog de la lógica
proposicional

1. Sintaxis de la lógica proposicional

2. Semántica de la lógica proposicional

Satisfacibilidad

Valores y funciones de verdad
Funciones de verdad
Valor de una fórmula en una interpretación
Interpretaciones de una fórmula
Modelo de una fórmula
Satisfacibilidad

Validez. Tautologías

Contramodelos de una fórmula
Validez. Tautologías

Consistencia de un conjunto de fórmulas

Interpretaciones principales de un conjunto de fórmulas
Modelo de un conjunto de fórmulas
Cálculo de modelos de conjuntos de fórmulas
Consistencia de un conjunto de fórmulas

Consecuencia lógica

6 / 34

PD Tema 14: Formalización en Prolog de la lógica proposicional

Semántica de la lógica proposicional

Satisfacibilidad

Valores de verdad
Valores de verdad:

1: verdadero y 0: falso

Def. de valor_de_verdad:

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

valor_de_verdad(0).
valor_de_verdad(1).

7 / 34

PD Tema 14: Formalización en Prolog de la lógica proposicional

Semántica de la lógica proposicional

Satisfacibilidad

Funciones de verdad

función_de_verdad(+Op, +V1, +V2, -V) se verifica si el valor

de verdad de la conectiva binaria Op aplicada a los valores de
verdad V1 y V2 es V.

función_de_verdad(+Op, +V1, -V) se verifica si el valor de

verdad de la conectiva unaria Op aplicada al valor de verdad V1 es
V.

función_de_verdad(v,
función_de_verdad(v,
función_de_verdad(&,
función_de_verdad(&,
función_de_verdad(=>,
función_de_verdad(=>,
función_de_verdad(<=>, X, X, 1) :- !.
función_de_verdad(<=>, _, _, 0).

0, 0, 0) :- !.
_, _, 1).
1, 1, 1) :- !.
_, _, 0).
1, 0, 0) :- !.
_, _, 1).

función_de_verdad(-,
función_de_verdad(-,

1, 0).
0, 1).

8 / 34

PD Tema 14: Formalización en Prolog de la lógica proposicional

Semántica de la lógica proposicional

Satisfacibilidad

Valor de una fórmula

Representación de las interpretaciones

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

Def. del valor de una fórmula en una interpretación:

valor(+F, +I, -V) se verifica si el valor de la fórmula F en la
interpretación I es V. Por ejemplo,
?- 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

9 / 34

PD Tema 14: Formalización en Prolog de la lógica proposicional

Semántica de la lógica proposicional

Satisfacibilidad

Valor de una fórmula

Def. de valor:

valor(F, I, V) :-

memberchk((F,V), I).

valor(-A, I, V) :-

valor(A, I, VA),
función_de_verdad(-, VA, V).

valor(F, I, V) :-
F =..[Op,A,B],
valor(A, I, VA),
valor(B, I, VB),
función_de_verdad(Op, VA, VB, V).

10 / 34

PD Tema 14: Formalización en Prolog de la lógica proposicional

Semántica de la lógica proposicional

Satisfacibilidad

Interpretaciones principales de una fórmula

I es una interpretación principal de F syss I es una aplicación del
conjunto de los símbolos proposicionales de F en el conjunto de
los valores de verdad.

Cálculo de las interpretaciones principales:

interpretaciones_fórmula(+F,-L) se verifica si L es el

conjunto de las interpretaciones principales de la fórmula F. Por
ejemplo,
?- interpretaciones_fórmula((p v q) & (-q v r),L).
L = [[ (p, 0), (q, 0), (r, 0)],
(r, 1)],
(r, 0)],
(r, 1)],
(r, 0)],
(r, 1)],
(r, 0)],
(r, 1)]]

[ (p, 0),
[ (p, 0),
[ (p, 0),
[ (p, 1),
[ (p, 1),
[ (p, 1),
[ (p, 1),

(q, 0),
(q, 1),
(q, 1),
(q, 0),
(q, 0),
(q, 1),
(q, 1),

interpretaciones_fórmula(F,U) :-

findall(I,interpretación_fórmula(I,F),U).

11 / 34

PD Tema 14: Formalización en Prolog de la lógica proposicional

Semántica de la lógica proposicional

Satisfacibilidad

Interpretación de una fórmula

interpretación_fórmula(?I,+F) se verifica si I es una

interpretación de la fórmula F. Por ejemplo,
?- interpretación_fórmula(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

interpretación_fórmula(I,F) :-

símbolos_fórmula(F,U),
interpretación_símbolos(U,I).

12 / 34

PD Tema 14: Formalización en Prolog de la lógica proposicional

Semántica de la lógica proposicional

Satisfacibilidad

Símbolos de una fórmula

símbolos_fórmula(+F,?U) se verifica si U es el conjunto

ordenado de los símbolos proposicionales de la fórmula F. Por
ejemplo,
?- símbolos_fórmula((p v q) & (-q v r), U).
U = [p, q, r]

símbolos_fórmula(F,U) :-

símbolos_fórmula_aux(F,U1),
sort(U1,U).

símbolos_fórmula_aux(F,[F]) :-

atom(F).

símbolos_fórmula_aux(-F,U) :-
símbolos_fórmula_aux(F,U).

símbolos_fórmula_aux(F,U) :-

F =..[_Op,A,B],
símbolos_fórmula_aux(A,UA),
símbolos_fórmula_aux(B,UB),
union(UA,UB,U).

13 / 34

PD Tema 14: Formalización en Prolog de la lógica proposicional

Semántica de la lógica proposicional

Satisfacibilidad

Interpretación de una lista de símbolos
interpretación_símbolos(+L,-I) se verifica si I es una
interpretación de la lista de símbolos proposicionales L. Por
ejemplo,
?- interpretación_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

interpretación_símbolos([],[]).
interpretación_símbolos([A|L],[(A,V)|IL]) :-

valor_de_verdad(V),
interpretación_símbolos(L,IL).

14 / 34

PD Tema 14: Formalización en Prolog de la lógica proposicional

Semántica de la lógica proposicional

Satisfacibilidad

Comprobación de modelo de una fórmula

es_modelo_fórmula(+I,+F) se verifica si la interpretación I es

un modelo de la fórmula F. Por ejemplo,
?- es_modelo_fórmula([(p,1),(q,0),(r,1)],
(p v q) & (-q v r)).

Yes
?- es_modelo_fórmula([(p,0),(q,0),(r,1)],
(p v q) & (-q v r)).

No

es_modelo_fórmula(I,F) :-

valor(F,I,V),
V = 1.

15 / 34

PD Tema 14: Formalización en Prolog de la lógica proposicional

Semántica de la lógica proposicional

Satisfacibilidad

Cálculo de los modelos principales de una fórmula

modelo_fórmula(?I,+F) se verifica si I es un modelo principal

de la fórmula F. Por ejemplo,
?- modelo_fórmula(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

modelo_fórmula(I,F) :-

interpretación_fórmula(I,F),
es_modelo_fórmula(I,F).

16 / 34

PD Tema 14: Formalización en Prolog de la lógica proposicional

Semántica de la lógica proposicional

Satisfacibilidad

Cálculo de los modelos principales de una fórmula

modelos_fórmula(+F,-L) se verifica si L es el conjunto de los

modelos principales de la fórmula F. Por ejemplo,
?- modelos_fórmula((p v q) & (-q v r),L).
L = [[ (p, 0), (q, 1), (r, 1)],
(r, 0)],
(r, 1)],
(r, 1)]]

[ (p, 1),
[ (p, 1),
[ (p, 1),

(q, 0),
(q, 0),
(q, 1),

modelos_fórmula(F,L) :-

findall(I,modelo_fórmula(I,F),L).

17 / 34

PD Tema 14: Formalización en Prolog de la lógica proposicional

Semántica de la lógica proposicional

Satisfacibilidad

Comprobación de satisfacibilidad

es_satisfacible(+F) se verifica si la fórmula F es satisfacible.

Por ejemplo,
?- es_satisfacible((p v q) & (-q v r)).
Yes
?- es_satisfacible((p & q) & (p => r) & (q => -r)).
No

es_satisfacible(F) :-

interpretación_fórmula(I,F),
es_modelo_fórmula(I,F).

18 / 34

PD Tema 14: Formalización en Prolog de la lógica proposicional

Semántica de la lógica proposicional

Validez. Tautologías

Tema 14: Formalización en Prolog de la lógica
proposicional

1. Sintaxis de la lógica proposicional

2. Semántica de la lógica proposicional

Satisfacibilidad

Valores y funciones de verdad
Funciones de verdad
Valor de una fórmula en una interpretación
Interpretaciones de una fórmula
Modelo de una fórmula
Satisfacibilidad

Validez. Tautologías

Contramodelos de una fórmula
Validez. Tautologías

Consistencia de un conjunto de fórmulas

Interpretaciones principales de un conjunto de fórmulas
Modelo de un conjunto de fórmulas
Cálculo de modelos de conjuntos de fórmulas
Consistencia de un conj