Generic Automatic Proof Tools
Logic in Computer Science
2016-08-31 v1
Abstract
This book chapter establishes connections between the interactive proof tool Isabelle and classical tableau and resolution technology. Isabelle's classical reasoner is described and demonstrated by an extended case study: the Church-Rosser theorem for combinators. Compared with other interactive theorem provers, Isabelle's classical reasoner achieves a high degree of automation.
Cite
@article{arxiv.cs/9711106,
title = {Generic Automatic Proof Tools},
author = {Lawrence C. Paulson},
journal= {arXiv preprint arXiv:cs/9711106},
year = {2016}
}