Generic Automatic Proof Tools
<|reference_start|>Generic Automatic Proof Tools: 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.<|reference_end|>
@article{paulson2001generic,
    title={Generic Automatic Proof Tools},
    author={Lawrence C. Paulson},
    journal={published in Robert Veroff (editor), Automated Reasoning and its
  Applications: Essays in Honor of Larry Wos (MIT Press, 1997), 23-47},
    year={2001},
    archivePrefix={arXiv},
    eprint={cs/9711106},
    primaryClass={cs.LO}
}