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

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 …