Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] DSL to encode induction heuristics in Isabelle

view this post on Zulip Email Gateway (Aug 22 2022 at 19:59):

From: "Nagashima, Yutaka" <Yutaka.Nagashima@uibk.ac.at>
Dear Isabelle users and developers,

I developed LiFtEr, a domain-specific language in Isabelle/ML, designed to encode induction heuristics in Isabelle.
LiFtEr is a domain-specific language in the sense that I developed it to encode induction heuristics,
but heuristics written in LiFtEr should not be specific to any problem domains.

I wrote a 19 page paper to explain this language, and the paper is available at GitHub [1].

For now, the intended workflow of LiFtEr is as following:

  1. Experienced users encode their induction heuristics as assertions in LiFtEr based on their experience in a certain problem, e.g. proving the equivalence of two reverse functions for list.
  2. New Isabelle users check if their invocations of the induct(ion) method are appropriate for their proof obligation (e.g. proving properties about stack machines) using the assertions developed by the experienced users in the previous step.

Eventually, I plan to

  1. encode many induction heuristics as assertions in LiFtEr,
  2. apply those assertions as a feature extractor to the Archive of Formal Proofs and build a database, which distills the essence of promising applications of the induct(ion) method,
  3. apply a machine learning algorithm to the database,
  4. build a tool that recommends how to apply the induct(ion) method to a given problem without completing a proof search.

My three page abstract at arXiv illustrates this supervised learning approach for automatic induction [2].

I developed LiFtEr based on my research hypothesis that many useful induction heuristics are programmable in a domain-independent way.
But I could not find preceding work in the same direction.
So, I will appreciate your constructive feedback about the direction of research, related work, Isabelle terminology, writing, etc.

[1] https://github.com/data61/PSL/blob/master/LiFtEr/LiFtEr.pdf
[2] https://arxiv.org/abs/1812.04088v2

Best,
Yutaka

Last updated: Apr 25 2024 at 12:23 UTC