Abduction Prover vs Sledgehammer: The Prod Trial

Hey there! 🎉 Ready for some exciting updates?

Dive into this video as we showcase the latest advancements of our Abduction Prover!

We’re stacking it up against Sledgehammer using 10 riveting inductive challenges from the Tons of Inductive Problems. 🚀

Here’s what’s fresh out of the oven this release:

🚦 Unveiled the Best-First Expansion, calibrated perfectly to your available processes.

🛠️ Upped our game with enhanced stability.

🐞 Bid farewell to a bunch of pesky bugs.

🌀 Transitioned to a bold strategy, applying PSL tactics to new conjectures with gusto!

🔄 Guess who’s back? Nitpick makes its grand return in Abduction Prover.

📊 Sharpened our senses with a refined function to sideline those unpromising conjectures.

🔖 Changed naming conventions to produce more informative lemma names.

Let’s jump right in! 🎥🎈

For further details, refer to our GitHub repository:

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

Contact: united.reasoning@gmail.com

#ProofAutomationHasGoneTooFar #Isabelle/HOL #ProofByAbduction #Conjecturing