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.service.logic;
017
018 import org.qedeq.kernel.se.common.ErrorCodes;
019
020 /**
021 * Error codes and messages for service package.
022 *
023 * @author Michael Meyling
024 */
025 public interface LogicErrors extends ErrorCodes {
026
027 /** Error code. */
028 public static final int IDENTITY_OPERATOR_ALREADY_EXISTS_CODE = 123476;
029
030 /** Error message. */
031 public static final String IDENTITY_OPERATOR_ALREADY_EXISTS_TEXT
032 = "identity operator already defined with";
033
034
035 /** Error code. */
036 public static final int PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_CODE = 30810;
037
038 /** Error message. */
039 public static final String PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_TEXT
040 = "a predicate definition needs an equivalence relation (with two parameters)";
041
042
043 /** Error code. */
044 public static final int PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_CODE = 30810;
045
046 /** Error message. */
047 public static final String PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_TEXT
048 = "a predicate definition needs an predicate constant as the first parameter";
049
050
051 /** Error code. */
052 public static final int MUST_HAVE_NAME_OF_PREDICATE_CODE = 40720;
053
054 /** Error message. */
055 public static final String MUST_HAVE_NAME_OF_PREDICATE_TEXT
056 = "predicate name found is not as expected: ";
057
058
059 /** Error code. */
060 public static final int FUNCTION_ALREADY_DEFINED_CODE = 40400;
061
062 /** Error message. */
063 public static final String FUNCTION_ALREADY_DEFINED_TEXT
064 = "function was already defined for this argument number: ";
065
066
067 /** Error code. */
068 public static final int NO_DEFINITION_FORMULA_FOR_FUNCTION_CODE = 40730;
069
070 /** Error message. */
071 public static final String NO_DEFINITION_FORMULA_FOR_FUNCTION_TEXT
072 = "no definition formula for new function found";
073
074
075 /** Error code. */
076 public static final int DEFINITION_FORMULA_FOR_FUNCTION_MUST_START_WITH_EQUAL_RELATION_CODE = 40740;
077
078 /** Error message. */
079 public static final String DEFINITION_FORMULA_FOR_FUNCTION_MUST_START_WITH_EQUAL_RELATION_TEXT
080 = "definition formula for new function must start with an equal relation";
081
082
083 /** Error code. */
084 public static final int PREDICATE_ALREADY_DEFINED_CODE = 40400;
085
086 /** Error message. */
087 public static final String PREDICATE_ALREADY_DEFINED_TEXT
088 = "predicate was already defined for this argument number: ";
089
090
091 /** Error code. */
092 public static final int MUST_BE_A_SUBJECT_VARIABLE_CODE = 40500;
093
094 /** Error message. */
095 public static final String MUST_BE_A_SUBJECT_VARIABLE_TEXT
096 = "a subject variable was expected here, but we found: ";
097
098
099 /** Error code. */
100 public static final int SUBJECT_VARIABLE_OCCURS_NOT_FREE_CODE = 40510;
101
102 /** Error message. */
103 public static final String SUBJECT_VARIABLE_OCCURS_NOT_FREE_TEXT
104 = "subject variable doesn't occur free in formula or term: ";
105
106
107 /** Error code. */
108 public static final int NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_CODE = 40520;
109
110 /** Error message. */
111 public static final String NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_TEXT
112 = "number of subject variables in definition not equal to number of free subject variables of formula or term";
113
114
115 /** Error code. */
116 public static final int IDENTITY_OPERATOR_MUST_BE_DEFINED_FIRST_CODE = 40530;
117
118 /** Error message. */
119 public static final String IDENTITY_OPERATOR_MUST_BE_DEFINED_FIRST_TEXT
120 = "the identity operator must be defined firstly before you can define a function constant";
121
122
123 /** Error code. */
124 public static final int DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_CODE = 40540;
125
126 /** Error message. */
127 public static final String DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_TEXT
128 = "a function definition must be an equal relation";
129
130
131 /** Error code. */
132 public static final int FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE = 40550;
133
134 /** Error message. */
135 public static final String FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT
136 = "first operand of equal relation must be the new function constant";
137
138
139 /** Error code. */
140 public static final int SECOND_OPERAND_MUST_BE_A_TERM_CODE = 40560;
141
142 /** Error message. */
143 public static final String SECOND_OPERAND_MUST_BE_A_TERM_TEXT
144 = "first operand of equal relation must be the new function constant";
145
146
147 /** Error code. */
148 public static final int MODULE_IMPORT_CHECK_FAILED_CODE = 11231;
149
150 /** Error message. */
151 public static final String MODULE_IMPORT_CHECK_FAILED_TEXT
152 = "import check failed: ";
153
154
155 /** Error code. */
156 public static final int PROPOSITION_FORMULA_MUST_NOT_BE_NULL_CODE = 37230;
157
158 /** Error message. */
159 public static final String PROPOSITION_FORMULA_MUST_NOT_BE_NULL_TEXT
160 = "proposition formula must not be null";
161
162
163 /** Error code. */
164 public static final int NODE_FORMULAS_MUST_BE_WELL_FORMED_CODE = 37250;
165
166 /** Error message. */
167 public static final String NODE_FORMULAS_MUST_BE_WELL_FORMED_TEXT
168 = "only nodes with well formed formulas can be checked";
169
170
171 /** Error code. */
172 public static final int NO_FORMAL_PROOF_FOUND_CODE = 37240;
173
174 /** Error message. */
175 public static final String NO_FORMAL_PROOF_FOUND_TEXT
176 = "no correct formal proof found";
177
178
179 }
|