[isabelle] New in the AFP: Auto2 Prover

Dear all,

we have another entry in the Tools section:


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.



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