Handling of incompatible pieces of knowledge and of incompatible reasoning rules is an important issue in knowledge engineering. Such knowledge and rules when formalized form an inconsistent theory. From the point of view of classical logic, inconsistent theories do not make any sense. Anything is provable in them and they do not have any models; therefore they lack any semantics. The report presents techniques for a more subtle study of semantics of inconsistent theories, while keeping the syntax, logical axioms and inference rules of first order predicate logic. Partial models, n-th partial models and a 'semantic' measure of consistency are defined. In the main theorem of the report it is proved that partial models are suitable approximations of classical models. This theorem is a new version of Herbrand's theorem, a basic theorem in automated theorem proving. Generalized semantic trees ordered according to substitution depth are defined and used to give an equivalent condition for the existent of an n-th partial model of a set of clauses. (Copyright (c) 1990 by Faculty of Technical Mathematics and Informatics, Delft, The Netherlands.)
展开▼
