001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
004 *
005 * "Hilbert II" is free software; you can redistribute
006 * it and/or modify it under the terms of the GNU General Public
007 * License as published by the Free Software Foundation; either
008 * version 2 of the License, or (at your option) any later version.
009 *
010 * This program is distributed in the hope that it will be useful,
011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
013 * GNU General Public License for more details.
014 */
015
016 package org.qedeq.kernel.bo.logic.proof.checker;
017
018 import org.qedeq.kernel.se.common.ErrorCodes;
019
020 /**
021 * Error codes and messages for proof checker.
022 *
023 * @author Michael Meyling
024 */
025 public interface BasicProofErrors extends ErrorCodes {
026
027 /** Error code. */
028 public static final int PROOF_LINE_MUST_NOT_BE_NULL_CODE = 37100;
029
030 /** Error message. */
031 public static final String PROOF_LINE_MUST_NOT_BE_NULL_TEXT
032 = "proof line must not be empty";
033
034
035 /** Error code. */
036 public static final int REASON_MUST_NOT_BE_NULL_CODE = 37110;
037
038 /** Error message. */
039 public static final String REASON_MUST_NOT_BE_NULL_TEXT
040 = "reason must not be empty";
041
042
043 /** Error code. */
044 public static final int THIS_IS_NO_ALLOWED_BASIC_REASON_CODE = 37120;
045
046 /** Error message. */
047 public static final String THIS_IS_NO_ALLOWED_BASIC_REASON_TEXT
048 = "this is no allowed basic rule: ";
049
050
051 /** Error code. */
052 public static final int THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE = 37130;
053
054 /** Error message. */
055 public static final String THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
056 = "this is not a reference to a proved formula: ";
057
058
059 /** Error code. */
060 public static final int EXPECTED_FORMULA_DIFFERS_CODE = 37140;
061
062 /** Error message. */
063 public static final String EXPECTED_FORMULA_DIFFERS_TEXT
064 = "this is not the expected part formula, please check with label: ";
065
066
067 /** Error code. */
068 public static final int EXPECTED_FORMULA_DIFFERS_2_CODE = 37142;
069
070 /** Error message. */
071 public static final String EXPECTED_FORMULA_DIFFERS_2_TEXT
072 = "this is not the expected part formula";
073
074
075 /** Error code. */
076 public static final int LOCAL_LABEL_ALREADY_EXISTS_CODE = 37150;
077
078 /** Error message. */
079 public static final String LOCAL_LABEL_ALREADY_EXISTS_TEXT
080 = "this proof line label exists already in this proof: ";
081
082
083 /** Error code. */
084 public static final int SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE = 37160;
085
086 /** Error message. */
087 public static final String SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
088 = "this proof line label dosn't (yet) exist in this proof: ";
089
090
091 /** Error code. */
092 public static final int IMPLICATION_EXPECTED_CODE = 37170;
093
094 /** Error message. */
095 public static final String IMPLICATION_EXPECTED_TEXT
096 = "this proof line label must point to an implication (with two arguments): ";
097
098
099 /** Error code. */
100 public static final int MUST_BE_HYPOTHESIS_OF_FIRST_REFERENCE_CODE = 37180;
101
102 /** Error message. */
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 /** Error code. */
108 public static final int CURRENT_MUST_BE_CONCLUSION_CODE = 37190;
109
110 /** Error message. */
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 /** Error code. */
116 public static final int LAST_PROOF_LINE_MUST_BE_IDENTICAL_TO_PROPOSITION_CODE = 37200;
117
118 /** Error message. */
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 /** Error code. */
124 public static final int SUBSTITUTION_FORMULA_IS_MISSING_CODE = 37210;
125
126 /** Error message. */
127 public static final String SUBSTITUTION_FORMULA_IS_MISSING_TEXT
128 = "the substitution formula is missing";
129
130
131 /** Error code. */
132 public static final int REFERENCE_TO_PROVED_FORMULA_IS_MISSING_CODE = 37220;
133
134 /** Error message. */
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 /** Error code. */
140 public static final int SUBSTITUTION_TERM_IS_MISSING_CODE = 37230;
141
142 /** Error message. */
143 public static final String SUBSTITUTION_TERM_IS_MISSING_TEXT
144 = "the substitution term is missing";
145
146
147 /** Error code. */
148 public static final int ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE = 37240;
149
150 /** Error message. */
151 public static final String ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT
152 = "only free subject variables as parameters allowed";
153
154
155 /** Error code. */
156 public static final int FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_CODE = 37250;
157
158 /** Error message. */
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 /** Error code. */
164 public static final int SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_CODE = 37260;
165
166 /** Error message. */
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 /** Error code. */
173 public static final int SUBJECT_VARIABLE_IS_MISSING_CODE = 37270;
174
175 /** Error message. */
176 public static final String SUBJECT_VARIABLE_IS_MISSING_TEXT
177 = "subject variable is missing";
178
179
180 /** Error code. */
181 public static final int MISSING_PROOF_LINE_FOR_CONDITIONAL_PROOF_CODE = 37370;
182
183 /** Error message. */
184 public static final String MISSING_PROOF_LINE_FOR_CONDITIONAL_PROOF_TEXT
185 = "missing proof lines for conditional proof";
186
187
188 /** Error code. */
189 public static final int SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_CODE = 37380;
190
191 /** Error message. */
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 /** Error code. */
197 public static final int NO_FORMAL_PROOFS_SUPORTED_CODE = 37400;
198
199 /** Error message. */
200 public static final String NO_FORMAL_PROOFS_SUPORTED_TEXT
201 = "the module has rule version that forbids formal proofs: ";
202
203
204 /** Error code. */
205 public static final int CONDITIONS_AND_FORMULA_DONT_AGREE_CODE = 37410;
206
207 /** Error message. */
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 /** Error code. */
213 public static final int PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE = 37420;
214
215 /** Error message. */
216 public static final String PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
217 = "proof method was not defined yet: ";
218
219
220 /** Error code. */
221 public static final int PROOF_METHOD_IS_NOT_SUPPORTED_CODE = 37430;
222
223 /** Error message. */
224 public static final String PROOF_METHOD_IS_NOT_SUPPORTED_TEXT
225 = "proof method is not supported for this proof checker: ";
226
227 /** Error message. Part two. */
228 public static final String PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2
229 = ", we only support: ";
230
231
232 /** Error code. */
233 public static final int HIGHER_PROOF_RULE_VERSION_NEEDED_CODE = 37440;
234
235 /** Error message. */
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 /** Error message. Part 2. */
240 public static final String HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2
241 = ", current: ";
242
243
244 }
|