OTTER experiments in a system of combinatory logic

DOI10.1007/BF00881715zbMath0822.03011arXivmath/9409201WikidataQ115059466 ScholiaQ115059466MaRDI QIDQ1893130

Thomas J. Jech

Publication date: 3 July 1995

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/math/9409201

zbMATH Keywords

TRCillative combinatory logicexperiments involving the automated theorem-proving program OTTER

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Software, source code, etc. for problems pertaining to mathematical logic and foundations (03-04)

Related Items (2)

System description generating models by SEM ⋮ Some results on combinators in the system TRC

Uses Software

• Unnamed Item

Cites Work

• Automated discovery of new axiomatizations of the left group and right group calculi
• Single axioms for groups
• Combinatory logic. With two sections by William Craig.
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Systems of combinatory logic related to Quine's `New Foundations'
• The kernel strategy and its use for the study of combinatory logic
• Single axioms for groups and abelian groups with various operations

This page was built for publication: OTTER experiments in a system of combinatory logic