3 citations · 6 across the 3 of their papers we have counts for
3 papers
cs.LO2023
Template-Based Conjecturing for Automated Induction in Isabelle/HOL
Yutaka Nagashima, Zijin Xu, Ningli Wang +2
Proof by induction plays a central role in formal verification. However, its automation remains as a formidable challenge in Computer Science. To solve inductive problems, human en…
cs.AI2017★ 3 cited
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…
cs.PL2016★ 3 cited
Close Encounters of the Higher Kind Emulating Constructor Classes in Standard ML
Yutaka Nagashima, Liam O'Connor
We implement a library for encoding constructor classes in Standard ML, including elaboration from minimal definitions, and automatic instantiation of superclasses.