Who Finds the Short Proof?

, , &
Logic Journal of the IGPL (forthcoming)
  Copy   BIBTEX

Abstract

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.

Categories

Keywords

Reprint years

DOI

10.1093/jigpal/jzac082

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,261

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

The curious inference of Boolos in MIZAR and OMEGA.Christoph Benzmüller & Chad Brown - 2007 - In Matuszewski Roman & Zalewska Anna (eds.), From Insight to Proof -- Festschrift in Honour of Andrzej Trybulec. The University of Bialystok, Polen. pp. 299-388.
Higher-Order Automated Theorem Provers.Benzmüller Christoph - 2015 - In David Delahaye & Bruno Woltzenlogel Paleo (eds.), All About Proofs, Proof for All. College Publications. pp. 171-214.
Omega.Christoph Benzmüller, Armin Fiedler, Andreas Meier, Martin Pollet & Jörg Siekmann - 2006 - In Freek Wiedijk (ed.), The Seventeen Provers of the World. Springer. pp. 127-141.
All About Proofs, Proof for All.David Delahaye & Bruno Woltzenlogel Paleo (eds.) - 2015 - College Publications.
Types, Tableaus and Gödel’s God in Isabelle/HOL.Fuenmayor David & Benzmüller Christoph - forthcoming - Archive of Formal Proofs.
Integrating TPS and OMEGA.Christoph Benzmüller, Matt Bishop & Volker Sorge - 1999 - Journal of Universal Computer Science 5 (3):188-207.
The Virtues of Automated Theorem Proving in Metaphysics --- A Case Study: E. J. Lowe's Modal Ontological Argument.Fuenmayor David, Benzmüller Christoph, Steen Alexander & Wsinieswki Max - 2017 - In David Fuenmayor, Christoph Benzmüller, Alexander Steen & Max Wsinieswki (eds.), The 2nd World Congress on Logic and Religion -- Book of Abstracts. Instytut Filozofii Uniwersytetu Warszawskiego.
Formalization, Mechanization and Automation of Gödel’s Proof of God’s Existence.Benzmüller Christoph & Woltzenlogel Paleo Bruno - 2013
Combined reasoning by automated cooperation.Christoph Benzmüller, Volker Sorge, Mateja Jamnik & Manfred Kerber - 2008 - Journal of Applied Logic 6 (3):318-342.
Analysis of an Ontological Proof Proposed by Leibniz.Matthias Bentert, Christoph Benzmüller, David Streit & Bruno Woltzenlogel Paleo - 2016 - In Charles Tandy (ed.), Death and Anti-Death, Volume 14: Four Decades After Michael Polanyi, Three Centuries After G.W. Leibniz. Ria University Press.
Proof Development in OMEGA: The Irrationality of Square Root of 2.Siekmann Jörg, Benzmüller Christoph, Fiedler Armin, Meier Andreas, Normann Immanuel & Pollet Martin - 2003 - In Fairouz Kamareddine (ed.), Thirty Five Years of Automating Mathematics. Kluwer Academic Publishers. pp. 271-314.
Computer supported mathematics with Ωmega.Jörg Siekmann, Christoph Benzmüller & Serge Autexier - 2006 - Journal of Applied Logic 4 (4):533-559.
Assertion-level Proof Representation with Under-Specification.Serge Autexier, Christoph Benzmüller, Armin Fiedler, Helmut Horacek & Bao Quoc Vo - 2004 - Electronic Notes in Theoretical Computer Science 93:5-23.
A short proof of reny's existence theorem for payoff secure games.Pavlo Prokopovych - unknown
Experiments in Computational Metaphysics: Gödel’s Proof of God’s Existence.Christoph Benzmüller & Bruno Woltzenlogel Paleo - 2017 - Savijnanam: Scientific Exploration for a Spiritual Paradigm. Journal of the Bhaktivedanta Institute 9:43-57.

Analytics

Added to PP
2023-01-27

Downloads
3 (#1,715,951)

6 months
2 (#1,206,802)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Christoph Benzmueller
Freie Universität Berlin

Citations of this work

No citations found.

Add more citations

References found in this work

A formulation of the simple theory of types.Alonzo Church - 1940 - Journal of Symbolic Logic 5 (2):56-68.
A curious inference.George Boolos - 1987 - Journal of Philosophical Logic 16 (1):1 - 12.
Don't eliminate cut.George Boolos - 1984 - Journal of Philosophical Logic 13 (4):373 - 378.
The Higher-Order Prover LEO-II.Christoph Benzmüller, Nik Sultana, Lawrence C. Paulson & Frank Theiß - 2015 - Journal of Automated Reasoning 55 (4):389-404.
The logic languages of the TPTP world.Geoff Sutcliffe - 2023 - Logic Journal of the IGPL 31 (6):1153-1169.

View all 6 references / Add more references