Email Gateway (Dec 20 2025 at 00:56): Email Gateway (Dec 20 2025 at 00:56):From: Gerwin Klein <cl-isabelle-users@lists.cam.ac.uk>
Following the Isabelle release, the AFP is now available for Isabelle2025-1 from https://isa-afp.org
There are now more than 5 million lines of Isabelle proof in 944 entries by 576 authors.
Five new entries have become available from the home page that were previously only available in the development version:
Dedekind Sums
by Manuel Eberl, Anthony Bordg, Lawrence C. Paulson and Wenda Li
https://www.isa-afp.org/entries/Dedekind_Sums.html
Complex Lattices, Elliptic Functions, and the Modular Group
by Manuel Eberl, Anthony Bordg, Wenda Li and Lawrence C. Paulson
https://www.isa-afp.org/entries/Elliptic_Functions.html
The Partition Function and the Pentagonal Number Theorem
by Manuel Eberl
https://www.isa-afp.org/entries/Pentagonal_Number_Theorem.html
Typed Ordered Resolution
by Adnan Mohammed Ahmed and Balazs Toth
https://www.isa-afp.org/entries/Typed_Ordered_Resolution.html
Ordered Resolution is a proof calculus for reasoning about first-order
logic that is implemented in many automatic theorem provers. It works
by saturating the given set of clauses and is refutationally complete,
meaning that if the set is inconsistent, the saturation will contain a
contradiction. In this formalization, we restructured the completeness
proof to cleanly separate the ground (i.e., variable-free) and
nonground aspects. We also added a type system to the calculus. We
relied on the library for first-order clauses and on the saturation
framework.
Zippy - Generic White-Box Proof Search with Zippers
by Kevin Kappelmann
https://www.isa-afp.org/entries/Zippy.html
This entry contains Zippy, a framework for tree-based searches. Zippy
is largely independent of concrete search tree representations, search
algorithms, states and effects. It is designed to create analysable
and navigable searches that are open to customisation and extensions
by users. An accompanying arXiv preprint is available here.
This entry also provides a concrete instantiation of the framework in
the form of a general purpose white-box prover, called zip. The prover
performs a proof tree search with customisable expansion actions and
search strategies, including A, breadth-first, depth-first, and
best-first search. By default, it integrates the classical reasoner,
simplifier, the blast and metis prover, and supports resolution with
higher-order and proof-producing unification, conditional substitutions,
case splitting, and induction, among other things. Users are free to
extend the prover with additional expansion actions and search
strategies. We demonstrate the capabilities of zip in an examples theory.
In most cases, zip can be used as a drop-in replacement for
Isabelle's classical methods, including auto, fastforce, force, fast, etc.
We demonstrate this with a benchmark containing 2267 method calls from
Isabelle's standard library, where zip achieves a success rate of
99.82% (2263/2267).
The Zippy framework is founded on concepts from functional programming
theory, particularly zippers, arrows, monads, lenses, and coroutines.
This entry contains a library of mentioned concepts for Isabelle/ML.
Enjoy!
Gerwin
This email and any files transmitted with it may contain confidential information. If you believe you have received this email or any of its contents in error, please notify me immediately by return email and destroy this email. Do not use, disseminate, forward, print or copy any contents of an email received in error.
Last updated: Dec 21 2025 at 20:24 UTC