Permalink
Browse files

Proofs for Allen Interval Algebra theorems

  • Loading branch information...
gruninger committed May 15, 2017
1 parent c89628a commit 2913f1f4036ded232601ce279abdf45d0715cf44
@@ -0,0 +1,64 @@
% Saved by Prover9-Mace4 Version 0.5B, March 2008 (Dec 2007 LADR).
set(ignore_option_dependencies). % GUI handles dependencies
if(Prover9). % Options for Prover9
assign(max_seconds, 600).
end_if.
if(Mace4). % Options for Mace4
assign(max_seconds, 60).
end_if.
formulas(assumptions).
%original interval meeting axioms
(all i all j all k all m
((meets(i,k)
& meets(j,k)
& meets(i,m))
->
meets(j,m))).
(all i all j all k all l
((meets(i,j)
& meets(k,l))
->
(meets(i,l) | b(i,l) | b(k,j)))).
(all x all y
(pre(x,y)
<->
(meets(x,y) | b(x,y) | (x=y)))).
(all x all y
(b(x,y)
<->
(exists z
(meets(x,z)
& meets(z,y))))).
-(all x all y
(exists z
(pre(x,z)
& pre(y,z)))).
(all i
(exists j exists k
(meets(i,j)
& meets(k,i)))).
(all x all y all z all u
((meets(x,y)
& meets(x,z)
& meets(y,u)
& meets(z,u))
->
(y=z))).
end_of_list.
formulas(goals).
end_of_list.
@@ -0,0 +1,37 @@
============================== prooftrans ============================
Prover9 (32) version Dec-2007, Dec 2007.
Process 58220 was started by mudcat on Romuald.local,
Sat May 6 10:19:28 2017
The command was "/Applications/Prover9-Mace4-v05B.app/Contents/Resources/bin-mac-intel/prover9".
============================== end of head ===========================
============================== end of input ==========================
============================== PROOF =================================
% -------- Comments from original proof --------
% Proof 1 at 0.01 (+ 0.01) seconds.
% Length of proof is 17.
% Level of proof is 5.
% Maximum clause weight is 15.
% Given clauses 58.
2 (all i all j all k all l (meets(i,j) & meets(k,l) -> meets(i,l) | b(i,l) | b(k,j))) # label(non_clause). [assumption].
3 (all x all y (pre(x,y) <-> meets(x,y) | b(x,y) | x = y)) # label(non_clause). [assumption].
5 -(all x all y exists z (pre(x,z) & pre(y,z))) # label(non_clause). [assumption].
6 (all i exists j exists k (meets(i,j) & meets(k,i))) # label(non_clause). [assumption].
9 -meets(x,y) | -meets(z,u) | meets(x,u) | b(x,u) | b(z,y). [clausify(2)].
11 pre(x,y) | -meets(x,y). [clausify(3)].
12 pre(x,y) | -b(x,y). [clausify(3)].
17 -pre(c1,x) | -pre(c2,x). [clausify(5)].
18 meets(x,f2(x)). [clausify(6)].
29 pre(x,f2(x)). [resolve(18,a,11,b)].
31 -meets(x,y) | meets(z,y) | b(z,y) | b(x,f2(z)). [resolve(18,a,9,a)].
64 -pre(c1,f2(c2)). [resolve(29,a,17,b)].
65 -pre(c2,f2(c1)). [ur(17,a,29,a)].
94 -b(c1,f2(c2)). [ur(12,a,64,a)].
95 -meets(c1,f2(c2)). [ur(11,a,64,a)].
97 -b(c2,f2(c1)). [ur(12,a,65,a)].
278 $F. [ur(31,b,95,a,c,94,a,d,97,a),unit_del(a,18)].
============================== end of proof ==========================
@@ -0,0 +1,56 @@
% Saved by Prover9-Mace4 Version 0.5B, March 2008 (Dec 2007 LADR).
set(ignore_option_dependencies). % GUI handles dependencies
if(Prover9). % Options for Prover9
assign(max_seconds, 600).
end_if.
if(Mace4). % Options for Mace4
assign(max_seconds, 60).
end_if.
formulas(assumptions).
%original interval meeting axioms
(all i all j all k all m
((meets(i,k)
& meets(j,k)
& meets(i,m))
->
meets(j,m))).
(all i all j all k all l
((meets(i,j)
& meets(k,l))
->
(meets(i,l) | b(i,l) | b(k,j)))).
(all x all y
(pre(x,y)
<->
(meets(x,y) | b(x,y) | (x=y)))).
(all x all y
(b(x,y)
<->
(exists z
(meets(x,z)
& meets(z,y))))).
-(all x all y
(exists z
(pre(z,x)
& pre(z,y)))).
(all i
(exists j exists k
(meets(i,j)
& meets(k,i)))).
end_of_list.
formulas(goals).
end_of_list.
@@ -0,0 +1,36 @@
============================== prooftrans ============================
Prover9 (32) version Dec-2007, Dec 2007.
Process 50903 was started by mudcat on mie-16-228.internal.mie.utoronto.ca,
Mon May 15 14:30:35 2017
The command was "/Applications/Prover9-Mace4-v05B.app/Contents/Resources/bin-mac-intel/prover9".
============================== end of head ===========================
============================== end of input ==========================
============================== PROOF =================================
% -------- Comments from original proof --------
% Proof 1 at 0.01 (+ 0.01) seconds.
% Length of proof is 16.
% Level of proof is 5.
% Maximum clause weight is 15.
% Given clauses 53.
2 (all i all j all k all l (meets(i,j) & meets(k,l) -> meets(i,l) | b(i,l) | b(k,j))) # label(non_clause). [assumption].
3 (all x all y (pre(x,y) <-> meets(x,y) | b(x,y) | x = y)) # label(non_clause). [assumption].
5 -(all x all y exists z (pre(z,x) & pre(z,y))) # label(non_clause). [assumption].
6 (all i exists j exists k (meets(i,j) & meets(k,i))) # label(non_clause). [assumption].
8 -meets(x,y) | -meets(z,u) | meets(x,u) | b(x,u) | b(z,y). [clausify(2)].
10 pre(x,y) | -meets(x,y). [clausify(3)].
11 pre(x,y) | -b(x,y). [clausify(3)].
16 -pre(x,c1) | -pre(x,c2). [clausify(5)].
18 meets(f3(x),x). [clausify(6)].
31 pre(f3(x),x). [resolve(18,a,10,b)].
46 -pre(f3(c2),c1). [resolve(31,a,16,b)].
47 -pre(f3(c1),c2). [ur(16,a,31,a)].
74 -b(f3(c2),c1). [ur(11,a,46,a)].
75 -meets(f3(c2),c1). [ur(10,a,46,a)].
77 -b(f3(c1),c2). [ur(11,a,47,a)].
241 $F. [ur(8,b,18,a,c,75,a,d,74,a,e,77,a),unit_del(a,18)].
============================== end of proof ==========================
@@ -0,0 +1,49 @@
formulas(assumptions).
-(all i all j all k all m
((meets(i,k)
& meets(j,k)
& meets(i,m))
->
meets(j,m))).
(all i all j all k
((meets(i,j)
& meets(j,k))
->
-meets(i,k))).
(all i all j all k all l
((meets(i,j)
& meets(k,l))
->
(meets(i,l)
| (exists n
((meets(i,n) & meets(n,l))
| (meets(k,n) & meets(n,j))))))).
(all i all j
(meets(i,j)
->
-meets(j,i))).
(all i all j all k all m
((meets(i,j)
& meets(j,k)
& meets(k,m))
->
(exists n
(meets(i,n)
& meets(n,m))))).
%unique_interval
(all x all y all z all u
((meets(x,y)
& meets(x,z)
& meets(y,u)
& meets(z,u))
->
(y=z))).
end_of_list.
@@ -0,0 +1,66 @@
============================== prooftrans ============================
Prover9 (32) version Dec-2007, Dec 2007.
Process 58801 was started by mudcat on Romuald.local,
Sun May 7 11:26:31 2017
The command was "/Applications/Prover9-Mace4-v05B.app/Contents/Resources/bin-mac-intel/prover9".
============================== end of head ===========================
============================== end of input ==========================
============================== PROOF =================================
% -------- Comments from original proof --------
% Proof 1 at 1.63 (+ 0.03) seconds.
% Length of proof is 46.
% Level of proof is 14.
% Maximum clause weight is 41.
% Given clauses 606.
1 -(all i all j all k all m (meets(i,k) & meets(j,k) & meets(i,m) -> meets(j,m))) # label(non_clause). [assumption].
2 (all i all j all k (meets(i,j) & meets(j,k) -> -meets(i,k))) # label(non_clause). [assumption].
3 (all i all j all k all l (meets(i,j) & meets(k,l) -> meets(i,l) | (exists n (meets(i,n) & meets(n,l) | meets(k,n) & meets(n,j))))) # label(non_clause). [assumption].
5 (all i all j all k all m (meets(i,j) & meets(j,k) & meets(k,m) -> (exists n (meets(i,n) & meets(n,m))))) # label(non_clause). [assumption].
7 meets(c1,c3). [clausify(1)].
8 meets(c2,c3). [clausify(1)].
9 meets(c1,c4). [clausify(1)].
10 -meets(c2,c4). [clausify(1)].
11 -meets(x,y) | -meets(y,z) | -meets(x,z). [clausify(2)].
12 -meets(x,y) | -meets(z,u) | meets(x,u) | meets(x,f1(x,y,z,u)) | meets(z,f1(x,y,z,u)). [clausify(3)].
13 -meets(x,y) | -meets(z,u) | meets(x,u) | meets(x,f1(x,y,z,u)) | meets(f1(x,y,z,u),y). [clausify(3)].
14 -meets(x,y) | -meets(z,u) | meets(x,u) | meets(f1(x,y,z,u),u) | meets(z,f1(x,y,z,u)). [clausify(3)].
15 -meets(x,y) | -meets(z,u) | meets(x,u) | meets(f1(x,y,z,u),u) | meets(f1(x,y,z,u),y). [clausify(3)].
17 -meets(x,y) | -meets(y,z) | -meets(z,u) | meets(x,f2(x,y,z,u)). [clausify(5)].
18 -meets(x,y) | -meets(y,z) | -meets(z,u) | meets(f2(x,y,z,u),u). [clausify(5)].
27 -meets(c1,x) | -meets(x,c4). [resolve(11,c,9,a)].
28 -meets(c2,x) | -meets(x,c3). [resolve(11,c,8,a)].
29 -meets(c1,x) | -meets(x,c3). [resolve(11,c,7,a)].
35 -meets(x,y) | meets(c2,y) | meets(c2,f1(c2,c3,x,y)) | meets(x,f1(c2,c3,x,y)). [resolve(12,a,8,a)].
36 -meets(x,y) | meets(c1,y) | meets(c1,f1(c1,c3,x,y)) | meets(x,f1(c1,c3,x,y)). [resolve(12,a,7,a)].
42 -meets(x,y) | meets(c1,y) | meets(c1,f1(c1,c3,x,y)) | meets(f1(c1,c3,x,y),c3). [resolve(13,a,7,a)].
47 -meets(x,y) | meets(c2,y) | meets(f1(c2,c3,x,y),y) | meets(x,f1(c2,c3,x,y)). [resolve(14,a,8,a)].
53 -meets(x,y) | meets(c2,y) | meets(f1(c2,c3,x,y),y) | meets(f1(c2,c3,x,y),c3). [resolve(15,a,8,a)].
54 -meets(x,y) | meets(c1,y) | meets(f1(c1,c3,x,y),y) | meets(f1(c1,c3,x,y),c3). [resolve(15,a,7,a)].
89 meets(c2,f1(c2,c3,c1,c4)) | meets(c1,f1(c2,c3,c1,c4)). [resolve(35,a,9,a),unit_del(a,10)].
100 meets(c1,f1(c2,c3,c1,c4)) | meets(c1,f1(c1,c3,c2,f1(c2,c3,c1,c4))) | meets(c2,f1(c1,c3,c2,f1(c2,c3,c1,c4))). [resolve(89,a,36,a),merge(b)].
162 meets(c1,f1(c2,c3,c1,c4)) | meets(c1,f1(c1,c3,c2,f1(c2,c3,c1,c4))) | meets(f1(c1,c3,c2,f1(c2,c3,c1,c4)),c3). [resolve(42,a,89,a),merge(d)].
166 meets(f1(c2,c3,c1,c4),c4) | meets(c1,f1(c2,c3,c1,c4)). [resolve(47,a,9,a),unit_del(a,10)].
182 meets(c1,f1(c2,c3,c1,c4)) | -meets(x,y) | -meets(y,f1(c2,c3,c1,c4)) | meets(f2(x,y,f1(c2,c3,c1,c4),c4),c4). [resolve(166,a,18,c)].
185 meets(c1,f1(c2,c3,c1,c4)) | -meets(x,y) | -meets(y,f1(c2,c3,c1,c4)) | meets(x,f2(x,y,f1(c2,c3,c1,c4),c4)). [resolve(166,a,17,c)].
207 meets(f1(c2,c3,c1,c4),c4) | meets(f1(c2,c3,c1,c4),c3). [resolve(53,a,9,a),unit_del(a,10)].
227 meets(f1(c2,c3,c1,c4),c3) | -meets(c1,f1(c2,c3,c1,c4)). [resolve(207,a,27,b)].
253 meets(c1,f1(c2,c3,c1,c4)) | meets(f1(c1,c3,c2,f1(c2,c3,c1,c4)),f1(c2,c3,c1,c4)) | meets(f1(c1,c3,c2,f1(c2,c3,c1,c4)),c3). [resolve(54,a,89,a),merge(d)].
334 meets(c1,f1(c2,c3,c1,c4)) | meets(c1,f1(c1,c3,c2,f1(c2,c3,c1,c4))) | -meets(f1(c1,c3,c2,f1(c2,c3,c1,c4)),c3). [resolve(100,c,28,a)].
1038 meets(c1,f1(c2,c3,c1,c4)) | meets(c1,f1(c1,c3,c2,f1(c2,c3,c1,c4))). [resolve(334,c,162,c),merge(c),merge(d)].
1041 meets(c1,f1(c2,c3,c1,c4)) | -meets(f1(c1,c3,c2,f1(c2,c3,c1,c4)),f1(c2,c3,c1,c4)) | meets(c1,f2(c1,f1(c1,c3,c2,f1(c2,c3,c1,c4)),f1(c2,c3,c1,c4),c4)). [resolve(1038,b,185,b),merge(b)].
1042 meets(c1,f1(c2,c3,c1,c4)) | -meets(f1(c1,c3,c2,f1(c2,c3,c1,c4)),f1(c2,c3,c1,c4)) | meets(f2(c1,f1(c1,c3,c2,f1(c2,c3,c1,c4)),f1(c2,c3,c1,c4),c4),c4). [resolve(1038,b,182,b),merge(b)].
1086 meets(c1,f1(c2,c3,c1,c4)) | -meets(f1(c1,c3,c2,f1(c2,c3,c1,c4)),x) | -meets(c1,x). [resolve(1038,b,11,a)].
4365 meets(c1,f1(c2,c3,c1,c4)) | meets(c1,f2(c1,f1(c1,c3,c2,f1(c2,c3,c1,c4)),f1(c2,c3,c1,c4),c4)) | meets(f1(c1,c3,c2,f1(c2,c3,c1,c4)),c3). [resolve(1041,b,253,b),merge(c)].
4367 meets(c1,f1(c2,c3,c1,c4)) | meets(c1,f2(c1,f1(c1,c3,c2,f1(c2,c3,c1,c4)),f1(c2,c3,c1,c4),c4)). [resolve(4365,c,1086,b),merge(c),unit_del(c,7)].
4435 meets(c1,f1(c2,c3,c1,c4)) | -meets(f2(c1,f1(c1,c3,c2,f1(c2,c3,c1,c4)),f1(c2,c3,c1,c4),c4),x) | -meets(c1,x). [resolve(4367,b,11,a)].
4660 meets(c1,f1(c2,c3,c1,c4)) | meets(f2(c1,f1(c1,c3,c2,f1(c2,c3,c1,c4)),f1(c2,c3,c1,c4),c4),c4) | meets(f1(c1,c3,c2,f1(c2,c3,c1,c4)),c3). [resolve(1042,b,253,b),merge(c)].
4662 meets(c1,f1(c2,c3,c1,c4)) | meets(f1(c1,c3,c2,f1(c2,c3,c1,c4)),c3). [resolve(4660,b,4435,b),merge(c),unit_del(c,9)].
4663 meets(c1,f1(c2,c3,c1,c4)). [resolve(4662,b,1086,b),merge(b),unit_del(b,7)].
4664 meets(f1(c2,c3,c1,c4),c3). [back_unit_del(227),unit_del(b,4663)].
4674 $F. [resolve(4663,a,29,a),unit_del(a,4664)].
============================== end of proof ==========================
@@ -0,0 +1,39 @@
formulas(assumptions).
(all i all j all k all m
((meets(i,k)
& meets(j,k)
& meets(i,m))
->
meets(j,m))).
-(all i all j all k
((meets(i,j)
& meets(j,k))
->
-meets(i,k))).
(all i all j all k all l
((meets(i,j)
& meets(k,l))
->
(meets(i,l)
| (exists n
((meets(i,n) & meets(n,l))
| (meets(k,n) & meets(n,j))))))).
(all i all j
(meets(i,j)
->
-meets(j,i))).
(all i all j all k all m
((meets(i,j)
& meets(j,k)
& meets(k,m))
->
(exists n
(meets(i,n)
& meets(n,m))))).
end_of_list.
@@ -0,0 +1,30 @@
============================== prooftrans ============================
Prover9 (32) version Dec-2007, Dec 2007.
Process 58810 was started by mudcat on Romuald.local,
Sun May 7 11:27:24 2017
The command was "/Applications/Prover9-Mace4-v05B.app/Contents/Resources/bin-mac-intel/prover9".
============================== end of head ===========================
============================== end of input ==========================
============================== PROOF =================================
% -------- Comments from original proof --------
% Proof 1 at 0.00 (+ 0.01) seconds.
% Length of proof is 10.
% Level of proof is 3.
% Maximum clause weight is 12.
% Given clauses 12.
1 (all i all j all k all m (meets(i,k) & meets(j,k) & meets(i,m) -> meets(j,m))) # label(non_clause). [assumption].
2 -(all i all j all k (meets(i,j) & meets(j,k) -> -meets(i,k))) # label(non_clause). [assumption].
4 (all i all j (meets(i,j) -> -meets(j,i))) # label(non_clause). [assumption].
6 -meets(x,y) | -meets(z,y) | -meets(x,u) | meets(z,u). [clausify(1)].
7 meets(c1,c2). [clausify(2)].
8 meets(c2,c3). [clausify(2)].
9 meets(c1,c3). [clausify(2)].
14 -meets(x,y) | -meets(y,x). [clausify(4)].
17 -meets(x,x). [factor(14,a,b)].
72 $F. [ur(6,b,8,a,c,7,a,d,17,a),unit_del(a,9)].
============================== end of proof ==========================
Oops, something went wrong.

0 comments on commit 2913f1f

Please sign in to comment.