Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Auto2 Prover

Email Gateway (Aug 22 2022 at 18:48):

From: Manuel Eberl <eberlm@in.tum.de>
Dear all,

we have another entry in the Tools section:

https://www.isa-afp.org/entries/Auto2_HOL.html

Auto2 Prover
by Bohua Zhan

Auto2 is a saturation-based heuristic prover for higher-order logic,
implemented as a tactic in Isabelle. This entry contains the
instantiation of auto2 for Isabelle/HOL, along with two basic
examples: solutions to some of the Pelletier’s problems, and
elementary number theory of primes.

Cheers,

Manuel

Last updated: Apr 27 2024 at 01:05 UTC