OTTER Experiments in a System of Combinatory Logic

Thomas Jech

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 fin…