Automating proof by induction in Isabelle/HOL using domain-specific languages

Add to your list(s) Download to your calendar using vCal

• Yutaka Nagashima, Czech University in Prague (CTU) & University of Innsbruck
• Wednesday 04 March 2020, 10:00-10:20
• Computer Lab, FW11.

If you have a question about this talk, please contact Jean Pichon-Pharabod.

Isabelle/HOL offers the induction tactic to facilitate inductive proofs. However, it still requires human ingenuity to decide what arguments to pass to the induction tactic. To automate this process, I developed two domain-specific languages, PSL and LiFtEr. PSL attempts to find out the right combination of arguments to the induction tactic through a search, whereas LiFtEr identifies promising combinations of arguments without relying on a search. Our evaluation demonstrated that PSL and LiFtEr produce valuable recommendations across problem domains.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Lab, FW11
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• tcw57’s list
• yk373's list
• yk449

Note that ex-directory lists are not shown.