University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Automating proof by induction in Isabelle/HOL using domain-specific languages

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

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

  • UserYutaka Nagashima, Czech University in Prague (CTU) & University of Innsbruck
  • ClockWednesday 04 March 2020, 10:00-10:20
  • HouseComputer 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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2020 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity