Proof by Abduction, August 2023

On By yutakang

Explore the enhanced capabilities of the Abduction Prover within Isabelle/HOL in our latest demo.

Dive deep into the upgraded features of our “goal-oriented conjecturing” tool, first unveiled at CICM20181.

Key Innovations in the Abduction Prover for Isabelle2022:

  • 🔍 Efficiently proves goals within Isabelle, crafting insightful conjectures.
  • 🔗 Offers sophisticated analyses of inter-conjecture dependencies.
  • 🌀 Enables both simultaneous and intricate nested abduction.
  • 🛠 Seamlessly integrates with platforms such as PSL2, Sledgehammer3, Smart-induction4, and SeLFiE5.
  • 🌿 Harnesses the power of SeLFiE and Quickcheck6 to weed out less viable conjectures.
  • 🚀 Undertakes parallel proof exploration while delivering intuitive proof scripts.
  • 💡 Features innovative tactics as conjecturing mechanisms and promotes template-based conjecture synthesis.
  • 🔄 Employs alpha-equivalence for free variable management, ensuring zero duplications.
  • 🔗 Pioneers lemma-sharing by crafting a comprehensive abduction graph. In this fast-forwarded video, we compare the Abduction Prover with Sledgehammer.

While showcasing the current state of the Abduction Prover, we highlight this as a somewhat “silly” comparison for these reasons:

1. The evaluation focuses on selected induction problems from the TIP benchmark.7 Induction problems are a known weakness of Sledgehammer.

2. The Abduction Prover has been granted longer timeouts than Sledgehammer’s default 30-second limit. However, we believe that even with extended timeouts, Sledgehammer might not fare much better. For further details, refer to our GitHub repository:

https://github.com/data61/PSL/releases/tag/v0.2.5-alpha.”

Contact: united.reasoning@gmail.com

  1. 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 ↩︎
  2. 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  ↩︎
  3. Lawrence C. Paulson, Jasmin Christian Blanchette: Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers. IWIL@LPAR 2010  ↩︎
  4. 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 https://doi.org/10.24963/ijcai.2021/273  ↩︎
  5. 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  ↩︎
  6. Bulwahn, L. (2012). The New Quickcheck for Isabelle. In: Hawblitzel, C., Miller, D. (eds) Certified Programs and Proofs. CPP 2012. Lecture Notes in Computer Science, vol 7679. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35308-6_10  ↩︎
  7. Claessen, K., Johansson, M., Rosén, D., Smallbone, N. (2015). TIP: Tons of Inductive Problems. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds) Intelligent Computer Mathematics. CICM 2015. Lecture Notes in Computer Science(), vol 9150. Springer, Cham. https://doi.org/10.1007/978-3-319-20615-8_23 ↩︎