This repository has been updated to Isabelle2024. However, we have received reports that the integration of Sledgehammer with this repository is now less stable under Isabelle2024. Therefore, although we have confirmed that the Abduction Prover works in some cases, its performance may currently be suboptimal. We are working to resolve this issue as quickly as possible. 🙇
For users seeking the best performance, we recommend using Isabelle2023 and this version of the Abduction Prover (v0.2.7-alpha), which was developed specifically for Isabelle2023."
This repository contains various tools to support interactive theorem proving in Isabelle/HOL using artificial intelligence. This repository contains the implementation of proof strategy language (PSL) and its default strategy, try_hard, for Isabelle2024. Past versions of Isabelle, such as Isabelle2022-1, are no longer supported.
We opened a YouTube channel to introduce aspects of this project.
(path to the Isabelle binary)isabelle jedit -d (path to the directory that contains this README file) -l Smart_Isabelle
/Applications/Isabelle2024.app/bin/isabelle jedit -d . -l Smart_Isabelle
imports "Smart_Isabelle.Smart_Isabelle"
.Example/Example.thy
to see if the installation is successful.The basic steps are the same as MacOS and Linux.
However, instead of using the binary file directly, use Isabelle2024\Cygwin-Terminal
in Command Prompt. Once you start Isabelle2024\Cygwin-Terminal
, you can install our tools by typing isabelle jedit -d (path to the directory that contains this README file) -l Smart_Isabelle
. Note that once you started Isabelle2024\Cygwin-Terminal
, you should not specify the path to the Isabelle binary file. Therefore, the command you need after starting Isabelle2024\Cygwin-Terminal
is something like isabelle jedit -d . -l Smart_Isabelle
, assuming that your current directory is this one with this README.md/
If you find it difficult to install our tool, please refer to the Isabelle System Manual. Alternatively, you can just send an email to Yutaka at united.reasoning+gmail.com (reaplace + with @).
PSL's runtime tactic generation can result in a large number of messages in Isabelle/jEdit's output panel. This might cause Isabelle/jEdit to pause PSL's proof search after reaching its default upper limit for tracing messages.
We published academic papers describing the ideas implemented in this project.
Generalize
and Conjecture
in PSL/PGT
. (arXiv/Springer)PSL/PaMpeR
. (arXiv/ACM) Note that PaMpeR is currently not supported to minimise the cost to maintain this repository.We presented the final goal of this project at AITP2017. Our position paper "Towards Smart Proof Search for Isabelle" is available at arXiv.
We also plan to improve the proof automation using evolutionary computation. We presented our plan during the poster session at GECCO2019. Our poster-only paper is available at ACM digital library and arXiv.
PSL: Nagashima, Y., Kumar, R. (2017). A Proof Strategy Language and Proof Script Generation for Isabelle/HOL. In: de Moura, L. (eds) Automated Deduction – CADE 26. CADE 2017. Lecture Notes in Computer Science(), vol 10395. Springer, Cham. https://doi.org/10.1007/978-3-319-63046-5_32
PGT: Nagashima, Y., Parsert, J. (2018). Goal-Oriented Conjecturing for Isabelle/HOL. In: Rabe, F., Farmer, W., Passmore, G., Youssef, A. (eds) Intelligent Computer Mathematics. CICM 2018. Lecture Notes in Computer Science(), vol 11006. Springer, Cham. https://doi.org/10.1007/978-3-319-96812-4_19
PaMpeR: Yutaka Nagashima and Yilun He. 2018. PaMpeR: proof method recommendation system for Isabelle/HOL. In Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering (ASE 2018). Association for Computing Machinery, New York, NY, USA, 362–372. DOI:https://doi.org/10.1145/3238147.3238210
Towards Evolutionary Theorem Proving for Isabelle/HOL: Yutaka Nagashima. 2019. Towards evolutionary theorem proving for Isabelle/HOL. In Proceedings of the Genetic and Evolutionary Computation Conference Companion (GECCO ’19). Association for Computing Machinery, New York, NY, USA, 419–420. DOI:https://doi.org/10.1145/3319619.3321921
LiFtEr: Nagashima, Y. (2019). LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL. In: Lin, A. (eds) Programming Languages and Systems. APLAS 2019. Lecture Notes in Computer Science(), vol 11893. Springer, Cham. https://doi.org/10.1007/978-3-030-34175-6_14
Simple Dataset
Nagashima Y. (2020) Simple Dataset for Proof Method Recommendation in Isabelle/HOL. In: Benzmüller C., Miller B. (eds) Intelligent Computer Mathematics. CICM 2020. Lecture Notes in Computer Science, vol 12236. Springer, Cham. https://doi.org/10.1007/978-3-030-53518-6_21
Smart Induction
Yutaka Nagashima. Smart Induction for Isabelle/HOL (Tool Paper). In: Ivrii A., Strichman O. (eds) Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 DOI:https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_32
sem_ind
Yutaka Nagashima. Faster Smarter Proof by Induction in Isabelle/HOL. Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence Main Track. Pages 1981-1988 DOI:https://doi.org/10.24963/ijcai.2021/273
Definitional Quantifier and SeLFiE
Nagashima, Y. (2022). Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction. In: Kovács, L., Meinke, K. (eds) Tests and Proofs. TAP 2022. Lecture Notes in Computer Science, vol 13361. Springer, Cham. https://doi.org/10.1007/978-3-031-09827-7_4
Template-Based Conjecturing
Nagashima, Y., Xu, Z., Wang, N., Goc, D.S., Bang, J. (2023). Template-Based Conjecturing for Automated Induction in Isabelle/HOL. In: Hojjat, H., Ábrahám, E. (eds) Fundamentals of Software Engineering. FSEN 2023. Lecture Notes in Computer Science, vol 14155 . Springer, Cham. https://doi.org/10.1007/978-3-031-42441-0_9