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.

Abstract

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

License

BSD License

Topics

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. https://doi.org/10.48550/ARXIV.2208.06879

Session Boolos_Curious_Inference_Automated