7 citations · 25 across the 19 of their papers we have counts for
4 papers · 1 filter
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…
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…
Towards Smart Proof Search for Isabelle
Yutaka Nagashima
Despite the recent progress in automatic theorem provers, proof engineers are still suffering from the lack of powerful proof automation. In this position paper we first report our…