Term Rewriting that Preserves Models in KR-Logic

In human proofs of mathematical problems, such as proofs in a group theory, term rewriting is usually used. When we consider Herbrand semantics for the first-order logic with constraints (FOLc), correct representation of evaluable terms cannot be obtained due to lack of representation power of the logic. In place of FOLc with Herbrand semantics, we use KRLc (KR-Logic with built-in constraints). We propose a class of term rewriting rules, and prove that they preserve the sets of all models in KR-Logic. Representation and computation by the rewriting rules in KR-Logic is well established in the space of KRLc. This paper opens a new method of logical problem solving, with KRLc being the representation space and ECLSN being the computation space. This theory integrates logical inference and functional rewriting under the broader concept of equivalent transformation.