PDF de programación - Razonamiento automático en lógica de primer orden

Razonamiento automático en lógica de primer orden

Juan J. Arrabal, José A. Alonso, Delia Balbontín y Javier Herrera
Departamento de Álgebra, Computación, Geometría y Topología

Facultad de Matemáticas

Universidad de Sevilla

12 de Julio de 1992

1 Introducción

El objetivo del presente trabajo consiste en una
demostración de las posibilidades del programa
OTTER [McCune 90] para la demostración au-
tomática de teoremas de Lógica de primer or-
den. Para dicha demostración hemos elegi-
do como campo de experimentación los ejer-
cicios propuestos por Jesús Mosterín en su
libro “Lógica de primer orden”. En la re-
solución de los ejercicios nos encontraremos
con los problemas centrales del razonamiento
automático: representación del conocimiento,
elección de reglas de inferencia y utilización
de estrategias de prueba. Como es corriente
en la experimentación en razonamiento au-
tomático, a lo largo del experimento apare-
cen nuevos problemas; en nuestro experimento
nos hemos encontrado con el problema del
tratamiento de los descriptores (ejercicios 25–
35) para los cuales hemos introducidos nuevos
axiomas, pero queda pendiente un estudio más
detallado que posiblemente demuestre la con-
veniencia de introducir una nueva regla de in-
ferencia.

2 Ejercicios

En esta sección presentamos las soluciones a
algunos de los ejercicios de [Mosterín 70] (pp.
58–87) usando la misma numeración del libro.
La selección se ha hecho considerando los ejer-
cicios que implican la introducción de nuevas
reglas de inferencia o estrategias de búsquedas.

Ejercicio 1.
∀x(P → P )

Para resolverlo, elegimos como regla de in-

ferencia la resolución binaria y ponemos en el
conjunto soporte la negación de la fórmula a
probar. El fichero de entrada para el Ejercicio
1 es

set(binary_res).
formula_list(sos).
- (all x (P -> P)).
end_of_list.

El programa OTTER transforma la fórmula
a cláusulas y realiza la demostración, dando
como fichero de salida

-------> sos clausifies to:
1 [] P.
2 [] -P.
-------- PROOF --------
1 [] P.
2 [] -P.
3 [binary,2,1] $F.

En el proceso de clausificación se obtienen las
cláusulas P y -P (la negación de P) que inmedi-
atamente generan la contradicción ($F).



Ejercicio 2.
xy(Rxy ∨ Ryx) ∀xRxx
Para este

suficiente

ejercicio no es

la
regla de resolución binaria. Lo resolveremos
añadiéndole la regla de factorización. Además,
colocamos en el conjunto soporte la hipótesis
y la negación de la conclusión. El fichero de
entrada es

set(binary_res).
set(factor).
formula_list(sos).
all x y (R(x,y) | R(y,x)).
- (all x R(x,x)).

1

end_of_list.

y el de salida es

-------> sos clausifies to:
1 [] R(x,y)|R(y,x).
2 [] -R($c1,$c1).
-------- PROOF --------
1 [] R(x,y)|R(y,x).
2 [] -R($c1,$c1).
3 [binary,1,2] R($c1,$c1).
4 [binary,3,2] $F.

La clausificación de la hipótesis genera la cláu-
sula 1 (donde | es el símbolo de disyunción).
La negación de la conclusión indica que existe
un elemento x que no verifica la fórmula Rxx;
en el proceso de clausificación, se introduce la
constante de Skolem $c1 para representar un
elemento verificando la negación de Rxx.

Para el Ejercicio 3 basta resolución binaria.
Ejercicio 4.



y(F y →

xF x)

El fichero de entrada es

set(binary_res).
formula_list(sos).
- (exists y (F(y) -> (all x F(x)))).
end_of_list.

y el de salida es

-------> sos clausifies to:
1 [] F(y).
2 [] -F($f1(y)).
-------- PROOF --------
1 [] F(y).
2 [] -F($f1(y)).
3 [binary,2,1] $F.

La negación de la fórmula a demostrar dice que
para cada elemento y que verifica la fórmula F y
existe un elemento (que depende de y) que no
la verifica; dicho elemento está representado en
la cláusula 2 por la función de Skolem $f1(y).
Los ejercicios 5, 6 y 7 requieren resolución
binaria. Además, en el 6 se necesita factor-
ización.

{





Ejercicio 8.
(Rxu ∧ Ryu) → Rxy),
xy(
yRxy}
x
xyz(Rxy ∧ Ryz → Rxz

Para resolver el ejercicio con resolución bi-
naria, se necesitan 36 pasos de resolución. Una
forma de obtener una demostración más corta
consiste en utilizar como regla de inferencia la
hiper–resolución. El fichero de entrada es

set(hyper_res).
formula_list(sos).
all x y ((exists u (R(x,u) & R(y,u)))

-> R(x,y)).

all x exists y R(x,y).
- (all x y z (R(x,y) & R(y,z) ->

R(x,z))).

end_of_list.

y el fichero de salida es

-------> sos clausifies to:
1 [] -R(x,u)| -R(y,u)|R(x,y).
2 [] R(x,$f1(x)).
3 [] R($c3,$c2).
4 [] R($c2,$c1).
5 [] -R($c3,$c1).
-------- PROOF --------
1 [] -R(x,u)| -R(y,u)|R(x,y).
2 [] R(x,$f1(x)).
3 [] R($c3,$c2).
4 [] R($c2,$c1).
5 [] -R($c3,$c1).
8 [hyper,1,2,2] R(x,x).
9 [hyper,8,1,4] R($c1,$c2).
12 [hyper,9,1,3] R($c3,$c1).
13 [binary,12,5] $F.

El Ejercicio 9 se resuelve con resolución bi-
naria; el 10, con hiper–resolución; el 11, con
hiper–resolución y factorización.

Ejercicio 12.
x((Bx ∨ N x) ∧ ¬(Bx ∧ N x)),
x(f x = a → Bx),

{

¬
f a = a}

xN x

Aunque en este ejercicio interviene el pred-
icado de igualdad, puede resolverse con res-
olución binaria. El fichero de entrada es

set(binary_res).
formula_list(sos).
all x ((B(x) | N(x)) & - (B(x) &

N(x))).

all x (f(x) = a -> B(x)).

2

f(a) = a.
all x N(x).
end_of_list.

y el de salida es

-------> sos clausifies to:
1 [] B(x)|N(x).
2 [] -B(x)| -N(x).
3 [] f(x)!=a|B(x).
4 [] f(a)=a.
5 [] N(x).
-------- PROOF --------
2 [] -B(x)| -N(x).
3 [] f(x)!=a|B(x).
4 [] f(a)=a.
5 [] N(x).
6 [binary,2,5] -B(x).
7 [binary,3,4] B(a).
8 [binary,7,6] $F.

En la cláusula 3 aparece el símbolo != que

Ejercicio 13.

representa =.
{−


x − Hx → −


xHx

x(

y(y = a → P y) → Hx),
x(P a ∧ −Hx)}

Para resolverlo basta la resolución binaria
como regla de inferencia, pero se necesita in-
troducir el axioma reflexivo (x = x). Dicho
axioma se usa en los restantes ejercicios salvo
14, 15, 16 y 34. El fichero de entrada es

set(binary_res).
list(usable).
x = x.
end_of_list.
formula_list(sos).
- (exists x ((all y (y = a -> P(y)))

-> H(x))).

(exists x (- H(x))) -> - (all x (P(a)

& - H(x))).

- (all x H(x)).
end_of_list.

El fichero de salida es

1 [] x=x.
-------> sos clausifies to:
2 [] y!=a|P(y).
3 [] -H(x).

4 [] H(x)| -P(a)|H($c1).
5 [] -H($c2).
-------- PROOF --------
1 [] x=x.
2 [] y!=a|P(y).
3 [] -H(x).
4 [] H(x)| -P(a)|H($c1).
5 [] -H($c2).
6 [binary,2,1] P(a).
7 [binary,4,6] H(x)|H($c1).
9 [binary,7,3] H(x).
10 [binary,9,5] $F.

El Ejercicio 14 se resuelve con hiper–

xRxx,

xf cx = c,

resolución.

Ejercicio 15.

{a = hf cc ∨

¬a = hc}
¬Rcc → Rcc
En este ejercicio es conveniente usar como
El

regla de inferencia la paramodulación.
fichero de entrada es

set(binary_res).
set(para_from).
formula_list(sos).
a=h(f(c,c)) | (all x R(x,x)).
all x (f(c,x)=c).
a!=h(c).
-(-R(c,c) -> R(c,c)).
end_of_list.

y el de salida es

-------> sos clausifies to:
1 [] a=h(f(c,c))|R(x,x).
2 [] f(c,x)=c.
3 [] a!=h(c).
4 [] -R(c,c).
5 [] -R(c,c).
-------- PROOF --------
1 [] a=h(f(c,c))|R(x,x).
2 [] f(c,x)=c.
3 [] a!=h(c).
5 [] -R(c,c).
10 [para_from,2,3] a!=h(f(c,x)).
28 [binary,1,10] R(x,x).
29 [binary,28,5] $F.

Ejercicio 16.

¬(¬f a = f b ∨ ¬Hf a) → Hf b

3

Este ejercicio puede resolverse con resolución
binaria, añadiendo el axioma de sustitución
correspondiente a H. El fichero de entrada es

set(binary_res).
formula_list(usable).
all x y (x = y -> (H(x) -> H(y))).
end_of_list.
formula_list(sos).
-( - (f(a) != f(b) | - H(f(a))) ->

H(f(b))).

end_of_list.

y el de salida es

-------> usable clausifies to:
1 [] x!=y| -H(x)|H(y).
-------> sos clausifies to:
2 [] f(a)=f(b).
3 [] H(f(a)).
4 [] -H(f(b)).
-------- PROOF --------
1 [] x!=y| -H(x)|H(y).
2 [] f(a)=f(b).
3 [] H(f(a)).
4 [] -H(f(b)).
5 [binary,3,1] f(a)!=x|H(x).
8 [binary,5,2] H(f(b)).
9 [binary,8,4] $F.

El Ejercicio 17 se soluciona utilizando res-
olución binaria y paramodulación; el 18 y 19,
con resolución binaria.

{



z

Ejercicio 20.

x(f xz = x ∧

xyuw(f xu = y ∧ f xw = y → u = w,


z

yf xy = z}
xf xw = x ↔ w = z

w(

Para este ejercicio se necesita una nueva
regla de inferencia (la UR–resolución) y una
nueva estrategia (la demodulación dinámica).
Además, hemos añadido un axioma de susti-
tución para la función f y reducido el con-
junto soporte a la negación de la conclusión.
El fichero de entrada es

set(ur_res).
set(factor).
set(para_from).
set(dynamic_demod).
formula_list(usable).
all x (x=x).

all x y u w (f(x,u)=y & f(x,w)=y ->

u=w).

exists z all x (f(x,z)=x & (exists y

(f(x,y)=z))).

end_of_list.
formula_list(sos).
- (exists z all w ((all x (f(x,w)=x))

<-> w=z)).

end_of_list.

y el de salida es

-------> usable clausifies to:
1 [] x=x.
2 [] f(x,u)!=y|f(x,w)!=y|u=w.
3 [] f(x,$c1)=x.
4 [] f(x,$f1(x))=$c1.
-------> sos clausifies to:
5 [] f(x,$f3(z))=x|$f3(z)=z.
6 [] f($f2(z),$f3(z))!=$f2(z)|

$f3(z)!=z.

-------- PROOF --------
1 [] x=x.
2 [] f(x,u)!=y|f(x,w)!=y|u=w.
3 [] f(x,$c1)=x.
5 [] f(x,$f3(z))=x|$f3(z)=z.
6 [] f($f2(z),$f3(z))!=$f2(z)|

$f3(z)!=z.

7 [para_from,5,2] f(x,y)!=z|x!=z|

$f3(u)=y|$f3(u)=u.

8 [factor,7] f(x,y)!=z|x!=z|$f3(y)=y.
16,15 [ur,8,3,1] $f3($c1)=$c1.
24 [ur,15,6,demod,16] f($f2($c1),$c1)

!=$f2($c1).

25 [binary,24,3] $F.

{




Ejercicio 21.

xyzf f xyz = f xf yz,
xf xhx = k,
xf kx = x}
xy

zf xz = y



Podemos interpretar las hipótesis del ejerci-
cio como axiomas de la teoría de grupos. Rep-
resentaremos el símbolo de función f por el op-
erador infijo + y el símbolo de función h por el
operador prefijo -. Además, reducimos el con-
junto soporte a la negación de la conclusión. El
fichero de entrada es

set(binary_res).
set(para_into).
op(500,xfy,+).

4

op(400,xf,’-’).
formula_list(usable).
all x (x=x).
all x y z ((x + y) + z=x + (y + z)).
all x (x + (- x) = e).
all x (e + x = x).