20 citations · 32 across the 4 of their papers we have counts for
7 papers · 1 filter
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…
A Tale of Two Set Theories
Chad E. Brown, Karol Pąk
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 certai…
GRUNGE: A Grand Unified ATP Challenge
Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk +2
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 formalism…
Internal Guidance for Satallax
Michael Färber, Chad Brown
We propose a new internal guidance method for automated theorem provers based on the given-clause algorithm. Our method influences the choice of unprocessed clauses using positive…