Automation of Boolos' Curious Inference in Isabelle/HOL

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

December 5, 2022

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


Boolos’ Curious Inference is automated in Isabelle/HOL after interactive speculation of a suitable shorthand notation (one or two definitions).


BSD License


Related publications

  • Benzmüller, C., Fuenmayor, D., Steen, A., & Sutcliffe, G. (2022). Who Finds the Short Proof? An Exploration of Variants of Boolos' Curious Inference using Higher-order Automated Theorem Provers. ArXiv.

Session Boolos_Curious_Inference_Automated