Quote from AntC on January 11, 2020, 6:20 am

As the only person round here likely to understand Prover9 format, I suppose I'd better chirp up. I've never before seen formulas trying to express domains, so the best I can do is act the cardboard programmer.

This comment (lower down) "In the formulas part I'm trying to assert that P1 and P2 are the domains of the relation y, while P2 and P3 are domains of the relation x." seems inconsistent with the ' formulas(assumptions)'  disjunction <-> P2(p2). One of the disjuncts uses x(p2,s), the other y(r,p2). So that seems to assert P2 is in the domain of both x (its first domain) and y (its second domain).

Edit: ahh, my mistake (I'll leave this here for ref). You put y first in your narrative, but second in the code. I read them the wrong way round.

Quote from Vadim on January 11, 2020, 3:17 am

I'm trying to prove the following relational lattice identity:

(y` ^ x') v (y' ^ x `) = (y' v x') ^ (y` v x `).

Assuming that x and y are two binary relations, and introducing the three unary domain relations P1, P2, P3, I have translated it into the Prover9 dialect of the predicate calculus syntax the following way:

formulas(assumptions).

( exists p x(p,q)) <-> P3(q).
( exists s x(p2,s)
| exists r y(r,p2) ) <-> P2(p2).
( exists r y(q,r)) <-> P1(q).


end_of_list.

formulas(goals).

exists p1 exists p3 (
(P3(p3) & exists p1 exists p2 y(p1,p2))
& -x(p2,p3)
|
-y(p1,p2) &
(P1(p1) & exists p2 exists p3 x(p2,p3))
)
<->
exists p1 exists p3
(-x(p2,p3)
|
-y(p1,p2))
&
exists p1 exists p3 (
P3(p3) & (exists p1 exists p2 y(p1,p2))
| P1(p1) & (exists p2 exists p3 x(p2,p3))
)
.

In the formulas part I'm trying to assert that P1 and P2 are the domains of the relation y, while P2 and P3 are domains of the relation x. However, Mace4 exhibits the following counterexample:

P1(0).
- P1(1).
- P1(2).

P2(0).
- P2(1).
- P2(2).

- P3(0).
- P3(1).
- P3(2).

- x(0,0).
x(0,1).
- x(0,2).
- x(1,0).
- x(1,1).
- x(1,2).
- x(2,0).
- x(2,1).
- x(2,2).

y(0,0).
- y(0,1).
- y(0,2).
- y(1,0).
- y(1,1).
- y(1,2).
- y(2,0).
- y(2,1).
- y(2,2).

It insists on P3 being empty, but this is wrong because x is not empty (i.e. x(0,1)=true). Certainly, it would invalidate the first formula/assumption that P3 is domain of x?

Edit: have solved the domain emptiness puzzle with the following formulas/assumptions:

all q (P3(q) | all p -x(p,q)).
all q (P1(q) | all p -y(q,p)).
all q (P2(q) | all p (-y(p,q)&-x(q,p)) ).

Still, there seems to be a counterexample...

 

 

Quote from AntC on January 11, 2020, 10:18 am

This code looks odd, particularly the scoping of the exists-bound pn variables:

exists p1 exists p3 (
(P3(p3) & exists p1 exists p2 y(p1,p2))
& -x(p2,p3)                                                                       % this p2 is free in the whole formula
|
-y(p1,p2) &                                                                        % this p2 is the same free
(P1(p1) & exists p2 exists p3 x(p2,p3))
)
<->
exists p1 exists p3
(-x(p2,p3)                                                                          % p2 free
|
-y(p1,p2))                                                                           % p2 free
&
exists p1 exists p3 (
P3(p3) & (exists p1 exists p2 y(p1,p2))
| P1(p1) & (exists p2 exists p3 x(p2,p3))
)
.

So the formula has a p2 free (i.e. implicit (for)all), but some appearances of p2 are exists-bound. The free occurrences of p2 are negations in branches of disjunctions. The formula has p1, p3 exists-bound at outer scope, but some appearances of p1, p3 are exists-bound at narrow scope.

The negations, disjunctions, local bindings, exists are all things that make the formula difficult to read. It seems over-complicated for what you're aiming to do. (Also it'll give Prover9 inference severe indigestion, as Tadeusz points out.)

Quote from Vadim on January 11, 2020, 5:53 pm

Thank you Anthony. Forum ate my indentations:-) Simplified domain definition, and it is proven:

formulas(assumptions).

all q D(q).



formulas(goals).

%(y` ^ x') v (y' ^ x `) = (y' v x') ^ (y` v x `).
(
  exists p3 ( (D(p3) & exists s exists t y(s,t)) & -x(p2,p3) )
  |
  exists p1 ( (D(p1) & exists s exists t x(s,t)) & -y(p1,p2) )
) 
<-> 
( 
  ( 
    exists t2 -x(p2,t2) 
    | 
    exists s2 -y(s2,p2) 
  )
  &
  (
    exists u (D(u) & exists q exists r y(q,r))
    | 
    exists w (D(w) & exists q exists r x(q,r))
  )
).