149 citations · 825 across the 48 of their papers we have counts for
6 papers · 1 filter
Semantic Parsing of Mathematics by Context-based Learning from Aligned Corpora and Theorem Proving
Cezary Kaliszyk, Josef Urban, Jiří Vyskočil
We study methods for automated parsing of informal mathematical expressions into formal ones, a main prerequisite for deep computer understanding of informal mathematical texts. We…
BliStrTune: Hierarchical Invention of Theorem Proving Strategies
Jan Jakubuv, Josef Urban
Inventing targeted proof search strategies for specific problem sets is a difficult task. State-of-the-art automated theorem provers (ATPs) such as E allow a large number of user-s…
Monte Carlo Tableau Proof Search
Michael Färber, Cezary Kaliszyk, Josef Urban
We study Monte Carlo Tree Search to guide proof search in tableau calculi. This includes proposing a number of proof-state evaluation heuristics, some of which are learnt from prev…
Extending E Prover with Similarity Based Clause Selection Strategies
Jan Jakubův, Josef Urban
E prover is a state-of-the-art theorem prover for first-order logic with equality. E prover is built around a saturation loop, where new clauses are derived by inference rules from…
DeepMath - Deep Sequence Models for Premise Selection
Alex A. Alemi, Francois Chollet, Niklas Een +3
We study the effectiveness of neural sequence models for premise selection in automated theorem proving, one of the main bottlenecks in the formalization of mathematics. We propose…
Extracting Higher-Order Goals from the Mizar Mathematical Library
Chad Brown, Josef Urban
Certain constructs allowed in Mizar articles cannot be represented in first-order logic but can be represented in higher-order logic. We describe a way to obtain higher-order theor…