EasyChair Publications
Search
Paper Information
Paper:Cezary Kaliszyk and Thomas Sternagel
Initial Experiments on Deriving a Complete HOL Simplification Set
Title:Initial Experiments on Deriving a Complete HOL Simplification Set
Authors:Cezary Kaliszyk and Thomas Sternagel
Keyphrases:completion, proof assistants, rewriting, higher order logic, simple type theory, hol light
Paper:
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.
Volume:Jasmin Christian Blanchette and Josef Urban (editors). PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving
Series:EPiC Series in Computing
Volume number:14
Pages:77-86
Editors:Jasmin Christian Blanchette and Josef Urban
Page views:14
Downloads:22
BibTeX entry:
@inproceedings{PxTP2013:Initial_Experiments_on_Deriving_a_Complete_HOL_Simplification_Set,
  author    = {Cezary Kaliszyk and Thomas Sternagel},
  title     = {Initial Experiments on Deriving a Complete HOL Simplification Set},
  booktitle = {PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving},
  editor    = {Jasmin Christian Blanchette and Josef Urban},
  series    = {EPiC Series in Computing},
  volume    = {14},
  pages     = {77-86},
  year      = {2013},
  publisher = {EasyChair},
  bibsource = {EasyChair, http://www.easychair.org},
  issn      = {2398-7340}}