OTTER Experiments in a System of Combinatory Logic
Logic
2008-02-03 v1
Abstract
This paper describes some experiments involving the automated theorem-proving program OTTER in the system TRC of illative combinatory logic. We show how OTTER can be steered to find a contradiction in an inconsistent variant of TRC, and present some experimentally discovered identities in TRC.
Cite
@article{arxiv.math/9409201,
title = {OTTER Experiments in a System of Combinatory Logic},
author = {Thomas Jech},
journal= {arXiv preprint arXiv:math/9409201},
year = {2008}
}