21 citations · 116 across the 21 of their papers we have counts for
Showing 2020Show all
3 papers · 1 filter
cs.AI2020★ 14 cited
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…
cs.AI2020★ 17 cited
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…
cs.LO2020★ 16 cited
Relating Apartness and Bisimulation
Herman Geuvers, Bart Jacobs
A bisimulation for a coalgebra of a functor on the category of sets can be described via a coalgebra in the category of relations, of a lifted functor. A final coalgebra then gives…