1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
|
Directproof.
This applies to Horn sets in which the only relation
is equality, and the denial is a unit.
It starts with a Prover9 proof. If there are nonunit
clauses in the proof, they must be used with hyperresolution
or positive resolution (e.g, no UR or paramodulation).
Def: a proof is bidirectional if a negative clause is used
for something (including flipping) other than unit conflict.
Algorithm:
While the proof is bidirectional:
eliminate the last backward step.
Note that if a proof is bidirectional, there is a backward step
right at the end, so all of the transformations are at the end
of the proof (involve the empty clause).
Note that the transformations can introduce para into variables,
para from variables, "instantiate" inferences, and instances of x=x
as new assumptions.
Cases handled so far:
Case 1: Flip negative clause then apply unit conflict:
Case 1a: Unit conflict does an implicit flip.
1. a != b. [ ... ]
2. b != a. [1,flip]
3. a = b. [ ... ]
4. $F [resolve,2,3(flip)]
Transform this by simply removing lines 2 and 4, then applying
unit conflict to 1 and 3.
Case 1b: Unit conflict does not do implicit flip.
1. a != b. [ ... ]
2. b != a. [1,flip]
3. b = a. [ ... ]
4. $F [resolve,2,3]
Transform this in the obvious way by removing steps 2 and 4,
flipping 3, and then applying unit conflict with 1.
Case 2: Para into negative clause to get an instance of x != x.
Case 2a: Para into top of negative clause
1. a = b. [ ... ]
2. a != b. [ ... ]
5. b != b. [para,1,3]
6. $F [3,xx_res]
(1 and 2 give unit conflict, but the proof can be as shown.)
Transform this by simply doing a unit conflict between 1 and 2
If para goes from or into the wrong side, we might have to
flip the positive one first.
Case 2b: Para into proper subterm of neg clause.
1. a = b. [ ... ]
2. f(g(a)) != f(g(b)). [ ... ]
3. f(g(b)) != f(g(b)). [para,1(left),2]
4. $F [3,xx_res]
Transformation: We have to derive f(g(a)) = f(g(b)) from a=b.
First assume f(g(x)) = f(g(x)), then para the *opposite* side
of a=b into the position in f(g(x)) = f(g(x)) that corresponds
to the into position of 2 (that is, the first occurrence of x).
Result:
1. a = b. [ ... ]
2. f(g(a)) != f(g(b)). [ ... ]
5. f(g(x)) = f(g(x)). [assumption]
6. f(g(a)) = f(g(b)). [para,1(right),5]
7. $F [resolve,2,6]
(Instead we could have an inference rule that takes a=b and
derives g(a) = g(b), and then apply it again to get f(g(a))=f(g(b)).
I have two objections to this: first, the IVY proof checker
cannot handle inferences like that; second, you have to build
up the equality you need one step at a time.)
Case 3: Para into a neg clause, then unit conflict with some positive clause.
Note: unit conflict can involve implicit flip. In that case, flip
the positive equality participating in the unit conflict (clause 3 below)
before doing anything else.
1. a = b1. [ ... ]
2. f[a] != c. [ ... ]
3. f[b2] = c. [ ... ]
4. f[b1] != c. [para,1(left),2]
5. $F [resolve,3,4] (b1 and b2 unify)
Case 3a: In clause 3, term b2 exists.
Transformation: Para *opposite* side of 1 into position in 3 (b2)
corresponding to the into position of 2. Then unit conflict with 2.
Result:
1. a = b1. [ ... ]
2. f[a] != c. [ ... ]
3. f[b2] = c. [ ... ]
6. f[a] = c. [para,1(right),3]
7. $F [resolve 2,6]
Case 3b: In clause 3, term at position b2 does not exist.
Transformation: Instantiate clause 3 (minimally) so that the
position exists, then proceed as in case 3a.
An example of case 3b:
Bidirectional:
1 a = b. [assumption].
2 f(c,g(h(g(a),d))) != g(h(g(b),d)). [assumption].
3 f(c,x) = x. [assumption].
4 f(c,g(h(g(b),d))) != g(h(g(b),d)). [para(1(a,1),2(a,1,2,1,1,1))].
5 $F. [resolve(3,a,4,a)].
Transformed:
1 a = b. [assumption].
2 f(c,g(h(g(a),d))) != g(h(g(b),d)). [assumption].
3 f(c,x) = x. [assumption].
6 f(c,g(h(g(y),z))) = g(h(g(y),z)). [instantiate(3,[[x:g(h(g(y),z))]])].
7 f(c,g(h(g(a),x))) = g(h(g(b),x)). [para(1(a,2),6(a,1,2,1,1,1))].
8 $F. [resolve(7,a,2,a)].
|
