TACAS2021: the first release of semantic_induct

This release the version of semantic_induct used in the evaluation for TACAS2021.

Our evaluation based on 1,095 inductive problems from 22 theory files shows the following:
when compared to smart_induct, semantic_induct achieves a 90.0% increase of the coincidence rate for the most promising candidate within 5.0 seconds of timeout while achieving a 62.0% decrease of the median value of execution time.

For the AEC at TACAS2020:
To format the raw results, you have to replace every ";"s with ","s in Database.txt and place them at the locations with the right names as written in the artifact submission.

PADL2021: the first release of SeLFiE

This is the accompanying release for our PADL2021 submission. This release contains the interpreter of SeLFiE in PSL/SeLFiE.

To learn how to install is, read the instructions in PSL/SeLFiE/README.md.

Proof by induction is a long-standing challenge in Computer Science.
Proof assistants offer tactics to apply proof by induction, but these tactics rely on inputs given by human engineers.
We address this problem with SeLFiE, a domain-specific language to encode experienced users’ expertise on how to apply the induct tactic in Isabelle/HOL: when we apply an induction heuristic written in SeLFiE to an inductive problem and arguments to the induct tactic, the interpreter examines both the syntactic structure of the problem and semantics of the relevant constants to judge whether the arguments to the induct tactic are plausible according to the heuristic.

FMCAD2020

This is the submission to FMCAD2020.

To use smart_induct, it is necessary to

1. install the latest version of Isabelle/HOL (Isabelle2020),
2. download this repository and start Isabelle/jEdit with smart_induct from Terminal for MacOS users (or Command Prompt for Windows users).

Assuming your current directory is the top directory of this repository, the necessary command should look like the following:

(path-to-the-Isabelle-binary)isabelle jedit -d PSL/ -l PSL -d LiFtEr/ -l LiFtEr -d Smart_Induct/ -l Smart_Induct

where PSL/ after -d should be the path to the sub-directory PSL/PSL, and LiFtEr after -d should be the path to the sub-directory PSL/LiFtEr, and so on.

For more details, see The Isabelle System Manual.

As a starter, users can find the example proofs used in the paper in PSL/Smart_Induct/Example/Induction_Demo.thy.

MFCS2020

This is the submission to MFCS2020.

Users have to build this file.

Assuming your current directory is the top directory of this repository, the necessary command should look like the following:

(path-to-the-Isabelle-binary)isabelle jedit -d PSL/ -l PSL -d LiFtEr/ -l LiFtEr -d Smart_Induct/ -l Smart_Induct

where PSL/ after -d should be the path to the sub-directory PSL/PSL, and LiFtEr after -d should be the path to the sub-directory PSL/LiFtEr, and so on.

For more details, see The Isabelle System Manual.

smart_induct for IJCAR2020

smart_induct

Dear IJCAR reviewers.
Our running example explained in the paper resides in PSL/Smart_Induct/Example/Induction_Demo.thy.

To use smart_induct in your own file,
you only have to use import Smart_Induct.thy in this directory using the imports keyword of Isabelle/HOL.
It is important to set the path to Smart_Induct.thy correctly.

The evaluation files reside in the Evaluation directory.
If you open the following files using Isabelle2019, you can see smart_induct at work:

• PSL/Smart_Induct/Evaluation/Depth-First-Search/DFS.thy
• PSL/Smart_Induct/Evaluation/KD_Tree/Nearest_Neighbor.thy
• PSL/Smart_Induct/Evaluation/Priority_Search_Trees/PST_RBT.thy.

Enjoy!

System requirements:

• Isabelle2019 (The vastest official version of Isabelle at the time of release.)
• A modern computer that can handle Isabelle/HOL will do. For example, you might want to have 16 GB of memory.

LiFtEr: the final version for APLAS2019 for Isabelle2019

This version contains a working prototype of LiFtEr.
The source code is compatible with Isabelle2019.

Our paper submitted at The 17th Asian Symposium on Programming Languages and Systems (APLAS2019) presents the concept of LiFtEr through examples.

One can find the examples used in the paper in the following files:

• LiFtEr/Example/Concrete_Semantics/Induction_Demo.thy,
• LiFtEr/Example/Concrete_Semantics/ASM.thy, and
• LiFtEr/Example/IMP2/basic/Semantics.thy

LiFtEr: APLAS2019 for Isabelle2019

This version contains a working prototype of LiFtEr. The source code is compatible with Isabelle2019.

Our paper submitted at The 17th Asian Symposium on Programming Languages and Systems (APLAS2019) presents the concept of LiFtEr through examples.

One can find the examples used in the paper in the following files:

• LiFtEr/Concrete_Semantics/Induction_Demo.thy, and
• LiFtEr/Concrete_Semantics/ASM.thy

PSL, PaMpeR, and PGT for Isabelle2018.

We have updated PSL and PaMpeR for Isabelle2018 and tested against a small test base.
PGT strategies (Generalize and Conjecture) might be still unstable.

PSL with PGT: CICM2018 for Isabelle2017

This version contains the prototype of Proof Goal Transformer (PGT) within the framework of PSL. The source code is compatible with Isabelle2017. We described PGT in our tool paper accepted at 11th Conference on Intelligent Computer Mathematics (CICM2018).

PaMpeR: ITP2018

Our draft "PaMpeR: A Proof Method Recommendation System for Isabelle/HOL" is based on this version.

This version provides the basic commands of PaMpeR and is ready to use.

We have confirmed that this version produces valuable recommendations about special-purpose proof methods in our preliminary evaluation.

The default recommendation of this version is based on Isabelle's standard library.

We expect that we can improve the accuracy of PaMpeR's proof recommendation by adding more features and using larger proof corpora for data extraction.