中文

OTTER Experiments in a System of Combinatory Logic

逻辑 2008-02-03 v1

摘要

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.

引用

@article{arxiv.math/9409201,
  title  = {OTTER Experiments in a System of Combinatory Logic},
  author = {Thomas Jech},
  journal= {arXiv preprint arXiv:math/9409201},
  year   = {2008}
}