arXiv Analytics

Sign in

arXiv:2208.06879 [math.LO]AbstractReferencesReviewsResources

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

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

Published 2022-08-14Version 1

We report on an exploration of variants of Boolos' curious inference using higher-order automated theorem provers (ATPs). Surprisingly, only a single shorthand notation still had to be provided by hand. All higher-order lemmas required for obtaining short proof are automatically discovered by the computer. Given the observations and suggestions in this paper, full proof automation of Boolos' example on the speedup of proof lengths, and related examples, now seems to be within reach for higher-order ATPs.

Comments: 12 pages, 7 appendices (data and proofs)
Categories: math.LO, cs.AI, cs.LO, cs.MS, math.HO
Related articles: Most relevant | Search more
arXiv:math/9204206 [math.LO] (Published 1992-04-15)
A short proof of the irreflexivity conjecture
arXiv:1012.4370 [math.LO] (Published 2010-12-20, updated 2011-03-18)
On many-sorted $ω$-categorical theories
arXiv:0810.4705 [math.LO] (Published 2008-10-26, updated 2010-01-02)
Iteratively algebraic orders

Links

Toolbox