### Initial Experiments on Deriving a Complete HOL Simplification Set

Cezary Kaliszyk and Thomas SternagelProceedings of the 3rd International Workshop on Proof Exchange for Theorem Proving (PxTP 2013), EasyChair Proceedings in Computing 14, pp. 77 – 86, 2013.

### Abstract

Rewriting is a common functionality in proof assistants, that allows to simplify theorems and goals. The set of equations to use in a rewrite step has to be manually specified, and therefore often includes rules which may lead to non-termination. Even in the case of termination another desirable property of a simplification set would be confluence. A well-known technique from rewriting to transform a terminating system into a terminating and confluent one is completion. But the sets of equations we find in the context of proof assistants are typically huge and most state-of-the-art completion tools only work on relatively small problems. In this paper we describe our initial experiments with the aim to close the gap and use rewriting to compute a complete first-order simplification set for a HOL-based proof assistant fully automatically.

### BibTeX

@inproceedings{CKTS-PxTP13, author = "Cezary Kaliszyk and Thomas Sternagel", title = "Initial Experiments on Deriving a Complete {HOL} Simplification Set", booktitle = "Proceedings of the 3rd International Workshop on Proof Exchange for Theorem Proving", series = "EasyChair Proceedings in Computing", volume = 14, pages = "77--86", year = 2013 }