Rewriting and Well-Definedness within a Proof System

TL;DR

This paper develops a theoretical foundation for integrating rewriting with a deductive proof system that manages well-definedness, enabling more robust automated theorem proving, exemplified through an implementation in Event-B.

Contribution

It introduces a formal framework for rewriting within proof systems that handle partial functions and ill-defined terms, enhancing proof automation.

Findings

Provides definitions and theorems for rewriting with well-definedness

Lays the groundwork for an extensible rewriting-based prover

Implementation demonstrated in Event-B

Abstract

Term rewriting has a significant presence in various areas, not least in automated theorem proving where it is used as a proof technique. Many theorem provers employ specialised proof tactics for rewriting. This results in an interleaving between deduction and computation (i.e., rewriting) steps. If the logic of reasoning supports partial functions, it is necessary that rewriting copes with potentially ill-defined terms. In this paper, we provide a basis for integrating rewriting with a deductive proof system that deals with well-definedness. The definitions and theorems presented in this paper are the theoretical foundations for an extensible rewriting-based prover that has been implemented for the set theoretical formalism Event-B.