{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:47:36Z","timestamp":1725486456861},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.29007\/95qb","type":"proceedings-article","created":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T17:59:05Z","timestamp":1516730345000},"page":"77-66","source":"Crossref","is-referenced-by-count":0,"title":["Initial Experiments on Deriving a Complete HOL Simplification Set"],"prefix":"10.29007","volume":"14","author":[{"given":"Cezary","family":"Kaliszyk","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Sternagel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"11545","event":{"name":"PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T18:00:09Z","timestamp":1516730409000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/h6b"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/95qb","relation":{},"ISSN":["2398-7340"],"issn-type":[{"type":"print","value":"2398-7340"}],"subject":[]}}