001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2011, 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.basic;
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 ELEMENT_MUST_NOT_BE_NULL_TEXT
032 = "proof line must not be null";
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 null";
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 LOCAL_LABEL_ALREADY_EXISTS_CODE = 37150;
069
070 /** Error message. */
071 public static final String LOCAL_LABEL_ALREADY_EXISTS_TEXT
072 = "this proof line label exists already in this proof: ";
073
074
075 /** Error code. */
076 public static final int SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE = 37160;
077
078 /** Error message. */
079 public static final String SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
080 = "this proof line label dosn't (yet) exist in this proof: ";
081
082
083 /** Error code. */
084 public static final int IMPLICATION_EXPECTED_CODE = 37170;
085
086 /** Error message. */
087 public static final String IMPLICATION_EXPECTED_TEXT
088 = "this proof line label must point to an implication (with two arguments): ";
089
090
091 /** Error code. */
092 public static final int MUST_BE_HYPOTHESIS_OF_FIRST_REFERENCE_CODE = 37180;
093
094 /** Error message. */
095 public static final String MUST_BE_HYPOTHESIS_OF_FIRST_REFERENCE_TEXT
096 = "this proof line label must be the hypothesis for the first reference: ";
097
098
099 /** Error code. */
100 public static final int CURRENT_MUST_BE_CONCLUSION_CODE = 37190;
101
102 /** Error message. */
103 public static final String CURRENT_MUST_BE_CONCLUSION_TEXT
104 = "this proof line must be the conclusion of the first reference: ";
105
106
107 /** Error code. */
108 public static final int LAST_PROOF_LINE_MUST_BE_IDENTICAL_TO_PROPOSITION_CODE = 37200;
109
110 /** Error message. */
111 public static final String LAST_PROOF_LINE_MUST_BE_IDENTICAL_TO_PROPOSITION_TEXT
112 = "the last proof line must be identical to the proposition formula";
113
114
115 /** Error code. */
116 public static final int SUBSTITUTION_FORMULA_IS_MISSING_CODE = 37210;
117
118 /** Error message. */
119 public static final String SUBSTITUTION_FORMULA_IS_MISSING_TEXT
120 = "the substitution formula is missing";
121
122
123 /** Error code. */
124 public static final int REFERENCE_TO_PROVED_FORMULA_IS_MISSING_CODE = 37220;
125
126 /** Error message. */
127 public static final String REFERENCE_TO_PROVED_FORMULA_IS_MISSING_TEXT
128 = "this is not a reference to a proved formula: ";
129
130
131 /** Error code. */
132 public static final int SUBSTITUTION_TERM_IS_MISSING_CODE = 37230;
133
134 /** Error message. */
135 public static final String SUBSTITUTION_TERM_IS_MISSING_TEXT
136 = "the substitution term is missing";
137
138
139 /** Error code. */
140 public static final int ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE = 37240;
141
142 /** Error message. */
143 public static final String ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT
144 = "only free subject variables as parameters allowed";
145
146
147 /** Error code. */
148 public static final int FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_CODE = 37250;
149
150 /** Error message. */
151 public static final String FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_TEXT
152 = "free subject variables should not get bound during substitution";
153
154
155 /** Error code. */
156 public static final int SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_CODE = 37260;
157
158 /** Error message. */
159 public static final String SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_TEXT
160 = "the substitution location contains subject variables that are bound within the "
161 + "replacement formula";
162
163
164 /** Error code. */
165 public static final int SUBJECT_VARIABLE_IS_MISSING_CODE = 37270;
166
167 /** Error message. */
168 public static final String SUBJECT_VARIABLE_IS_MISSING_TEXT
169 = "subject variable is missing";
170
171
172 }
|