[isabelle] New in the AFP: Auto2 Prover



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.