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

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

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

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.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Average on weekdays: 9142.55710306 kWh The History of Art Graduate Centre - 4a Trumpington Street (above Hot Numbers coffee shop) Graduate Development Lecture Series

Other talks

Cooperation as a Laboratory of Being A Novel Diffusion Model based Approach for Sleep Music Generation The United States of America at 250: Reflections on the Past, Present and Future of Independence Title TBC title abstract tbc Shape modes of CP^1 vortices
 

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