1 |
|
|
2 |
|
|
3 |
|
|
4 |
|
|
5 |
|
|
6 |
|
|
7 |
|
|
8 |
|
|
9 |
|
|
10 |
|
|
11 |
|
|
12 |
|
|
13 |
|
|
14 |
|
|
15 |
|
|
16 |
|
package org.qedeq.kernel.bo.logic.proof.checker; |
17 |
|
|
18 |
|
import org.qedeq.kernel.se.common.ErrorCodes; |
19 |
|
|
20 |
|
|
21 |
|
|
22 |
|
|
23 |
|
@author |
24 |
|
|
|
|
| - |
Uncovered Elements: 0 (0) |
Complexity: 0 |
Complexity Density: - |
|
25 |
|
public interface BasicProofErrors extends ErrorCodes { |
26 |
|
|
27 |
|
|
28 |
|
public static final int PROOF_LINE_MUST_NOT_BE_NULL_CODE = 37100; |
29 |
|
|
30 |
|
|
31 |
|
public static final String PROOF_LINE_MUST_NOT_BE_NULL_TEXT |
32 |
|
= "proof line must not be empty"; |
33 |
|
|
34 |
|
|
35 |
|
|
36 |
|
public static final int REASON_MUST_NOT_BE_NULL_CODE = 37110; |
37 |
|
|
38 |
|
|
39 |
|
public static final String REASON_MUST_NOT_BE_NULL_TEXT |
40 |
|
= "reason must not be empty"; |
41 |
|
|
42 |
|
|
43 |
|
|
44 |
|
public static final int THIS_IS_NO_ALLOWED_BASIC_REASON_CODE = 37120; |
45 |
|
|
46 |
|
|
47 |
|
public static final String THIS_IS_NO_ALLOWED_BASIC_REASON_TEXT |
48 |
|
= "this is no allowed basic rule: "; |
49 |
|
|
50 |
|
|
51 |
|
|
52 |
|
public static final int THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE = 37130; |
53 |
|
|
54 |
|
|
55 |
|
public static final String THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT |
56 |
|
= "this is not a reference to a proved formula: "; |
57 |
|
|
58 |
|
|
59 |
|
|
60 |
|
public static final int EXPECTED_FORMULA_DIFFERS_CODE = 37140; |
61 |
|
|
62 |
|
|
63 |
|
public static final String EXPECTED_FORMULA_DIFFERS_TEXT |
64 |
|
= "this is not the expected part formula, please check with label: "; |
65 |
|
|
66 |
|
|
67 |
|
|
68 |
|
public static final int EXPECTED_FORMULA_DIFFERS_2_CODE = 37142; |
69 |
|
|
70 |
|
|
71 |
|
public static final String EXPECTED_FORMULA_DIFFERS_2_TEXT |
72 |
|
= "this is not the expected part formula"; |
73 |
|
|
74 |
|
|
75 |
|
|
76 |
|
public static final int LOCAL_LABEL_ALREADY_EXISTS_CODE = 37150; |
77 |
|
|
78 |
|
|
79 |
|
public static final String LOCAL_LABEL_ALREADY_EXISTS_TEXT |
80 |
|
= "this proof line label exists already in this proof: "; |
81 |
|
|
82 |
|
|
83 |
|
|
84 |
|
public static final int SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE = 37160; |
85 |
|
|
86 |
|
|
87 |
|
public static final String SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT |
88 |
|
= "this proof line label dosn't (yet) exist in this proof: "; |
89 |
|
|
90 |
|
|
91 |
|
|
92 |
|
public static final int IMPLICATION_EXPECTED_CODE = 37170; |
93 |
|
|
94 |
|
|
95 |
|
public static final String IMPLICATION_EXPECTED_TEXT |
96 |
|
= "this proof line label must point to an implication (with two arguments): "; |
97 |
|
|
98 |
|
|
99 |
|
|
100 |
|
public static final int MUST_BE_HYPOTHESIS_OF_FIRST_REFERENCE_CODE = 37180; |
101 |
|
|
102 |
|
|
103 |
|
public static final String MUST_BE_HYPOTHESIS_OF_FIRST_REFERENCE_TEXT |
104 |
|
= "this proof line label must be the hypothesis for the first reference: "; |
105 |
|
|
106 |
|
|
107 |
|
|
108 |
|
public static final int CURRENT_MUST_BE_CONCLUSION_CODE = 37190; |
109 |
|
|
110 |
|
|
111 |
|
public static final String CURRENT_MUST_BE_CONCLUSION_TEXT |
112 |
|
= "this proof line must be the conclusion of the first reference: "; |
113 |
|
|
114 |
|
|
115 |
|
|
116 |
|
public static final int LAST_PROOF_LINE_MUST_BE_IDENTICAL_TO_PROPOSITION_CODE = 37200; |
117 |
|
|
118 |
|
|
119 |
|
public static final String LAST_PROOF_LINE_MUST_BE_IDENTICAL_TO_PROPOSITION_TEXT |
120 |
|
= "the last proof line must be identical to the proposition formula"; |
121 |
|
|
122 |
|
|
123 |
|
|
124 |
|
public static final int SUBSTITUTION_FORMULA_IS_MISSING_CODE = 37210; |
125 |
|
|
126 |
|
|
127 |
|
public static final String SUBSTITUTION_FORMULA_IS_MISSING_TEXT |
128 |
|
= "the substitution formula is missing"; |
129 |
|
|
130 |
|
|
131 |
|
|
132 |
|
public static final int REFERENCE_TO_PROVED_FORMULA_IS_MISSING_CODE = 37220; |
133 |
|
|
134 |
|
|
135 |
|
public static final String REFERENCE_TO_PROVED_FORMULA_IS_MISSING_TEXT |
136 |
|
= "this is not a reference to a proved formula: "; |
137 |
|
|
138 |
|
|
139 |
|
|
140 |
|
public static final int SUBSTITUTION_TERM_IS_MISSING_CODE = 37230; |
141 |
|
|
142 |
|
|
143 |
|
public static final String SUBSTITUTION_TERM_IS_MISSING_TEXT |
144 |
|
= "the substitution term is missing"; |
145 |
|
|
146 |
|
|
147 |
|
|
148 |
|
public static final int ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE = 37240; |
149 |
|
|
150 |
|
|
151 |
|
public static final String ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT |
152 |
|
= "only free subject variables as parameters allowed"; |
153 |
|
|
154 |
|
|
155 |
|
|
156 |
|
public static final int FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_CODE = 37250; |
157 |
|
|
158 |
|
|
159 |
|
public static final String FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_TEXT |
160 |
|
= "free subject variables should not get bound during substitution"; |
161 |
|
|
162 |
|
|
163 |
|
|
164 |
|
public static final int SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_CODE = 37260; |
165 |
|
|
166 |
|
|
167 |
|
public static final String SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_TEXT |
168 |
|
= "the substitution location contains subject variables that are bound within the " |
169 |
|
+ "replacement formula"; |
170 |
|
|
171 |
|
|
172 |
|
|
173 |
|
public static final int SUBJECT_VARIABLE_IS_MISSING_CODE = 37270; |
174 |
|
|
175 |
|
|
176 |
|
public static final String SUBJECT_VARIABLE_IS_MISSING_TEXT |
177 |
|
= "subject variable is missing"; |
178 |
|
|
179 |
|
|
180 |
|
|
181 |
|
public static final int MISSING_PROOF_LINE_FOR_CONDITIONAL_PROOF_CODE = 37370; |
182 |
|
|
183 |
|
|
184 |
|
public static final String MISSING_PROOF_LINE_FOR_CONDITIONAL_PROOF_TEXT |
185 |
|
= "missing proof lines for conditional proof"; |
186 |
|
|
187 |
|
|
188 |
|
|
189 |
|
public static final int SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_CODE = 37380; |
190 |
|
|
191 |
|
|
192 |
|
public static final String SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_TEXT |
193 |
|
= "the operator that should be substituted was found within a precondition"; |
194 |
|
|
195 |
|
|
196 |
|
|
197 |
|
public static final int NO_FORMAL_PROOFS_SUPORTED_CODE = 37400; |
198 |
|
|
199 |
|
|
200 |
|
public static final String NO_FORMAL_PROOFS_SUPORTED_TEXT |
201 |
|
= "the module has rule version that forbids formal proofs: "; |
202 |
|
|
203 |
|
|
204 |
|
|
205 |
|
public static final int CONDITIONS_AND_FORMULA_DONT_AGREE_CODE = 37410; |
206 |
|
|
207 |
|
|
208 |
|
public static final String CONDITIONS_AND_FORMULA_DONT_AGREE_TEXT |
209 |
|
= "the conditions for this proof line doesn't agree with the formula "; |
210 |
|
|
211 |
|
|
212 |
|
|
213 |
|
public static final int PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE = 37420; |
214 |
|
|
215 |
|
|
216 |
|
public static final String PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT |
217 |
|
= "proof method was not defined yet: "; |
218 |
|
|
219 |
|
|
220 |
|
|
221 |
|
public static final int PROOF_METHOD_IS_NOT_SUPPORTED_CODE = 37430; |
222 |
|
|
223 |
|
|
224 |
|
public static final String PROOF_METHOD_IS_NOT_SUPPORTED_TEXT |
225 |
|
= "proof method is not supported for this proof checker: "; |
226 |
|
|
227 |
|
|
228 |
|
public static final String PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 |
229 |
|
= ", we only support: "; |
230 |
|
|
231 |
|
|
232 |
|
|
233 |
|
public static final int HIGHER_PROOF_RULE_VERSION_NEEDED_CODE = 37440; |
234 |
|
|
235 |
|
|
236 |
|
public static final String HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT |
237 |
|
= "you need a higher rule version for applying this rule here, needed: "; |
238 |
|
|
239 |
|
|
240 |
|
public static final String HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 |
241 |
|
= ", current: "; |
242 |
|
|
243 |
|
|
244 |
|
} |