Showing 1–12 of 12 results for author: Brown, C E

Symbolic Computation for All the Fun

Authors: Chad E. Brown, Mikoláš Janota, Mirek Olšák

Abstract: Motivated by the recent 10 million dollar AIMO challenge, this paper targets the problem of finding all functions conforming to a given specification. This is a popular problem at mathematical competitions and it brings about a number of challenges, primarily, synthesizing the possible solutions and proving that no other solutions exist. Often, there are infinitely many solutions and then the set… ▽ More Motivated by the recent 10 million dollar AIMO challenge, this paper targets the problem of finding all functions conforming to a given specification. This is a popular problem at mathematical competitions and it brings about a number of challenges, primarily, synthesizing the possible solutions and proving that no other solutions exist. Often, there are infinitely many solutions and then the set of solutions has to be captured symbolically. We propose an approach to solving this problem and evaluate it on a set of problems that appeared in mathematical competitions and olympics. △ Less

Submitted 23 June, 2024; v1 submitted 18 April, 2024; originally announced April 2024.

A Formal Proof of R(4,5)=25

Authors: Thibault Gauthier, Chad E. Brown

Abstract: In 1995, McKay and Radziszowski proved that the Ramsey number R(4,5) is equal to 25. Their proof relies on a combination of high-level arguments and computational steps. The authors have performed the computational parts of the proof with different implementations in order to reduce the possibility of an error in their programs. In this work, we prove this theorem in the interactive theorem prover… ▽ More In 1995, McKay and Radziszowski proved that the Ramsey number R(4,5) is equal to 25. Their proof relies on a combination of high-level arguments and computational steps. The authors have performed the computational parts of the proof with different implementations in order to reduce the possibility of an error in their programs. In this work, we prove this theorem in the interactive theorem prover HOL4 limiting the uncertainty to the small HOL4 kernel. Instead of verifying their algorithms directly, we rely on the HOL4 interface to MiniSat SAT to prove gluing lemmas. To reduce the number of such lemmas and thus make the computational part of the proof feasible, we implement a generalization algorithm. We verify that its output covers all the possible cases by implementing a custom SAT-solver extended with a graph isomorphism checker. △ Less

Submitted 12 June, 2024; v1 submitted 2 April, 2024; originally announced April 2024.

A Mathematical Benchmark for Inductive Theorem Provers

Authors: Thibault Gauthier, Chad E. Brown, Mikolas Janota, Josef Urban

Abstract: We present a benchmark of 29687 problems derived from the On-Line Encyclopedia of Integer Sequences (OEIS). Each problem expresses the equivalence of two syntactically different programs generating the same OEIS sequence. Such programs were conjectured by a learning-guided synthesis system using a language with loo** operators. The operators implement recursion, and thus many of the proofs requi… ▽ More We present a benchmark of 29687 problems derived from the On-Line Encyclopedia of Integer Sequences (OEIS). Each problem expresses the equivalence of two syntactically different programs generating the same OEIS sequence. Such programs were conjectured by a learning-guided synthesis system using a language with loo** operators. The operators implement recursion, and thus many of the proofs require induction on natural numbers. The benchmark contains problems of varying difficulty from a wide area of mathematical domains. We believe that these characteristics will make it an effective judge for the progress of inductive theorem provers in this domain for years to come. △ Less

Submitted 6 April, 2023; originally announced April 2023.

Lash 1.0 (System Description)

Authors: Chad E. Brown, Cezary Kaliszyk

Abstract: Lash is a higher-order automated theorem prover created as a fork of the theorem prover Satallax. The basic underlying calculus of Satallax is a ground tableau calculus whose rules only use shallow information about the terms and formulas taking part in the rule. Lash uses new, efficient C representations of vital structures and operations. Most importantly, Lash uses a C representation of (normal… ▽ More Lash is a higher-order automated theorem prover created as a fork of the theorem prover Satallax. The basic underlying calculus of Satallax is a ground tableau calculus whose rules only use shallow information about the terms and formulas taking part in the rule. Lash uses new, efficient C representations of vital structures and operations. Most importantly, Lash uses a C representation of (normal) terms with perfect sharing along with a C implementation of normalizing substitutions. We describe the ways in which Lash differs from Satallax and the performance improvement of Lash over Satallax when used with analogous flag settings. With a 10s timeout Lash outperforms Satallax on a collection TH0 problems from the TPTP. We conclude with ideas for continuing the development of Lash. △ Less

Submitted 13 May, 2022; originally announced May 2022.

Journal ref: IJCAR 2022 Conference Submission

Prolog Technology Reinforcement Learning Prover

Authors: Zsolt Zombori, Josef Urban, Chad E. Brown

Abstract: We present a reinforcement learning toolkit for experiments with guiding automated theorem proving in the connection calculus. The core of the toolkit is a compact and easy to extend Prolog-based automated theorem prover called plCoP. plCoP builds on the leanCoP Prolog implementation and adds learning-guided Monte-Carlo Tree Search as done in the rlCoP system. Other components include a Python int… ▽ More We present a reinforcement learning toolkit for experiments with guiding automated theorem proving in the connection calculus. The core of the toolkit is a compact and easy to extend Prolog-based automated theorem prover called plCoP. plCoP builds on the leanCoP Prolog implementation and adds learning-guided Monte-Carlo Tree Search as done in the rlCoP system. Other components include a Python interface to plCoP and machine learners, and an external proof checker that verifies the validity of plCoP proofs. The toolkit is evaluated on two benchmarks and we demonstrate its extendability by two additions: (1) guidance is extended to reduction steps and (2) the standard leanCoP calculus is extended with rewrite steps and their learned guidance. We argue that the Prolog setting is suitable for combining statistical and symbolic learning methods. The complete toolkit is publicly released. △ Less

Submitted 15 April, 2020; originally announced April 2020.

Self-Learned Formula Synthesis in Set Theory

Authors: Chad E. Brown, Thibault Gauthier

Abstract: A reinforcement learning algorithm accomplishes the task of synthesizing a set-theoretical formula that evaluates to given truth values for given assignments. A reinforcement learning algorithm accomplishes the task of synthesizing a set-theoretical formula that evaluates to given truth values for given assignments. △ Less

Submitted 3 December, 2019; originally announced December 2019.

Can Neural Networks Learn Symbolic Rewriting?

Authors: Bartosz Piotrowski, Josef Urban, Chad E. Brown, Cezary Kaliszyk

Abstract: This work investigates if the current neural architectures are adequate for learning symbolic rewriting. Two kinds of data sets are proposed for this research -- one based on automated proofs and the other being a synthetic set of polynomial terms. The experiments with use of the current neural machine translation models are performed and its results are discussed. Ideas for extending this line of… ▽ More This work investigates if the current neural architectures are adequate for learning symbolic rewriting. Two kinds of data sets are proposed for this research -- one based on automated proofs and the other being a synthetic set of polynomial terms. The experiments with use of the current neural machine translation models are performed and its results are discussed. Ideas for extending this line of research are proposed, and its relevance is motivated. △ Less

Submitted 26 May, 2020; v1 submitted 7 November, 2019; originally announced November 2019.

A Tale of Two Set Theories

Authors: Chad E. Brown, Karol Pąk

Abstract: We describe the relationship between two versions of Tarski-Grothendieck set theory: the first-order set theory of Mizar and the higher-order set theory of Egal. We show how certain higher-order terms and propositions in Egal have equivalent first-order presentations. We then prove Tarski's Axiom A (an axiom in Mizar) in Egal and construct a Grothendieck Universe operator (a primitive with axioms… ▽ More We describe the relationship between two versions of Tarski-Grothendieck set theory: the first-order set theory of Mizar and the higher-order set theory of Egal. We show how certain higher-order terms and propositions in Egal have equivalent first-order presentations. We then prove Tarski's Axiom A (an axiom in Mizar) in Egal and construct a Grothendieck Universe operator (a primitive with axioms in Egal) in Mizar. △ Less

Submitted 18 July, 2019; originally announced July 2019.

Cantor-Bernstein implies Excluded Middle

Authors: Cécilia Pradic, Chad E. Brown

Abstract: We prove in constructive logic that the statement of the Cantor-Bernstein theorem implies excluded middle. This establishes that the Cantor-Bernstein theorem can only be proven assuming the full power of classical logic. The key ingredient is a theorem of Martín Escardó stating that quantification over a particular subset of the Cantor space $2^{\mathbb{N}}$, the so-called one-point compactifica… ▽ More We prove in constructive logic that the statement of the Cantor-Bernstein theorem implies excluded middle. This establishes that the Cantor-Bernstein theorem can only be proven assuming the full power of classical logic. The key ingredient is a theorem of Martín Escardó stating that quantification over a particular subset of the Cantor space $2^{\mathbb{N}}$, the so-called one-point compactification of $\mathbb{N}$, preserves decidable predicates. △ Less

Submitted 15 August, 2022; v1 submitted 19 April, 2019; originally announced April 2019.

Comments: 6pp / update: corrected an error in the intro wrt applicability of Thm 1, typos, added a couple of acks and a ref

MSC Class: 03F55

GRUNGE: A Grand Unified ATP Challenge

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

Abstract: This paper describes a large set of related theorem proving problems obtained by translating theorems from the HOL4 standard library into multiple logical formalisms. The formalisms are in higher-order logic (with and without type variables) and first-order logic (possibly with multiple types, and possibly with type variables). The resultant problem sets allow us to run automated theorem provers t… ▽ More This paper describes a large set of related theorem proving problems obtained by translating theorems from the HOL4 standard library into multiple logical formalisms. The formalisms are in higher-order logic (with and without type variables) and first-order logic (possibly with multiple types, and possibly with type variables). The resultant problem sets allow us to run automated theorem provers that support different logical formats on corresponding problems, and compare their performances. This also results in a new "grand unified" large theory benchmark that emulates the ITP/ATP hammer setting, where systems and metasystems can use multiple ATP formalisms in complementary ways, and jointly learn from the accumulated knowledge. △ Less

Submitted 19 November, 2019; v1 submitted 6 March, 2019; originally announced March 2019.

Comments: CADE 27 -- 27th International Conference on Automated Deduction

Analytic Tableaux for Simple Type Theory and its First-Order Fragment

Authors: Chad E. Brown, Gert Smolka

Abstract: We study simple type theory with primitive equality (STT) and its first-order fragment EFO, which restricts equality and quantification to base types but retains lambda abstraction and higher-order variables. As deductive system we employ a cut-free tableau calculus. We consider completeness, compactness, and existence of countable models. We prove these properties for STT with respect to Henkin… ▽ More We study simple type theory with primitive equality (STT) and its first-order fragment EFO, which restricts equality and quantification to base types but retains lambda abstraction and higher-order variables. As deductive system we employ a cut-free tableau calculus. We consider completeness, compactness, and existence of countable models. We prove these properties for STT with respect to Henkin models and for EFO with respect to standard models. We also show that the tableau system yields a decision procedure for three EFO fragments. △ Less

Submitted 22 June, 2010; v1 submitted 12 April, 2010; originally announced April 2010.

ACM Class: 03B15

Journal ref: Logical Methods in Computer Science, Volume 6, Issue 2 (June 23, 2010) lmcs:1169

Cut-Simulation and Impredicativity

Authors: Christoph Benzmueller, Chad E. Brown, Michael Kohlhase

Abstract: We investigate cut-elimination and cut-simulation in impredicative (higher-order) logics. We illustrate that adding simple axioms such as Leibniz equations to a calculus for an impredicative logic -- in our case a sequent calculus for classical type theory -- is like adding cut. The phenomenon equally applies to prominent axioms like Boolean- and functional extensionality, induction, choice, and… ▽ More We investigate cut-elimination and cut-simulation in impredicative (higher-order) logics. We illustrate that adding simple axioms such as Leibniz equations to a calculus for an impredicative logic -- in our case a sequent calculus for classical type theory -- is like adding cut. The phenomenon equally applies to prominent axioms like Boolean- and functional extensionality, induction, choice, and description. This calls for the development of calculi where these principles are built-in instead of being treated axiomatically. △ Less

Submitted 2 March, 2009; v1 submitted 30 January, 2009; originally announced February 2009.

Comments: 21 pages

ACM Class: F.4.1; I.2.3

Journal ref: Logical Methods in Computer Science, Volume 5, Issue 1 (March 3, 2009) lmcs:1144