5 citations · 6 across the 7 of their papers we have counts for
Showing cs.LOShow all
2 papers · 1 filter
cs.LO2026
Abduction Prover in Isabelle/HOL
Yutaka Nagashima, Daniel Sebastian Goc
Proof assistants based on expressive logics suffer limited automation for proof search, raising the cost of formal verification based on proof assistants. We address this problem b…
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…