20 citations · 86 across the 12 of their papers we have counts for
14 papers
Translating SUMO-K to Higher-Order Set Theory
Chad Brown, Adam Pease, Josef Urban
We describe a translation from a fragment of SUMO (SUMO-K) into higher-order set theory. The translation provides a formal semantics for portions of SUMO which are beyond first-ord…
A Mathematical Benchmark for Inductive Theorem Provers
Thibault Gauthier, Chad E. Brown, Mikolas Janota +1
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 pr…
Lash 1.0 (System Description)
Chad E. Brown, Cezary Kaliszyk
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…
Prolog Technology Reinforcement Learning Prover
Zsolt Zombori, Josef Urban, Chad E. Brown
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 exte…
Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar
Qingxiang Wang, Chad Brown, Cezary Kaliszyk +1
In this paper we share several experiments trying to automatically translate informal mathematics into formal mathematics. In our context informal mathematics refers to human-writt…
Self-Learned Formula Synthesis in Set Theory
Chad E. Brown, Thibault Gauthier
A reinforcement learning algorithm accomplishes the task of synthesizing a set-theoretical formula that evaluates to given truth values for given assignments.