17 citations · 42 across the 6 of their papers we have counts for
7 papers
Learning Guided Automated Reasoning: A Brief Survey
Lasse Blaauwbroek, David Cerna, Thibault Gauthier +4
Automated theorem provers and formal proof assistants are general reasoning systems that are in theory capable of proving arbitrarily hard theorems, thus solving arbitrary problems…
The Tactician's Web of Large-Scale Formal Knowledge
Lasse Blaauwbroek
The Tactician's Web is a platform offering a large web of strongly interconnected, machine-checked, formal mathematical knowledge conveniently packaged for machine learning, analyt…
Graph2Tac: Online Representation Learning of Formal Math Concepts
Lasse Blaauwbroek, Miroslav Olšák, Jason Rute +3
In proof assistants, the physical proximity between two formal mathematical concepts is a strong predictor of their mutual relevance. Furthermore, lemmas with close proximity regul…
Hashing Modulo Context-Sensitive -Equivalence
Lasse Blaauwbroek, Miroslav Olšák, Herman Geuvers
The notion of -equivalence between -terms is commonly used to identify terms that are considered equal. However, due to the primitive treatment of free variables, this notion…
Online Machine Learning Techniques for Coq: A Comparison
Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski +3
We present a comparison of several online machine learning techniques for tactical learning and proving in the Coq proof assistant. This work builds on top of Tactician, a plugin f…
The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq
Lasse Blaauwbroek, Josef Urban, Herman Geuvers
We present Tactician, a tactic learner and prover for the Coq Proof Assistant. Tactician helps users make tactical proof decisions while they retain control over the general proof…
Tactic Learning and Proving for the Coq Proof Assistant
Lasse Blaauwbroek, Josef Urban, Herman Geuvers
We present a system that utilizes machine learning for tactic proof search in the Coq Proof Assistant. In a similar vein as the TacticToe project for HOL4, our system predicts appr…