7 citations · 25 across the 19 of their papers we have counts for
4 papers · 1 filter
Domain-Specific Language to Encode Induction Heuristics
Yutaka Nagashima
Proof assistants, such as Isabelle/HOL, offer tools to facilitate inductive theorem proving. Isabelle experts know how to use these tools effectively; however, they did not have a…
Designing Game of Theorems
Yutaka Nagashima
"Theorem proving is similar to the game of Go. So, we can probably improve our provers using deep learning, like DeepMind built the super-human computer Go program, AlphaGo." Such…
LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL
Yutaka Nagashima
Proof assistants, such as Isabelle/HOL, offer tools to facilitate inductive theorem proving. Isabelle experts know how to use these tools effectively; however, there is a little to…
Towards Evolutionary Theorem Proving for Isabelle/HOL
Yutaka Nagashima
Mechanized theorem proving is becoming the basis of reliable systems programming and rigorous mathematics. Despite decades of progress in proof automation, writing mechanized proof…