1 |
|
|
2 |
|
|
3 |
|
|
4 |
|
|
5 |
|
|
6 |
|
|
7 |
|
|
8 |
|
|
9 |
|
|
10 |
|
|
11 |
|
|
12 |
|
|
13 |
|
|
14 |
|
|
15 |
|
package org.qedeq.kernel.bo.logic.proof.checker; |
16 |
|
|
17 |
|
import java.io.File; |
18 |
|
|
19 |
|
import org.qedeq.kernel.bo.KernelContext; |
20 |
|
import org.qedeq.kernel.bo.logic.common.LogicalCheckExceptionList; |
21 |
|
import org.qedeq.kernel.bo.logic.common.ReferenceResolver; |
22 |
|
import org.qedeq.kernel.bo.logic.proof.common.ProofChecker; |
23 |
|
import org.qedeq.kernel.bo.logic.proof.common.RuleChecker; |
24 |
|
import org.qedeq.kernel.bo.module.KernelNodeBo; |
25 |
|
import org.qedeq.kernel.bo.module.KernelQedeqBo; |
26 |
|
import org.qedeq.kernel.bo.test.QedeqBoTestCase; |
27 |
|
import org.qedeq.kernel.se.base.list.Element; |
28 |
|
import org.qedeq.kernel.se.base.module.FormalProofLineList; |
29 |
|
import org.qedeq.kernel.se.base.module.Proposition; |
30 |
|
import org.qedeq.kernel.se.common.DefaultModuleAddress; |
31 |
|
import org.qedeq.kernel.se.common.ModuleAddress; |
32 |
|
import org.qedeq.kernel.se.common.ModuleContext; |
33 |
|
import org.qedeq.kernel.se.common.RuleKey; |
34 |
|
import org.qedeq.kernel.se.dto.list.DefaultAtom; |
35 |
|
import org.qedeq.kernel.se.dto.list.DefaultElementList; |
36 |
|
import org.qedeq.kernel.se.dto.module.FormalProofLineListVo; |
37 |
|
|
38 |
|
|
39 |
|
|
40 |
|
|
41 |
|
@author |
42 |
|
|
|
|
| 95.5% |
Uncovered Elements: 6 (134) |
Complexity: 20 |
Complexity Density: 0.19 |
|
43 |
|
public class ProofCheckerTest extends QedeqBoTestCase { |
44 |
|
|
45 |
|
private ProofChecker checker0; |
46 |
|
|
47 |
|
private ProofChecker checker1; |
48 |
|
|
49 |
|
private ProofChecker checker2; |
50 |
|
|
51 |
|
private RuleChecker ruleCheckerAll; |
52 |
|
|
53 |
|
private ReferenceResolver resolverLocal; |
54 |
|
|
55 |
|
private Element disjunction_idempotence_axiom = |
56 |
|
new DefaultElementList("IMPL", new Element[] { |
57 |
|
new DefaultElementList("OR", new Element[] { |
58 |
|
new DefaultElementList("PREDVAR", new Element[] { |
59 |
|
new DefaultAtom("A") |
60 |
|
}), |
61 |
|
new DefaultElementList("PREDVAR", new Element[] { |
62 |
|
new DefaultAtom("A") |
63 |
|
}) |
64 |
|
}), |
65 |
|
new DefaultElementList("PREDVAR", new Element[] { |
66 |
|
new DefaultAtom("A") |
67 |
|
}) |
68 |
|
}); |
69 |
|
|
70 |
|
private Element disjunction_weakening_axiom = |
71 |
|
new DefaultElementList("IMPL", new Element[] { |
72 |
|
new DefaultElementList("PREDVAR", new Element[] { |
73 |
|
new DefaultAtom("A") |
74 |
|
}), |
75 |
|
new DefaultElementList("OR", new Element[] { |
76 |
|
new DefaultElementList("PREDVAR", new Element[] { |
77 |
|
new DefaultAtom("A") |
78 |
|
}), |
79 |
|
new DefaultElementList("PREDVAR", new Element[] { |
80 |
|
new DefaultAtom("B") |
81 |
|
}) |
82 |
|
}) |
83 |
|
}); |
84 |
|
|
85 |
|
private Element disjunction_addition_axiom = |
86 |
|
new DefaultElementList("IMPL", new Element[] { |
87 |
|
new DefaultElementList("IMPL", new Element[] { |
88 |
|
new DefaultElementList("PREDVAR", new Element[] { |
89 |
|
new DefaultAtom("A") |
90 |
|
}), |
91 |
|
new DefaultElementList("PREDVAR", new Element[] { |
92 |
|
new DefaultAtom("B") |
93 |
|
}) |
94 |
|
}), |
95 |
|
new DefaultElementList("IMPL", new Element[] { |
96 |
|
new DefaultElementList("IMPL", new Element[] { |
97 |
|
new DefaultElementList("PREDVAR", new Element[] { |
98 |
|
new DefaultAtom("C") |
99 |
|
}), |
100 |
|
new DefaultElementList("PREDVAR", new Element[] { |
101 |
|
new DefaultAtom("A") |
102 |
|
}) |
103 |
|
}), |
104 |
|
new DefaultElementList("IMPL", new Element[] { |
105 |
|
new DefaultElementList("PREDVAR", new Element[] { |
106 |
|
new DefaultAtom("C") |
107 |
|
}), |
108 |
|
new DefaultElementList("PREDVAR", new Element[] { |
109 |
|
new DefaultAtom("B") |
110 |
|
}) |
111 |
|
}) |
112 |
|
}) |
113 |
|
}); |
114 |
|
|
115 |
|
private Element universal_instantiation_axiom = |
116 |
|
new DefaultElementList("IMPL", new Element[] { |
117 |
|
new DefaultElementList("FORALL", new Element[] { |
118 |
|
new DefaultElementList("VAR", new Element[] { |
119 |
|
new DefaultAtom("x") |
120 |
|
}), |
121 |
|
new DefaultElementList("PREDVAR", new Element[] { |
122 |
|
new DefaultAtom("\\phi"), |
123 |
|
new DefaultElementList("VAR", new Element[] { |
124 |
|
new DefaultAtom("x") |
125 |
|
}) |
126 |
|
}) |
127 |
|
}), |
128 |
|
new DefaultElementList("PREDVAR", new Element[] { |
129 |
|
new DefaultAtom("\\phi"), |
130 |
|
new DefaultElementList("VAR", new Element[] { |
131 |
|
new DefaultAtom("y") |
132 |
|
}) |
133 |
|
}) |
134 |
|
}); |
135 |
|
|
136 |
|
private Element existencial_generalization_axiom = |
137 |
|
new DefaultElementList("IMPL", new Element[] { |
138 |
|
new DefaultElementList("PREDVAR", new Element[] { |
139 |
|
new DefaultAtom("\\phi"), |
140 |
|
new DefaultElementList("VAR", new Element[] { |
141 |
|
new DefaultAtom("y") |
142 |
|
}) |
143 |
|
}), |
144 |
|
new DefaultElementList("EXISTS", new Element[] { |
145 |
|
new DefaultElementList("VAR", new Element[] { |
146 |
|
new DefaultAtom("x") |
147 |
|
}), |
148 |
|
new DefaultElementList("PREDVAR", new Element[] { |
149 |
|
new DefaultAtom("\\phi"), |
150 |
|
new DefaultElementList("VAR", new Element[] { |
151 |
|
new DefaultAtom("x") |
152 |
|
}) |
153 |
|
}) |
154 |
|
}) |
155 |
|
}); |
156 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (6) |
Complexity: 1 |
Complexity Density: 0.17 |
|
157 |
3
|
public void setUp() throws Exception {... |
158 |
3
|
super.setUp(); |
159 |
3
|
checker0 = new ProofChecker0Impl(); |
160 |
3
|
checker1 = new ProofChecker1Impl(); |
161 |
3
|
checker2 = new ProofChecker2Impl(); |
162 |
3
|
ruleCheckerAll = new RuleChecker() { |
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
163 |
96
|
public RuleKey getRule(String ruleName) {... |
164 |
96
|
return new RuleKey(ruleName, "0.01.00"); |
165 |
|
} |
166 |
|
}; |
167 |
3
|
resolverLocal = new ReferenceResolver() { |
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
168 |
264
|
public Element getNormalizedFormula(Element element) {... |
169 |
264
|
return element; |
170 |
|
} |
171 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
172 |
0
|
public Element getNormalizedLocalProofLineReference(String reference) {... |
173 |
0
|
return null; |
174 |
|
} |
175 |
|
|
|
|
| 90.5% |
Uncovered Elements: 2 (21) |
Complexity: 6 |
Complexity Density: 0.55 |
|
176 |
20
|
public Element getNormalizedReferenceFormula(String reference) {... |
177 |
20
|
if ("axiom:disjunction_idempotence".equals(reference)) { |
178 |
2
|
return disjunction_idempotence_axiom; |
179 |
18
|
} else if ("axiom:disjunction_weakening".equals(reference)) { |
180 |
2
|
return disjunction_weakening_axiom; |
181 |
16
|
} else if ("axiom:disjunction_addition".equals(reference)) { |
182 |
8
|
return disjunction_addition_axiom; |
183 |
8
|
} else if ("axiom:universalInstantiation".equals(reference)) { |
184 |
6
|
return universal_instantiation_axiom; |
185 |
2
|
} else if ("axiom:existencialGeneralization".equals(reference)) { |
186 |
2
|
return existencial_generalization_axiom; |
187 |
|
} |
188 |
0
|
return null; |
189 |
|
} |
190 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
191 |
0
|
public ModuleContext getReferenceContext(String reference) {... |
192 |
0
|
return null; |
193 |
|
} |
194 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
195 |
48
|
public boolean isLocalProofLineReference(String reference) {... |
196 |
48
|
return false; |
197 |
|
} |
198 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
199 |
20
|
public boolean isProvedFormula(String reference) {... |
200 |
20
|
return true; |
201 |
|
} |
202 |
|
}; |
203 |
|
} |
204 |
|
|
205 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (25) |
Complexity: 2 |
Complexity Density: 0.09 |
1
PASS
|
|
206 |
1
|
public void testCheck1() throws Exception {... |
207 |
1
|
final ModuleAddress address = new DefaultModuleAddress(new File(getDocDir(), |
208 |
|
"sample/qedeq_sample3.xml")); |
209 |
1
|
KernelContext.getInstance().checkWellFormedness(address); |
210 |
1
|
final KernelQedeqBo bo = (KernelQedeqBo) KernelContext.getInstance().getQedeqBo(address); |
211 |
1
|
assertTrue(bo.isWellFormed()); |
212 |
1
|
assertNotNull(bo.getWarnings()); |
213 |
1
|
assertEquals(0, bo.getWarnings().size()); |
214 |
1
|
assertEquals(0, bo.getErrors().size()); |
215 |
1
|
final KernelNodeBo node = bo.getLabels().getNode("proposition:one"); |
216 |
1
|
final Proposition prop = node.getNodeVo().getNodeType().getProposition(); |
217 |
1
|
final FormalProofLineList original = prop.getFormalProofList().get(0) |
218 |
|
.getFormalProofLineList(); |
219 |
1
|
final FormalProofLineListVo list = new FormalProofLineListVo(); |
220 |
10
|
for (int i = 0; i < 9; i++) { |
221 |
9
|
list.add(original.get(i)); |
222 |
|
} |
223 |
1
|
LogicalCheckExceptionList e0 = |
224 |
|
checker0.checkProof(prop.getFormula().getElement(), list, ruleCheckerAll, |
225 |
|
DefaultModuleAddress.MEMORY.createModuleContext(), resolverLocal); |
226 |
1
|
assertNotNull(e0); |
227 |
1
|
assertEquals(1, e0.size()); |
228 |
1
|
assertEquals(37400, e0.get(0).getErrorCode()); |
229 |
1
|
LogicalCheckExceptionList e1 = |
230 |
|
checker1.checkProof(prop.getFormula().getElement(), list, ruleCheckerAll, |
231 |
|
DefaultModuleAddress.MEMORY.createModuleContext(), resolverLocal); |
232 |
1
|
assertNotNull(e1); |
233 |
1
|
assertEquals(0, e1.size()); |
234 |
1
|
LogicalCheckExceptionList e2 = |
235 |
|
checker2.checkProof(prop.getFormula().getElement(), list, ruleCheckerAll, |
236 |
|
DefaultModuleAddress.MEMORY.createModuleContext(), resolverLocal); |
237 |
1
|
assertNotNull(e2); |
238 |
1
|
assertEquals(0, e2.size()); |
239 |
|
} |
240 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (25) |
Complexity: 2 |
Complexity Density: 0.09 |
1
PASS
|
|
241 |
1
|
public void testCheck4() throws Exception {... |
242 |
1
|
final ModuleAddress address = new DefaultModuleAddress(new File(getDocDir(), |
243 |
|
"sample/qedeq_sample3.xml")); |
244 |
1
|
KernelContext.getInstance().checkWellFormedness(address); |
245 |
1
|
final KernelQedeqBo bo = (KernelQedeqBo) KernelContext.getInstance().getQedeqBo(address); |
246 |
1
|
assertTrue(bo.isWellFormed()); |
247 |
1
|
assertNotNull(bo.getWarnings()); |
248 |
1
|
assertEquals(0, bo.getWarnings().size()); |
249 |
1
|
assertEquals(0, bo.getErrors().size()); |
250 |
1
|
final KernelNodeBo node = bo.getLabels().getNode("proposition:four"); |
251 |
1
|
final Proposition prop = node.getNodeVo().getNodeType().getProposition(); |
252 |
1
|
final FormalProofLineList original = prop.getFormalProofList().get(0) |
253 |
|
.getFormalProofLineList(); |
254 |
1
|
final FormalProofLineListVo list = new FormalProofLineListVo(); |
255 |
9
|
for (int i = 0; i < 8; i++) { |
256 |
8
|
list.add(original.get(i)); |
257 |
|
} |
258 |
1
|
LogicalCheckExceptionList e0 = |
259 |
|
checker0.checkProof(prop.getFormula().getElement(), list, ruleCheckerAll, |
260 |
|
DefaultModuleAddress.MEMORY.createModuleContext(), resolverLocal); |
261 |
1
|
assertNotNull(e0); |
262 |
1
|
assertEquals(1, e0.size()); |
263 |
1
|
assertEquals(37400, e0.get(0).getErrorCode()); |
264 |
1
|
LogicalCheckExceptionList e1 = |
265 |
|
checker1.checkProof(prop.getFormula().getElement(), list, ruleCheckerAll, |
266 |
|
DefaultModuleAddress.MEMORY.createModuleContext(), resolverLocal); |
267 |
1
|
assertNotNull(e1); |
268 |
1
|
assertEquals(0, e1.size()); |
269 |
1
|
LogicalCheckExceptionList e2 = |
270 |
|
checker2.checkProof(prop.getFormula().getElement(), list, ruleCheckerAll, |
271 |
|
DefaultModuleAddress.MEMORY.createModuleContext(), resolverLocal); |
272 |
1
|
assertNotNull(e2); |
273 |
1
|
assertEquals(0, e2.size()); |
274 |
|
} |
275 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (40) |
Complexity: 3 |
Complexity Density: 0.08 |
1
PASS
|
|
276 |
1
|
public void testCheck6() throws Exception {... |
277 |
1
|
final ModuleAddress address = new DefaultModuleAddress(new File(getDocDir(), |
278 |
|
"sample/qedeq_sample3.xml")); |
279 |
1
|
KernelContext.getInstance().checkWellFormedness(address); |
280 |
1
|
final KernelQedeqBo bo = (KernelQedeqBo) KernelContext.getInstance().getQedeqBo(address); |
281 |
1
|
assertTrue(bo.isWellFormed()); |
282 |
1
|
assertNotNull(bo.getWarnings()); |
283 |
1
|
assertEquals(0, bo.getWarnings().size()); |
284 |
1
|
assertEquals(0, bo.getErrors().size()); |
285 |
1
|
final KernelNodeBo node = bo.getLabels().getNode("proposition:six"); |
286 |
1
|
final Proposition prop = node.getNodeVo().getNodeType().getProposition(); |
287 |
1
|
final FormalProofLineList original = prop.getFormalProofList().get(0) |
288 |
|
.getFormalProofLineList(); |
289 |
1
|
FormalProofLineListVo list = new FormalProofLineListVo(); |
290 |
16
|
for (int i = 0; i < 15; i++) { |
291 |
15
|
list.add(original.get(i)); |
292 |
|
} |
293 |
1
|
LogicalCheckExceptionList e0 = |
294 |
|
checker0.checkProof(prop.getFormula().getElement(), list, ruleCheckerAll, |
295 |
|
DefaultModuleAddress.MEMORY.createModuleContext(), resolverLocal); |
296 |
1
|
assertNotNull(e0); |
297 |
1
|
assertEquals(1, e0.size()); |
298 |
1
|
assertEquals(37400, e0.get(0).getErrorCode()); |
299 |
1
|
LogicalCheckExceptionList e2 = |
300 |
|
checker1.checkProof(prop.getFormula().getElement(), list, ruleCheckerAll, |
301 |
|
DefaultModuleAddress.MEMORY.createModuleContext(), resolverLocal); |
302 |
1
|
assertNotNull(e2); |
303 |
1
|
assertEquals(1, e2.size()); |
304 |
1
|
assertEquals(37200, e2.get(0).getErrorCode()); |
305 |
1
|
list.add(original.get(15)); |
306 |
1
|
LogicalCheckExceptionList e3 = |
307 |
|
checker1.checkProof(prop.getFormula().getElement(), list, ruleCheckerAll, |
308 |
|
DefaultModuleAddress.MEMORY.createModuleContext(), resolverLocal); |
309 |
1
|
assertNotNull(e3); |
310 |
1
|
assertEquals(0, e3.size()); |
311 |
|
|
312 |
1
|
list = new FormalProofLineListVo(); |
313 |
16
|
for (int i = 0; i < 15; i++) { |
314 |
15
|
list.add(original.get(i)); |
315 |
|
} |
316 |
1
|
LogicalCheckExceptionList e4 = |
317 |
|
checker2.checkProof(prop.getFormula().getElement(), list, ruleCheckerAll, |
318 |
|
DefaultModuleAddress.MEMORY.createModuleContext(), resolverLocal); |
319 |
1
|
assertNotNull(e4); |
320 |
|
|
321 |
|
|
322 |
|
|
323 |
|
|
324 |
1
|
assertEquals(1, e4.size()); |
325 |
|
|
326 |
1
|
assertEquals(37200, e4.get(0).getErrorCode()); |
327 |
1
|
list.add(original.get(15)); |
328 |
1
|
LogicalCheckExceptionList e5 = |
329 |
|
checker2.checkProof(prop.getFormula().getElement(), list, ruleCheckerAll, |
330 |
|
DefaultModuleAddress.MEMORY.createModuleContext(), resolverLocal); |
331 |
1
|
assertNotNull(e5); |
332 |
|
|
333 |
|
|
334 |
|
|
335 |
|
|
336 |
1
|
assertEquals(0, e5.size()); |
337 |
|
} |
338 |
|
|
339 |
|
} |