We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

math.LO
< prev | next >
new | recent | 2208

Change to browse by:

cs
cs.AI
cs.LO
math
math.HO

References & Citations

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo

Mathematics > Logic

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

Authors: Christoph Benzmüller, David Fuenmayor, Alexander Steen, Geoff Sutcliffe
(Submitted on 14 Aug 2022 (v1), last revised 1 Dec 2022 (this version, v3))
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.
Comments: 11 pages, 7 appendices (data, proofs and links to proofs); to appear in the Logic Journal of the IGPL
Subjects: Logic (math.LO); Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO); History and Overview (math.HO)
MSC classes: 03B35, 03B10, 03B16, 68T27, 68T30, 03A05, 00A30
ACM classes: F.4.1; I.2.3; I.2.4
DOI: 10.1093/jigpal/jzac082
Cite as: arXiv:2208.06879 [math.LO]
  (or arXiv:2208.06879v3 [math.LO] for this version)

Submission history

From: Christoph Benzmüller [view email]
[v1] Sun, 14 Aug 2022 16:31:04 GMT (472kb,D)
[v2] Mon, 22 Aug 2022 14:30:23 GMT (472kb,D)
[v3] Thu, 1 Dec 2022 17:11:08 GMT (408kb,D)
Which authors of this paper are endorsers? | Disable MathJax (What is MathJax?)

Link back to: arXiv, form interface, contact.