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

Cite

× 
@article{Boolos_Curious_Inference_Automated-AFP,
  author  = {Christoph Benzmüller and David Fuenmayor and Alexander Steen and Geoff Sutcliffe},
  title   = {Automation of Boolos' Curious Inference in Isabelle/HOL},
  journal = {Archive of Formal Proofs},
  month   = {December},
  year    = {2022},
  note    = {\url{https://isa-afp.org/entries/Boolos_Curious_Inference_Automated.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: