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
|
<HTML>
<HEAD>
<TITLE>CASC-JC Entrants' Sample Solutions</TITLE>
</HEAD>
<BODY>
<HR><!------------------------------------------------------------------------>
<A NAME="E---0.62">
<HR><!------------------------------------------------------------------------>
<H2>EP 0.8</H2>
S. Schulz<BR>
Institut für Informatik, Technische Universität München,
Germany, and RISC-Linz, Johannes Kepler Universität Linz,
Austria<BR>
schulz@informatik.tu-muenchen.de
<P>
Here is a list of all inferences:
<DL>
<DT> er
<DD> Equality resolution: x!=a v x=x ==> a=a
<DT> pm
<DD> Paramodulation. Note that E considers all literals as equational,
and thus also performs resolution by a combination of top-level
paramodulation and clause normalization.
<DT> ef
<DD> Equality factoring (factor equations on one side only, move the
remaining disequation into the precondition): x=a v b=c v x=d ==>
a!=c v b=c vb=d
<DT> split
<DD> Clause splitting a la Vampire (non-deductive, but maintains
unsatisfiability)
<DT> rw
<DD> Rewriting, each rw-expression corresponds to exacly one rewrite
step with the named clause. This is also used for equational
unfolding.
<DT> sr
<DD> Simplify-reflect: An (equational) version of unit-cutting. As as
example, see this positive simplify-reflect step:
[a=b], [f(a)!=f(b)] => [].
<DT> ar
<DD> AC-resolution: Delete literals that are trivial modulo the
AC-theory induced by the named clauses
<DT> cn
<DD> Clause normalize, delete trivial and repeated literals
</DL>
<P>
The first proof uses all but "ef", although it uses some in fairly
trivial ways. Note that clause normalization is inherently performed
after all inferences but rewriting. The second is the required proof
for SYN075-1, and contains an example for "ef".
<p>
<strong>ALL_RULES</strong>
<PRE>
# Problem is unsatisfiable, constructing proof object
# TSTP exit status: Unsatisfiable
# Proof object starts here.
1 : [++equal(f(X1,X2), f(X2,X1))] : initial
2 : [++equal(f(X1,f(X2,X3)), f(f(X1,X2),X3))] : initial
3 : [++equal(g(X1,X2), g(X2,X1))] : initial
4 : [--equal(f(f(X1,X2),f(X3,g(X4,X5))), f(f(g(X4,X5),X3),f(X2,X1))),--equal(k(X1,X1), k(a,b))] : initial
5 : [++equal(b, c),--equal(X1, X2),--equal(X3, X4),--equal(c, d)] : initial
6 : [++equal(a, b),++equal(a, c)] : initial
7 : [++equal(i(X1), i(X2))] : initial
8 : [++equal(c, d),--equal(h(i(a)), h(i(e)))] : initial
13 : [--equal(k(a,b), k(X1,X1))] : ar(4,1,3,2)
23 : [++equal(c, b),++epred1_0,--equal(d, c),--equal(X3, X4)] : split(5)
24 : [++epred2_0,--equal(X1, X2)] : split(5)
25 : [--epred2_0,--epred1_0] : split(5)
26 : [++epred2_0] : er(24)
27 : [--$true,--epred1_0] : rw(25,26)
28 : [++equal(c, b),++epred1_0,--equal(d, c)] : er(23)
29 : [++equal(c, b),--equal(d, c)] : sr(28,27)
30 : [++equal(d, c)] : sr(8,7)
31 : [++equal(c, b),--equal(c, c)] : rw(29,30)
32 : [++equal(c, b)] : cn(31)
34 : [++equal(b, a)] : pm(6,32)
35 : [--equal(k(b,b), k(X1,X1))] : rw(13,34)
120 : [] : er(35)
121 : [] : 120 : "proof"
# Proof object ends here.
</pre>
<p>
<strong>SYN075-1</strong>
<PRE>
# Problem is unsatisfiable, constructing proof object
# TSTP exit status: Unsatisfiable
# Proof object starts here.
1 : [++equal(X1, a),--big_f(X1,X2)] : initial
3 : [++big_f(X1,X2),--equal(X1, a),--equal(X2, b)] : initial
4 : [++equal(f(X2), X2),--big_f(X1,f(X2)),--equal(X1, g(X2))] : initial
6 : [++big_f(X1,f(X2)),++equal(f(X2), X2),--equal(X1, g(X2))] : initial
9 : [++big_f(h(X1,X2),f(X1)),++equal(h(X1,X2), X2),--equal(f(X1), X1)] : initial
10 : [--equal(f(X1), X1),--equal(h(X1,X2), X2),--big_f(h(X1,X2),f(X1))] : initial
18 : [++equal(f(X2), X2),--equal(g(X2), X1)] : pm(4,6)
19 : [++equal(f(X1), X1)] : er(18)
24 : [--equal(X1, X1),--equal(h(X1,X2), X2),--big_f(h(X1,X2),f(X1))] : rw(10,19)
25 : [--equal(X1, X1),--equal(h(X1,X2), X2),--big_f(h(X1,X2),X1)] : rw(24,19)
26 : [--equal(h(X1,X2), X2),--big_f(h(X1,X2),X1)] : cn(25)
27 : [++equal(h(X1,X2), X2),++big_f(h(X1,X2),X1),--equal(f(X1), X1)] : rw(9,19)
28 : [++equal(h(X1,X2), X2),++big_f(h(X1,X2),X1),--equal(X1, X1)] : rw(27,19)
29 : [++equal(h(X1,X2), X2),++big_f(h(X1,X2),X1)] : cn(28)
30 : [++equal(a, h(X1,X2)),++equal(h(X1,X2), X2)] : pm(1,29)
36 : [++equal(h(X1,X2), X2),--equal(a, X2)] : ef(30)
46 : [--big_f(X2,X1),--equal(h(X1,X2), X2),--equal(a, X2)] : pm(26,36)
56 : [--big_f(X2,X1),--equal(a, X2)] : pm(46,36)
63 : [--equal(a, X1),--equal(b, X2)] : pm(56,3)
94 : [--equal(b, X1)] : er(63)
103 : [] : er(94)
104 : [] : 103 : "proof"
# Proof object ends here.
</pre>
<HR><!------------------------------------------------------------------------>
</BODY>
</HTML>
|
