diff --git a/metadata/entries/Affine_Arithmetic.toml b/metadata/entries/Affine_Arithmetic.toml
--- a/metadata/entries/Affine_Arithmetic.toml
+++ b/metadata/entries/Affine_Arithmetic.toml
@@ -1,34 +1,32 @@
title = "Affine Arithmetic"
date = 2014-02-07
topics = [
"Mathematics/Analysis",
]
abstract = """
We give a formalization of affine forms as abstract representations of zonotopes.
We provide affine operations as well as overapproximations of some non-affine operations like multiplication and division.
Expressions involving those operations can automatically be turned into (executable) functions approximating the original
expression in affine arithmetic."""
license = "bsd"
note = ""
[authors]
[authors.immler]
homepage = "immler_homepage"
[contributors]
[notify]
immler = "immler_email"
[history]
-2015-01-31 = """
-added algorithm for zonotope/hyperplane intersection
-"""
+2015-01-31 = "added algorithm for zonotope/hyperplane intersection
"
2017-09-20 = """
linear approximations for all symbols from the floatarith data
type"""
[extra]
[related]
diff --git a/metadata/entries/Algebraic_Numbers.toml b/metadata/entries/Algebraic_Numbers.toml
--- a/metadata/entries/Algebraic_Numbers.toml
+++ b/metadata/entries/Algebraic_Numbers.toml
@@ -1,43 +1,41 @@
title = "Algebraic Numbers in Isabelle/HOL"
date = 2015-12-22
topics = [
"Mathematics/Algebra",
]
abstract = """
Based on existing libraries for matrices, factorization of rational polynomials, and Sturm's theorem, we formalized algebraic numbers in Isabelle/HOL. Our development serves as an implementation for real and complex numbers, and it admits to compute roots and completely factorize real and complex polynomials, provided that all coefficients are rational numbers. Moreover, we provide two implementations to display algebraic numbers, an injective and expensive one, or a faster but approximative version.
To this end, we mechanized several results on resultants, which also required us to prove that polynomials over a unique factorization domain form again a unique factorization domain.
""" license = "bsd" note = "" [authors] [authors.thiemann] email = "thiemann_email" [authors.yamada] email = "yamada_email" [authors.joosten] email = "joosten_email" [contributors] [contributors.eberl] homepage = "eberl_homepage" [notify] thiemann = "thiemann_email" yamada = "yamada_email1" joosten = "joosten_email" [history] -2016-01-29 = """ -Split off Polynomial Interpolation and Polynomial Factorization
A preliminary version of this work (without pairing heaps) is described
in a paper
published in the proceedings of the conference on Interactive
Theorem Proving ITP 2015. An extended version of this publication
is available here."""
license = "bsd"
note = ""
[authors]
[authors.nipkow]
homepage = "nipkow_homepage"
[contributors]
[notify]
nipkow = "nipkow_email"
[history]
-2015-03-17 = """
-Added pairing heaps by Hauke Brinkop.
-"""
-2016-07-12 = """
-Moved splay heaps from here to Splay_Tree
-"""
+2015-03-17 = "Added pairing heaps by Hauke Brinkop.
"
+2016-07-12 = "Moved splay heaps from here to Splay_Tree
"
2016-07-14 = "Moved pairing heaps from here to the new Pairing_Heap"
[extra]
[related]
diff --git a/metadata/entries/Applicative_Lifting.toml b/metadata/entries/Applicative_Lifting.toml
--- a/metadata/entries/Applicative_Lifting.toml
+++ b/metadata/entries/Applicative_Lifting.toml
@@ -1,42 +1,40 @@
title = "Applicative Lifting"
date = 2015-12-22
topics = [
"Computer science/Functional programming",
]
abstract = """
Applicative functors augment computations with effects by lifting function application to types which model the effects. As the structure of the computation cannot depend on the effects, applicative expressions can be analysed statically. This allows us to lift universally quantified equations to the effectful types, as observed by Hinze. Thus, equational reasoning over effectful computations can be reduced to pure types.
This entry provides a package for registering applicative functors and two proof methods for lifting of equations over applicative functors. The first method normalises applicative expressions according to the laws of applicative functors. This way, equations whose two sides contain the same list of variables can be lifted to every applicative functor.
To lift larger classes of equations, the second method exploits a number of additional properties (e.g., commutativity of effects) provided the properties have been declared for the concrete applicative functor at hand upon registration.
We declare several types from the Isabelle library as applicative functors and illustrate the use of the methods with two examples: the lifting of the arithmetic type class hierarchy to streams and the verification of a relabelling function on binary trees. We also formalise and verify the normalisation algorithm used by the first proof method.
""" license = "bsd" note = "" [authors] [authors.lochbihler] homepage = "lochbihler_homepage" [authors.schneider] [contributors] [notify] lochbihler = "lochbihler_email1" [history] -2016-03-03 = """ -added formalisation of lifting with combinators
To support arbitrary nesting of sets, we define a linear order on sets based on a linear order of the elements and provide efficient implementations.
It even allows to compare complements with non-complements."""
license = "bsd"
note = ""
[authors]
[authors.lochbihler]
homepage = "lochbihler_homepage"
[contributors]
[contributors.thiemann]
email = "thiemann_email"
[notify]
lochbihler = "lochbihler_email1"
[history]
-2013-07-11 = """
-add pretty printing for sets (revision 7f3f52c5f5fa)
-"""
+2013-07-11 = "add pretty printing for sets (revision 7f3f52c5f5fa)
"
2013-09-20 = """
provide generators for canonical type class instantiations
(revision 159f4401f4a8 by René Thiemann)
"""
-2014-07-08 = """
-add support for going from partial functions to mappings (revision 7a6fc957e8ed)
-"""
+2014-07-08 = "add support for going from partial functions to mappings (revision 7a6fc957e8ed)
"
2018-03-05 = "add two application examples: depth-first search and 2SAT (revision e5e1a1da2411)"
[extra]
[related]
diff --git a/metadata/entries/Efficient-Mergesort.toml b/metadata/entries/Efficient-Mergesort.toml
--- a/metadata/entries/Efficient-Mergesort.toml
+++ b/metadata/entries/Efficient-Mergesort.toml
@@ -1,38 +1,36 @@
title = "Efficient Mergesort"
date = 2011-11-09
topics = [
"Computer science/Algorithms",
]
abstract = "We provide a formalization of the mergesort algorithm as used in GHC's Data.List module, proving correctness and stability. Furthermore, experimental data suggests that generated (Haskell-)code for this algorithm is much faster than for previous algorithms available in the Isabelle distribution."
license = "bsd"
note = ""
[authors]
[authors.sternagel]
email = "sternagel_email"
[contributors]
[notify]
sternagel = "sternagel_email"
[history]
-2012-10-24 = """
-Added reference to journal article.
-"""
+2012-10-24 = "Added reference to journal article.
"
2018-09-17 = """
Added theory Efficient_Mergesort that works exclusively with the mutual
induction schemas generated by the function package.
"""
2018-09-19 = """
Theory Efficient_Mergesort replaces theory Efficient_Sort but keeping the old
name Efficient_Sort.
"""
2020-11-20 = """
Additional theory Natural_Mergesort that developes an efficient mergesort
algorithm without key-functions for educational purposes."""
[extra]
[related]
diff --git a/metadata/entries/Flyspeck-Tame.toml b/metadata/entries/Flyspeck-Tame.toml
--- a/metadata/entries/Flyspeck-Tame.toml
+++ b/metadata/entries/Flyspeck-Tame.toml
@@ -1,37 +1,35 @@
title = "Flyspeck I: Tame Graphs"
date = 2006-05-22
topics = [
"Mathematics/Graph theory",
]
abstract = """
These theories present the verified enumeration of tame plane graphs
as defined by Thomas C. Hales in his proof of the Kepler Conjecture in his
book Dense Sphere Packings. A Blueprint for Formal Proofs. [CUP 2012].
The values of the constants in the definition of tameness are identical to
those in the Flyspeck project.
The IJCAR 2006 paper by Nipkow, Bauer and Schultz refers to the original version of Hales' proof,
the ITP 2011 paper by Nipkow refers to the Blueprint version of the proof."""
license = "bsd"
note = ""
[authors]
[authors.bauer]
[authors.nipkow]
homepage = "nipkow_homepage"
[contributors]
[notify]
nipkow = "nipkow_email"
[history]
-2010-11-02 = """
-modified theories to reflect the modified definition of tameness in Hales' revised proof.
-"""
+2010-11-02 = "modified theories to reflect the modified definition of tameness in Hales' revised proof.
"
2014-07-03 = "modified constants in def of tameness and Archive according to the final state of the Flyspeck proof."
[extra]
[related]
diff --git a/metadata/entries/Interpreter_Optimizations.toml b/metadata/entries/Interpreter_Optimizations.toml
--- a/metadata/entries/Interpreter_Optimizations.toml
+++ b/metadata/entries/Interpreter_Optimizations.toml
@@ -1,40 +1,38 @@
title = "Inline Caching and Unboxing Optimization for Interpreters"
date = 2020-12-07
topics = [
"Computer science/Programming languages/Misc",
]
abstract = """
This Isabelle/HOL formalization builds on the
VeriComp entry of the Archive of Formal
Proofs to provide the following contributions:
Matrix interpretations are useful as measure functions in termination proving. In order to use these interpretations also for complexity analysis, the growth rate of matrix powers has to examined. Here, we formalized a central result of spectral radius theory, namely that the growth rate is polynomially bounded if and only if the spectral radius of a matrix is at most one.
To formally prove this result we first studied the growth rates of matrices in Jordan normal form, and prove the result that every complex matrix has a Jordan normal form using a constructive prove via Schur decomposition.
The whole development is based on a new abstract type for matrices, which is also executable by a suitable setup of the code generator. It completely subsumes our former AFP-entry on executable matrices, and its main advantage is its close connection to the HMA-representation which allowed us to easily adapt existing proofs on determinants.
All the results have been applied to improve CeTA, our certifier to validate termination and complexity proof certificates.
""" license = "bsd" note = "" [authors] [authors.thiemann] email = "thiemann_email" [authors.yamada] email = "yamada_email" [contributors] [contributors.bentkamp] email = "bentkamp_email" [notify] thiemann = "thiemann_email" yamada = "yamada_email1" [history] -2016-01-07 = """ -Added Schur-decomposition, Gram-Schmidt orthogonalization, uniqueness of Jordan normal formsSession Ordinary-Differential-Equations formalizes ordinary differential equations (ODEs) and initial value problems. This work comprises proofs for local and global existence of unique solutions (Picard-Lindelöf theorem). Moreover, it contains a formalization of the (continuous or even differentiable) dependency of the flow on initial conditions as the flow of ODEs.
Not in the generated document are the following sessions:
This formalization also contains an abstract representation as coefficient functions with finite
support and a type of power-products. If this type is ordered by a linear (term) ordering, various
additional notions, such as leading power-product, leading coefficient etc., are introduced as
well. Furthermore, a lot of generic properties of, and functions on, multivariate polynomials are
formalized, including the substitution and evaluation homomorphisms, embeddings of polynomial rings
into larger rings (i.e. with one additional indeterminate), homogenization and dehomogenization of
polynomials, and the canonical isomorphism between R[X,Y] and R[X][Y]."""
license = "lgpl"
note = ""
[authors]
[authors.sternagel]
email = "sternagel_email"
[authors.thiemann]
homepage = "thiemann_homepage"
[authors.maletzky]
homepage = "maletzky_homepage"
[authors.immler]
homepage = "immler_homepage"
[authors.haftmann]
homepage = "haftmann_homepage"
[authors.lochbihler]
homepage = "lochbihler_homepage"
[authors.bentkamp]
email = "bentkamp_email"
[contributors]
[notify]
thiemann = "thiemann_email"
sternagel = "sternagel_email1"
maletzky = "maletzky_email"
immler = "immler_email"
[history]
-2010-09-17 = """
-Moved theories on arbitrary (ordered) semirings to Abstract Rewriting.
-"""
-2016-10-28 = """
-Added abstract representation of polynomials and authors Maletzky/Immler.
-"""
+2010-09-17 = "Moved theories on arbitrary (ordered) semirings to Abstract Rewriting.
"
+2016-10-28 = "Added abstract representation of polynomials and authors Maletzky/Immler.
"
2018-01-23 = """
Added authors Haftmann, Lochbihler after incorporating
their formalization of multivariate polynomials based on Polynomial mappings.
Moved material from Bentkamp's entry \"Deep Learning\".
"""
2019-04-18 = """
Added material about polynomials whose power-products are represented themselves
by polynomial mappings."""
[extra]
[related]
diff --git a/metadata/entries/Regular-Sets.toml b/metadata/entries/Regular-Sets.toml
--- a/metadata/entries/Regular-Sets.toml
+++ b/metadata/entries/Regular-Sets.toml
@@ -1,36 +1,34 @@
title = "Regular Sets and Expressions"
date = 2010-05-12
topics = [
"Computer science/Automata and formal languages",
]
abstract = "This is a library of constructions on regular expressions and languages. It provides the operations of concatenation, Kleene star and derivative on languages. Regular expressions and their meaning are defined. An executable equivalence checker for regular expressions is verified; it does not need automata but works directly on regular expressions. By mapping regular expressions to binary relations, an automatic and complete proof method for (in)equalities of binary relations over union, concatenation and (reflexive) transitive closure is obtained.
Extended regular expressions with complement and intersection are also defined and an equivalence checker is provided."
license = "bsd"
note = ""
[authors]
[authors.krauss]
homepage = "krauss_homepage"
[authors.nipkow]
homepage = "nipkow_homepage"
[contributors]
[contributors.eberl]
homepage = "eberl_homepage"
[notify]
nipkow = "nipkow_email"
krauss = "krauss_email"
urban = "urban_email"
[history]
-2011-08-26 = """
-Christian Urban added a theory about derivatives and partial derivatives of regular expressions
-"""
+2011-08-26 = "Christian Urban added a theory about derivatives and partial derivatives of regular expressions
"
2012-05-10 = "Tobias Nipkow added equivalence checking with partial derivatives"
[extra]
[related]
diff --git a/metadata/entries/Resolution_FOL.toml b/metadata/entries/Resolution_FOL.toml
--- a/metadata/entries/Resolution_FOL.toml
+++ b/metadata/entries/Resolution_FOL.toml
@@ -1,60 +1,60 @@
title = "The Resolution Calculus for First-Order Logic"
date = 2016-06-30
topics = [
"Logic/General logic/Mechanization of proofs",
]
abstract = """
This theory is a formalization of the resolution calculus for
first-order logic. It is proven sound and complete. The soundness
proof uses the substitution lemma, which shows a correspondence
between substitutions and updates to an environment. The completeness
proof uses semantic trees, i.e. trees whose paths are partial Herbrand
interpretations. It employs Herbrand's theorem in a formulation which
states that an unsatisfiable set of clauses has a finite closed
semantic tree. It also uses the lifting lemma which lifts resolution
derivation steps from the ground world up to the first-order world.
The theory is presented in a paper in the Journal of Automated Reasoning
[Sch18] which extends a paper presented at the International Conference
on Interactive Theorem Proving [Sch16]. An earlier version was
presented in an MSc thesis [Sch15]. The formalization mostly follows
textbooks by Ben-Ari [BA12], Chang and Lee [CL73], and Leitsch [Lei97].
The theory is part of the IsaFoL project [IsaFoL].
[Sch18] Anders Schlichtkrull. \"Formalization of the
Resolution Calculus for First-Order Logic\". Journal of Automated
Reasoning, 2018.
[Sch16] Anders
Schlichtkrull. \"Formalization of the Resolution Calculus for First-Order
Logic\". In: ITP 2016. Vol. 9807. LNCS. Springer, 2016.
[Sch15] Anders Schlichtkrull.
\"Formalization of Resolution Calculus in Isabelle\".
https://people.compute.dtu.dk/andschl/Thesis.pdf.
MSc thesis. Technical University of Denmark, 2015.
[BA12] Mordechai Ben-Ari. Mathematical Logic for
Computer Science. 3rd. Springer, 2012.
[CL73] Chin-Liang Chang and Richard Char-Tung Lee.
Symbolic Logic and Mechanical Theorem Proving. 1st. Academic
Press, Inc., 1973.
[Lei97] Alexander
Leitsch. The Resolution Calculus. Texts in theoretical computer
science. Springer, 1997.
[IsaFoL]
IsaFoL authors.
IsaFoL: Isabelle Formalization of Logic.
https://bitbucket.org/jasmin_blanchette/isafol."""
license = "bsd"
note = ""
[authors]
[authors.schlichtkrull]
homepage = "schlichtkrull_homepage"
[contributors]
[notify]
schlichtkrull = "schlichtkrull_email"
[history]
-2018-01-24 = "added several new versions of the soundness and completeness theorems as described in the paper "
-2018-03-20 = "added a concrete instance of the unification and completeness theorems using the First-Order Terms AFP-entry from IsaFoR as described in the papers "
+2018-01-24 = "added several new versions of the soundness and completeness theorems as described in the paper"
+2018-03-20 = "added a concrete instance of the unification and completeness theorems using the First-Order Terms AFP-entry from IsaFoR as described in the papers"
[extra]
[related]
diff --git a/metadata/entries/Show.toml b/metadata/entries/Show.toml
--- a/metadata/entries/Show.toml
+++ b/metadata/entries/Show.toml
@@ -1,39 +1,37 @@
title = "Haskell's Show Class in Isabelle/HOL"
date = 2014-07-29
topics = [
"Computer science/Functional programming",
]
abstract = """
We implemented a type class for \"to-string\" functions, similar to
Haskell's Show class. Moreover, we provide instantiations for Isabelle/HOL's
standard types like bool, prod, sum, nats, ints, and rats. It is further
possible, to automatically derive show functions for arbitrary user defined
datatypes similar to Haskell's \"deriving Show\"."""
license = "lgpl"
note = ""
[authors]
[authors.sternagel]
email = "sternagel_email"
[authors.thiemann]
email = "thiemann_email"
[contributors]
[notify]
sternagel = "sternagel_email1"
thiemann = "thiemann_email"
[history]
-2015-03-11 = """
-Adapted development to new-style (BNF-based) datatypes.
-"""
+2015-03-11 = "Adapted development to new-style (BNF-based) datatypes.
"
2015-04-10 = """
Moved development for old-style datatypes into subdirectory
\"Old_Datatype\".
"""
[extra]
[related]
diff --git a/metadata/entries/Sqrt_Babylonian.toml b/metadata/entries/Sqrt_Babylonian.toml
--- a/metadata/entries/Sqrt_Babylonian.toml
+++ b/metadata/entries/Sqrt_Babylonian.toml
@@ -1,32 +1,30 @@
title = "Computing N-th Roots using the Babylonian Method"
date = 2013-01-03
topics = [
"Mathematics/Analysis",
]
abstract = """
We implement the Babylonian method to compute n-th roots of numbers.
We provide precise algorithms for naturals, integers and rationals, and
offer an approximation algorithm for square roots over linear ordered fields. Moreover, there
are precise algorithms to compute the floor and the ceiling of n-th roots."""
license = "lgpl"
note = ""
[authors]
[authors.thiemann]
email = "thiemann_email"
[contributors]
[notify]
thiemann = "thiemann_email"
[history]
-2013-10-16 = """
-Added algorithms to compute floor and ceiling of sqrt of integers.
-"""
+2013-10-16 = "Added algorithms to compute floor and ceiling of sqrt of integers."
2014-07-11 = "Moved NthRoot_Impl from Real-Impl to this entry."
[extra]
[related]
diff --git a/metadata/entries/Well_Quasi_Orders.toml b/metadata/entries/Well_Quasi_Orders.toml
--- a/metadata/entries/Well_Quasi_Orders.toml
+++ b/metadata/entries/Well_Quasi_Orders.toml
@@ -1,60 +1,54 @@
title = "Well-Quasi-Orders"
date = 2012-04-13
topics = [
"Mathematics/Combinatorics",
]
abstract = """
Based on Isabelle/HOL's type class for preorders,
we introduce a type class for well-quasi-orders (wqo)
which is characterized by the absence of \"bad\" sequences
(our proofs are along the lines of the proof of Nash-Williams,
from which we also borrow terminology). Our main results are
instantiations for the product type, the list type, and a type of finite trees,
which (almost) directly follow from our proofs of (1) Dickson's Lemma, (2)
Higman's Lemma, and (3) Kruskal's Tree Theorem. More concretely: