4 Search Results for "Brown, Chad E."

Document
DOI: 10.4230/LIPIcs.ITP.2023.9
Automated Theorem Proving for Metamath

Authors: Mario Carneiro, Chad E. Brown, and Josef Urban

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
Metamath is a proof assistant that keeps surprising outsiders by its combination of a very minimalist design with a large library of advanced results, ranking high on the Freek Wiedijk’s 100 list. In this work, we develop several translations of the Metamath logic and its large set-theoretical library into higher-order and first-order TPTP formats for automated theorem provers (ATPs). We show that state-of-the-art ATPs can prove 68% of the Metamath problems automatically when using the premises that were used in the human-written Metamath proofs. Finally, we add proof reconstruction and premise selection methods and combine the components into the first hammer system for Metamath.
Cite as

Mario Carneiro, Chad E. Brown, and Josef Urban. Automated Theorem Proving for Metamath. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 9:1-9:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{carneiro_et_al:LIPIcs.ITP.2023.9,
  author =	{Carneiro, Mario and Brown, Chad E. and Urban, Josef},
  title =	{{Automated Theorem Proving for Metamath}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{9:1--9:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.9},
  URN =		{urn:nbn:de:0030-drops-183846},
  doi =		{10.4230/LIPIcs.ITP.2023.9},
  annote =	{Keywords: Metamath, Automated theorem proving, Interactive theorem proving, Formal proof assistants, proof discovery}
}
Document
DOI: 10.4230/LIPIcs.ITP.2023.19
MizAR 60 for Mizar 50

Authors: Jan Jakubův, Karel Chvalovský, Zarathustra Goertzel, Cezary Kaliszyk, Mirek Olšák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, and Josef Urban

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
As a present to Mizar on its 50th anniversary, we develop an AI/TP system that automatically proves about 60% of the Mizar theorems in the hammer setting. We also automatically prove 75% of the Mizar theorems when the automated provers are helped by using only the premises used in the human-written Mizar proofs. We describe the methods and large-scale experiments leading to these results. This includes in particular the E and Vampire provers, their ENIGMA and Deepire learning modifications, a number of learning-based premise selection methods, and the incremental loop that interleaves growing a corpus of millions of ATP proofs with training increasingly strong AI/TP systems on them. We also present a selection of Mizar problems that were proved automatically.
Cite as

Jan Jakubův, Karel Chvalovský, Zarathustra Goertzel, Cezary Kaliszyk, Mirek Olšák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, and Josef Urban. MizAR 60 for Mizar 50. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 19:1-19:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{jakubuv_et_al:LIPIcs.ITP.2023.19,
  author =	{Jakub\r{u}v, Jan and Chvalovsk\'{y}, Karel and Goertzel, Zarathustra and Kaliszyk, Cezary and Ol\v{s}\'{a}k, Mirek and Piotrowski, Bartosz and Schulz, Stephan and Suda, Martin and Urban, Josef},
  title =	{{MizAR 60 for Mizar 50}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{19:1--19:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.19},
  URN =		{urn:nbn:de:0030-drops-183942},
  doi =		{10.4230/LIPIcs.ITP.2023.19},
  annote =	{Keywords: Mizar, ENIGMA, Automated Reasoning, Machine Learning}
}
Document
DOI: 10.4230/OASIcs.FMBC.2022.4
Proofgold: Blockchain for Formal Methods

Authors: Chad E. Brown, Cezary Kaliszyk, Thibault Gauthier, and Josef Urban

Published in: OASIcs, Volume 105, 4th International Workshop on Formal Methods for Blockchains (FMBC 2022)

Abstract
Proofgold is a peer to peer cryptocurrency making use of formal logic. Users can publish theories and then develop a theory by publishing documents with definitions, conjectures and proofs. The blockchain records the theories and their state of development (e.g., which theorems have been proven and when). Two of the main theories are a form of classical set theory (for formalizing mathematics) and an intuitionistic theory of higher-order abstract syntax (for reasoning about syntax with binders). We have also significantly modified the open source Proofgold Core client software to create a faster, more stable and more efficient client, Proofgold Lava. Two important changes are the cryptography code and the database code, and we discuss these improvements. We also discuss how the Proofgold network can be used to support large formalization efforts.
Cite as

Chad E. Brown, Cezary Kaliszyk, Thibault Gauthier, and Josef Urban. Proofgold: Blockchain for Formal Methods. In 4th International Workshop on Formal Methods for Blockchains (FMBC 2022). Open Access Series in Informatics (OASIcs), Volume 105, pp. 4:1-4:15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{brown_et_al:OASIcs.FMBC.2022.4,
  author =	{Brown, Chad E. and Kaliszyk, Cezary and Gauthier, Thibault and Urban, Josef},
  title =	{{Proofgold: Blockchain for Formal Methods}},
  booktitle =	{4th International Workshop on Formal Methods for Blockchains (FMBC 2022)},
  pages =	{4:1--4:15},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-250-1},
  ISSN =	{2190-6807},
  year =	{2022},
  volume =	{105},
  editor =	{Dargaye, Zaynah and Schneidewind, Clara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2022.4},
  URN =		{urn:nbn:de:0030-drops-171851},
  doi =		{10.4230/OASIcs.FMBC.2022.4},
  annote =	{Keywords: Formal logic, Blockchain, Proofgold}
}
Document
DOI: 10.4230/LIPIcs.ITP.2019.9
Higher-Order Tarski Grothendieck as a Foundation for Formal Proof

Authors: Chad E. Brown, Cezary Kaliszyk, and Karol Pąk

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract
We formally introduce a foundation for computer verified proofs based on higher-order Tarski-Grothendieck set theory. We show that this theory has a model if a 2-inaccessible cardinal exists. This assumption is the same as the one needed for a model of plain Tarski-Grothendieck set theory. The foundation allows the co-existence of proofs based on two major competing foundations for formal proofs: higher-order logic and TG set theory. We align two co-existing Isabelle libraries, Isabelle/HOL and Isabelle/Mizar, in a single foundation in the Isabelle logical framework. We do this by defining isomorphisms between the basic concepts, including integers, functions, lists, and algebraic structures that preserve the important operations. With this we can transfer theorems proved in higher-order logic to TG set theory and vice versa. We practically show this by formally transferring Lagrange’s four-square theorem, Fermat 3-4, and other theorems between the foundations in the Isabelle framework.
Cite as

Chad E. Brown, Cezary Kaliszyk, and Karol Pąk. Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 9:1-9:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{brown_et_al:LIPIcs.ITP.2019.9,
  author =	{Brown, Chad E. and Kaliszyk, Cezary and P\k{a}k, Karol},
  title =	{{Higher-Order Tarski Grothendieck as a Foundation for Formal Proof}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{9:1--9:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.9},
  URN =		{urn:nbn:de:0030-drops-110643},
  doi =		{10.4230/LIPIcs.ITP.2019.9},
  annote =	{Keywords: model, higher-order, Tarski Grothendieck, proof foundation}
}
  • Refine by Author
  • 3 Brown, Chad E.
  • 3 Kaliszyk, Cezary
  • 3 Urban, Josef
  • 1 Carneiro, Mario
  • 1 Chvalovský, Karel
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Automated reasoning
  • 2 Theory of computation → Logic and verification
  • 1 Theory of computation → Higher order logic
  • 1 Theory of computation → Interactive proof systems

  • Refine by Keyword
  • 1 Automated Reasoning
  • 1 Automated theorem proving
  • 1 Blockchain
  • 1 ENIGMA
  • 1 Formal logic
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 2 2023
  • 1 2019
  • 1 2022

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact