Options
Who finds the short proof? : Searching for Wormholes in Proof-Space
Benzmüller, Christoph (2025): Who finds the short proof? : Searching for Wormholes in Proof-Space, in: Bamberg: Otto-Friedrich-Universität, S. 6.
Faculty/Chair:
Author:
Publisher Information:
Year of publication:
2025
Pages:
Source/Other editions:
Dagstuhl Reports : Dokumentationen zu Dagstuhl-Seminaren und Dagstuhl-Perspektiven-Workshops, Wadern: Schloss Dagstuhl, 2024, Jg. 13, Nr. 10, S. 6, ISSN: 2192-5283
Year of first publication:
2024
Language:
English
Abstract:
In my talk I presented recently published results that had not been communicated at conferences or workshops before: 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
GND Keywords:
Automatisches Beweisverfahren
Keywords:
short proof
DDC Classification:
RVK Classification:
Type:
Article
Activation date:
May 30, 2025
Permalink
https://fis.uni-bamberg.de/handle/uniba/108389