7 citations · 25 across the 19 of their papers we have counts for
5 papers · 1 filter
Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction
Yutaka Nagashima
Proof assistants offer tactics to apply proof by induction, but these tactics rely on inputs given by human engineers. To automate this laborious process, we developed SeLFiE, a bo…
Faster Smarter Induction in Isabelle/HOL
Yutaka Nagashima
Proof by induction plays a critical role in formal verification and mathematics at large. However, its automation remains as one of the long-standing challenges in Computer Science…
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…