1 citations · 2 across the 6 of their papers we have counts for
10 papers
Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description)
Yutaka Nagashima
Recently, a growing number of researchers have applied machine learning to assist users of interactive theorem provers. However, the expressive nature of underlying logics and esot…
Towards United Reasoning for Automatic Induction in Isabelle/HOL
Yutaka Nagashima
Inductive theorem proving is an important long-standing challenge in computer science. In this extended abstract, we first summarize the recent developments of proof by induction f…
Smart Induction for Isabelle/HOL (System Description)
Yutaka Nagashima
Proof assistants offer tactics to facilitate inductive proofs. However, it still requires human ingenuity to decide what arguments to pass to those induction tactics. To automate t…
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…