Abduction Prover October 2023

What's new?

In this release, we:

• Introduced Best-First Expansion based on the number of available processes,
• Improved stability,
• Fixed many bugs,
• Switched to a strategy that applies PSL strategies to new conjectures more aggressively,
• Reintroduced Nitpick into Abduction Prover, and
• Enhanced the function to filter out unpromising conjectures.

Our small experiment based on this release confirmed that this version can automatically prove the following TIP problems: Prof01, Prod06, Prod11, Prod16, Prod21, Prod26, Prod31, Prod36, Prod41, and Prod46."

PSL and all that for Isabelle2023

We have updated PSL and all that for Isabelle2023.

The previous versions of Isabelle are no longer supported.

Abduction Prover

Performance improvement over the previous version.

Abduction Prover

The first release of Abduction Prover for Isabelle 2022.

PSL for Isabelle2021-1

This release should be compatible with Isabelle2021-1.

One needs to use the command similar the following to use PSL and all that.

(path to the Isabelle binary)isabelle jedit -d (path to the directory that contains this README file) -l Smart_Isabelle

Use it at your own risk.

Your feedback will be appreciated.

PSL for Isabelle2021

This release should be compatible with Isabelle2021.

Note that the directory layout has been changed from Isabelle2020 to Isabelle2021.
Therefore, one needs to use the command similar the following to use PSL and all that.

(path to the Isabelle binary)isabelle jedit -d (path to the directory that contains this README file) -l Smart_Isabelle

Other news:

• SeLFiE and sem_ind have made LiFtEr and smart_induct obsolete.

If you encounter problems, please send a message to the main developer, Yutaka Ng.

KR2021 based on Isabelle2020.

Note that this release is compatible for Isabelle2020.

TACAS2021: Artifact Submission

This release documents and minor fixes made for the artefact submission of semantic_induct at TACAS2021.

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.