A Constructor-Based EI-Model Semantics of EI-CTRS

摘要

This paper investigates the semantics of conditional term rewriting systems with negation (denoted by EI-CTRS), called constructor-based EI-model semantics. The introduction of "≠" in EI-CTRS make EI-CTRS more difficult to study. This is in part because of a failure of EI-CTRS to guarantee that there exist least Herbrand models in classical logical point of views. The key idea of EI-model is to explain that "t ≠ s" means that the two concepts represented by t and s respectively actually belong to distinguished basic concepts represented by two constructor-ground terms. We define the concept of EI-model, and show that there exist least Herbrand EI-models for EI-satisfiable EI-CTRS. Prom algebraic and logic point of view, we show that there are very strong reasons for regarding the least Herbrand EI-models as the intended semantics of EI-CTRS. According to fixpoint theory, we develop a method to construct least Herbrand EI-models in a bottom-up manner. Moreover, we discuss soundness and completeness of EI-rewrite for EI-model semantics.