Who Finds the Short Proof? An Exploration of Variants of Boolos' Curious Inference using Higher-order Automated Theorem Provers
This work advances automated theorem proving by enabling full proof automation for complex logical examples, benefiting researchers in formal methods and AI.
The paper tackled the automation of Boolos' Curious Inference using higher-order automated theorem provers, achieving short proofs with only minimal manual shorthand notations and automatic discovery of higher-order lemmas.
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.