Logical Approach to Theorem Proving with Term Rewriting on KR-logic

Term rewriting is often used for proving theorems. To mechanizing such a proof method with computation correctness guaranteed strictly, we follow LPSF, which is a general framework for generating logical problem solution methods. In place of the first-order logic, we use KR-logic, which has function variables, for correct formalization. By repeating (1) specialization by a substitution for usual variables, and (2) application of an already derived rewriting rule, we can generate a term rewriting rule from the resulting equational clause. The obtained term rewriting rules are proved to be equivalent transformation rules. The correctness of the computation results is guaranteed. This theory shows that LPSF integrates logical inference and functional rewriting under the broader concept of equivalent transformation.