A Constructor-Based EI-Model Semantics ofEI-CTRS  

作　　者：王怀民 陈火旺 

出　　处：《Journal of Computer Science & Technology》1995年第1期85-95,共11页计算机科学技术学报（英文版）

摘　　要：This paper investigates the semantics of conditional term rewriting systemswith negation (denoted by EI-CTRS), called constructor-based EI-model se-mantics. The introduction of '≠' in EI-CTRS make EI-CTRS more difficult tostudy. This is in part because of a failure of EI-CTRS to guarantee that thereexist least Herbrand models in classical logical point of views. The key idea ofEI-model is to explain that 't ≠ s' means that the two concepts representedby t and s respectively actually belong to distinguished basic concepts repre-sented by two constructor-ground terms. We define the concept of EI-model,and show that there exist least Herbrand ELmodels for EI-satisfiable EI-CTRS.From algebraic and logic point of view, we show that there are very strong rea-sons for regarding the least Herbrand EI-models as the intended semantics ofEI-CTRS. According to fixpoint theory, we develop a method to construct leastHerbrand EI-models in a bottom-up manner. Moreover, we discuss soundnessand completeness of EI-rewrite for EI-model semantics.This paper investigates the semantics of conditional term rewriting systemswith negation (denoted by EI-CTRS), called constructor-based EI-model se-mantics. The introduction of '≠' in EI-CTRS make EI-CTRS more difficult tostudy. This is in part because of a failure of EI-CTRS to guarantee that thereexist least Herbrand models in classical logical point of views. The key idea ofEI-model is to explain that 't ≠ s' means that the two concepts representedby t and s respectively actually belong to distinguished basic concepts repre-sented by two constructor-ground terms. We define the concept of EI-model,and show that there exist least Herbrand ELmodels for EI-satisfiable EI-CTRS.From algebraic and logic point of view, we show that there are very strong rea-sons for regarding the least Herbrand EI-models as the intended semantics ofEI-CTRS. According to fixpoint theory, we develop a method to construct leastHerbrand EI-models in a bottom-up manner. Moreover, we discuss soundnessand completeness of EI-rewrite for EI-model semantics.

关 键 词：Conditional term rewriting model semantics NEGATION FIXPOINT CONSTRUCTOR 

分 类 号：TP301.6[自动化与计算机技术—计算机系统结构]