Who Finds the Short Proof? An Exploration of Variants of Boolos' Curious Inference using Higher-order Automated Theorem Provers

DOI10.1093/JIGPAL/JZAC082arXiv2208.06879WikidataQ126392300 ScholiaQ126392300MaRDI QIDQ6407822FDOQ6407822

Authors: Christoph Benzmüller, David Fuenmayor, Alexander Steen, Geoff Sutcliffe 

Publication date: 14 August 2022

Abstract: This paper reports on an exploration of Boolos' Curious Inference, using higher-order automated theorem provers (ATPs). Surprisingly, only suitable shorthand notations had to be provided by hand for ATPs to find a short proof. The higher-order lemmas required for constructing a short proof are automatically discovered by the ATPs. Given the observations and suggestions in this paper, full proof automation of Boolos' and related examples now seems to be within reach of higher-order ATPs.

Mathematics Subject Classification ID

Knowledge representation (68T30) Philosophical and critical aspects of logic and foundations (03A05) Logic in artificial intelligence (68T27) Philosophy of mathematics (00A30) Classical first-order logic (03B10) Higher-order logic (03B16) Mechanization of proofs and logical operations (03B35)

This page was built for publication: Who Finds the Short Proof? An Exploration of Variants of Boolos' Curious Inference using Higher-order Automated Theorem Provers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6407822)