{
  "id": "2208.06879",
  "version": "v1",
  "published": "2022-08-14T16:31:04.000Z",
  "updated": "2022-08-14T16:31:04.000Z",
  "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"
  ],
  "comment": "12 pages, 7 appendices (data and proofs)",
  "categories": [
    "math.LO",
    "cs.AI",
    "cs.LO",
    "cs.MS",
    "math.HO"
  ],
  "abstract": "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.",
  "revisions": [
    {
      "version": "v1",
      "updated": "2022-08-14T16:31:04.000Z"
    }
  ],
  "analyses": {
    "subjects": [
      "03B35",
      "03B15",
      "03B45",
      "68T15",
      "68T27",
      "68T30",
      "03Bxx",
      "I.2.3",
      "F.4.1",
      "I.2.4"
    ],
    "keywords": [
      "higher-order automated theorem provers",
      "short proof",
      "curious inference",
      "exploration",
      "single shorthand notation"
    ],
    "note": {
      "typesetting": "TeX",
      "pages": 12,
      "language": "en",
      "license": "arXiv",
      "status": "editable"
    }
  }
}