diff --git a/web/entries/Knights_Tour.html b/web/entries/Knights_Tour.html --- a/web/entries/Knights_Tour.html +++ b/web/entries/Knights_Tour.html @@ -1,195 +1,195 @@ Knight's Tour Revisited Revisited - Archive of Formal Proofs

Knight's Tour Revisited Revisited

Title:	Knight's Tour Revisited Revisited
Author:	Lukas Koller (lukas /dot/ koller /at/ tum /dot/ de)
Submission date:	2022-01-04
Abstract:	-This is a formalization of the article "Knight's Tour Revisited" by +This is a formalization of the article Knight's Tour Revisited by Cull and De Curtins where they prove the existence of a Knight's -path for arbitrary n × m-boards with min(n,m) ≤ +path for arbitrary n × m-boards with min(n,m) ≥ 5. If n · m is even, then there exists a Knight's circuit. A Knight's Path is a sequence of moves of a Knight on a chessboard s.t. the Knight visits every square of a chessboard exactly once. Finding a Knight's path is a an instance of the Hamiltonian path problem. A Knight's circuit is a Knight's path, where additionally the Knight can move from the last square to the first square of the path, forming a loop. During the formalization two mistakes in the original proof were discovered. These mistakes are corrected in this formalization.
BibTeX:	@article{Knights_Tour-AFP, author = {Lukas Koller}, title = {Knight's Tour Revisited Revisited}, journal = {Archive of Formal Proofs}, month = jan, year = 2022, note = {\url{https://isa-afp.org/entries/Knights_Tour.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License

Proof outline
Proof document

Browse theories

Download this entry

Older releases: None

\ No newline at end of file diff --git a/web/rss.xml b/web/rss.xml --- a/web/rss.xml +++ b/web/rss.xml @@ -1,618 +1,618 @@ Archive of Formal Proofs https://www.isa-afp.org The Archive of Formal Proofs is a collection of proof libraries, examples, and larger scientific developments, mechanically checked in the theorem prover Isabelle. 04 Jan 2022 00:00:00 +0000 Knight's Tour Revisited Revisited https://www.isa-afp.org/entries/Knights_Tour.html https://www.isa-afp.org/entries/Knights_Tour.html Lukas Koller 04 Jan 2022 00:00:00 +0000 -This is a formalization of the article "Knight's Tour Revisited" by +This is a formalization of the article Knight's Tour Revisited by Cull and De Curtins where they prove the existence of a Knight's -path for arbitrary n × m-boards with min(n,m) ≤ +path for arbitrary n × m-boards with min(n,m) ≥ 5. If n · m is even, then there exists a Knight's circuit. A Knight's Path is a sequence of moves of a Knight on a chessboard s.t. the Knight visits every square of a chessboard exactly once. Finding a Knight's path is a an instance of the Hamiltonian path problem. A Knight's circuit is a Knight's path, where additionally the Knight can move from the last square to the first square of the path, forming a loop. During the formalization two mistakes in the original proof were discovered. These mistakes are corrected in this formalization. Hyperdual Numbers and Forward Differentiation https://www.isa-afp.org/entries/Hyperdual.html https://www.isa-afp.org/entries/Hyperdual.html Filip Smola, Jacques Fleuriot 31 Dec 2021 00:00:00 +0000 Hyperdual numbers are ones with a real component and a number of infinitesimal components, usually written as $a_0 + a_1 \cdot \epsilon_1 + a_2 \cdot \epsilon_2 + a_3 \cdot \epsilon_1\epsilon_2$. They have been proposed by <a href="https://doi.org/10.2514/6.2011-886">Fike and Alonso</a> in an approach to automatic differentiation. In this entry we formalise hyperdual numbers and their application to forward differentiation. We show them to be an instance of multiple algebraic structures and then, along with facts about twice-differentiability, we define what we call the hyperdual extensions of functions on real-normed fields. This extension formally represents the proposed way that the first and second derivatives of a function can be automatically calculated. We demonstrate it on the standard logistic function $f(x) = \frac{1}{1 + e^{-x}}$ and also reproduce the example analytic function $f(x) = \frac{e^x}{\sqrt{sin(x)^3 + cos(x)^3}}$ used for demonstration by Fike and Alonso. Gale-Shapley Algorithm https://www.isa-afp.org/entries/Gale_Shapley.html https://www.isa-afp.org/entries/Gale_Shapley.html Tobias Nipkow 29 Dec 2021 00:00:00 +0000 This is a stepwise refinement and proof of the Gale-Shapley stable matching (or marriage) algorithm down to executable code. Both a purely functional implementation based on lists and a functional implementation based on efficient arrays (provided by the Collections Framework in the AFP) are developed. The latter implementation runs in time O(n2) where n is the cardinality of the two sets to be matched. Roth's Theorem on Arithmetic Progressions https://www.isa-afp.org/entries/Roth_Arithmetic_Progressions.html https://www.isa-afp.org/entries/Roth_Arithmetic_Progressions.html Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson 28 Dec 2021 00:00:00 +0000 We formalise a proof of Roth's Theorem on Arithmetic Progressions, a major result in additive combinatorics on the existence of 3-term arithmetic progressions in subsets of natural numbers. To this end, we follow a proof using graph regularity. We employ our recent formalisation of Szemerédi's Regularity Lemma, a major result in extremal graph theory, which we use here to prove the Triangle Counting Lemma and the Triangle Removal Lemma. Our sources are Yufei Zhao's MIT lecture notes "<a href="https://ocw.mit.edu/courses/mathematics/18-217-graph-theory-and-additive-combinatorics-fall-2019/lecture-notes/MIT18_217F19_ch3.pdf">Graph Theory and Additive Combinatorics</a>" (revised version <a href="https://yufeizhao.com/gtac/gtac17.pdf">here</a>) and W.T. Gowers's Cambridge lecture notes "<a href="https://www.dpmms.cam.ac.uk/~par31/notes/tic.pdf">Topics in Combinatorics</a>". We also refer to the University of Georgia notes by Stephanie Bell and Will Grodzicki, "<a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.432.327">Using Szemerédi's Regularity Lemma to Prove Roth's Theorem</a>". Markov Decision Processes with Rewards https://www.isa-afp.org/entries/MDP-Rewards.html https://www.isa-afp.org/entries/MDP-Rewards.html Maximilian Schäffeler, Mohammad Abdulaziz 16 Dec 2021 00:00:00 +0000 We present a formalization of Markov Decision Processes with rewards. In particular we first build on Hölzl's formalization of MDPs (AFP entry: Markov_Models) and extend them with rewards. We proceed with an analysis of the expected total discounted reward criterion for infinite horizon MDPs. The central result is the construction of the iteration rule for the Bellman operator. We prove the optimality equations for this operator and show the existence of an optimal stationary deterministic solution. The analysis can be used to obtain dynamic programming algorithms such as value iteration and policy iteration to solve MDPs with formal guarantees. Our formalization is based on chapters 5 and 6 in Puterman's book "Markov Decision Processes: Discrete Stochastic Dynamic Programming". Verified Algorithms for Solving Markov Decision Processes https://www.isa-afp.org/entries/MDP-Algorithms.html https://www.isa-afp.org/entries/MDP-Algorithms.html Maximilian Schäffeler, Mohammad Abdulaziz 16 Dec 2021 00:00:00 +0000 We present a formalization of algorithms for solving Markov Decision Processes (MDPs) with formal guarantees on the optimality of their solutions. In particular we build on our analysis of the Bellman operator for discounted infinite horizon MDPs. From the iterator rule on the Bellman operator we directly derive executable value iteration and policy iteration algorithms to iteratively solve finite MDPs. We also prove correct optimized versions of value iteration that use matrix splittings to improve the convergence rate. In particular, we formally verify Gauss-Seidel value iteration and modified policy iteration. The algorithms are evaluated on two standard examples from the literature, namely, inventory management and gridworld. Our formalization covers most of chapter 6 in Puterman's book "Markov Decision Processes: Discrete Stochastic Dynamic Programming". Regular Tree Relations https://www.isa-afp.org/entries/Regular_Tree_Relations.html https://www.isa-afp.org/entries/Regular_Tree_Relations.html Alexander Lochmann, Bertram Felgenhauer, Christian Sternagel, René Thiemann, Thomas Sternagel 15 Dec 2021 00:00:00 +0000 Tree automata have good closure properties and therefore a commonly used to prove/disprove properties. This formalization contains among other things the proofs of many closure properties of tree automata (anchored) ground tree transducers and regular relations. Additionally it includes the well known pumping lemma and a lifting of the Myhill Nerode theorem for regular languages to tree languages. We want to mention the existence of a <a href="https://www.isa-afp.org/entries/Tree-Automata.html">tree automata APF-entry</a> developed by Peter Lammich. His work is based on epsilon free top-down tree automata, while this entry builds on bottom-up tree auotamta with epsilon transitions. Moreover our formalization relies on the <a href="https://www.isa-afp.org/entries/Collections.html">Collections Framework</a>, also by Peter Lammich, to obtain efficient code. All proven constructions of the closure properties are exportable using the Isabelle/HOL code generation facilities. Simplicial Complexes and Boolean functions https://www.isa-afp.org/entries/Simplicial_complexes_and_boolean_functions.html https://www.isa-afp.org/entries/Simplicial_complexes_and_boolean_functions.html Jesús Aransay, Alejandro del Campo, Julius Michaelis 29 Nov 2021 00:00:00 +0000 In this work we formalise the isomorphism between simplicial complexes of dimension $n$ and monotone Boolean functions in $n$ variables, mainly following the definitions and results as introduced by N. A. Scoville. We also take advantage of the AFP representation of <a href="https://www.isa-afp.org/entries/ROBDD.html">ROBDD</a> (Reduced Ordered Binary Decision Diagrams) to compute the ROBDD representation of a given simplicial complex (by means of the isomorphism to Boolean functions). Some examples of simplicial complexes and associated Boolean functions are also presented. van Emde Boas Trees https://www.isa-afp.org/entries/Van_Emde_Boas_Trees.html https://www.isa-afp.org/entries/Van_Emde_Boas_Trees.html Thomas Ammer, Peter Lammich 23 Nov 2021 00:00:00 +0000 The van Emde Boas tree or van Emde Boas priority queue is a data structure supporting membership test, insertion, predecessor and successor search, minimum and maximum determination and deletion in O(log log U) time, where U = 0,...,2n-1 is the overall range to be considered. The presented formalization follows Chapter 20 of the popular Introduction to Algorithms (3rd ed.) by Cormen, Leiserson, Rivest and Stein (CLRS), extending the list of formally verified CLRS algorithms. Our current formalization is based on the first author's bachelor's thesis. First, we prove correct a functional implementation, w.r.t. an abstract data type for sets. Apart from functional correctness, we show a resource bound, and runtime bounds w.r.t. manually defined timing functions for the operations. Next, we refine the operations to Imperative HOL with time, and show correctness and complexity. This yields a practically more efficient implementation, and eliminates the manually defined timing functions from the trusted base of the proof. Foundation of geometry in planes, and some complements: Excluding the parallel axioms https://www.isa-afp.org/entries/Foundation_of_geometry.html https://www.isa-afp.org/entries/Foundation_of_geometry.html Fumiya Iwama 22 Nov 2021 00:00:00 +0000 "Foundations of Geometry" is a mathematical book written by Hilbert in 1899. This entry is a complete formalization of "Incidence" (excluding cubic axioms), "Order" and "Congruence" (excluding point sequences) of the axioms constructed in this book. In addition, the theorem of the problem about the part that is treated implicitly and is not clearly stated in it is being carried out in parallel. The Hahn and Jordan Decomposition Theorems https://www.isa-afp.org/entries/Hahn_Jordan_Decomposition.html https://www.isa-afp.org/entries/Hahn_Jordan_Decomposition.html Marie Cousin, Mnacho Echenim, Hervé Guiol 19 Nov 2021 00:00:00 +0000 In this work we formalize the Hahn decomposition theorem for signed measures, namely that any measure space for a signed measure can be decomposed into a positive and a negative set, where every measurable subset of the positive one has a positive measure, and every measurable subset of the negative one has a negative measure. We also formalize the Jordan decomposition theorem as a corollary, which states that the signed measure under consideration admits a unique decomposition into a difference of two positive measures, at least one of which is finite. Exploring Simplified Variants of Gödel’s Ontological Argument in Isabelle/HOL https://www.isa-afp.org/entries/SimplifiedOntologicalArgument.html https://www.isa-afp.org/entries/SimplifiedOntologicalArgument.html Christoph Benzmüller 08 Nov 2021 00:00:00 +0000 Simplified variants of Gödel's ontological argument are explored. Among those is a particularly interesting simplified argument which is (i) valid already in basic modal logics K or KT, (ii) which does not suffer from modal collapse, and (iii) which avoids the rather complex predicates of essence (Ess.) and necessary existence (NE) as used by Gödel. Whether the presented variants increase or decrease the attractiveness and persuasiveness of the ontological argument is a question I would like to pass on to philosophy and theology. Real Exponents as the Limits of Sequences of Rational Exponents https://www.isa-afp.org/entries/Real_Power.html https://www.isa-afp.org/entries/Real_Power.html Jacques D. Fleuriot 08 Nov 2021 00:00:00 +0000 In this formalisation, we construct real exponents as the limits of sequences of rational exponents. In particular, if $a \ge 1$ and $x \in \mathbb{R}$, we choose an increasing rational sequence $r_n$ such that $\lim_{n\to\infty} {r_n} = x$. Then the sequence $a^{r_n}$ is increasing and if $r$ is any rational number such that $r > x$, $a^{r_n}$ is bounded above by $a^r$. By the convergence criterion for monotone sequences, $a^{r_n}$ converges. We define $a^ x = \lim_{n\to\infty} a^{r_n}$ and show that it has the expected properties (for $a \ge 0$). This particular construction of real exponents is needed instead of the usual one using the natural logarithm and exponential functions (which already exists in Isabelle) to support our mechanical derivation of Euler's exponential series as an ``infinite polynomial". Aside from helping us avoid circular reasoning, this is, as far as we are aware, the first time real exponents are mechanised in this way within a proof assistant. Automating Public Announcement Logic and the Wise Men Puzzle in Isabelle/HOL https://www.isa-afp.org/entries/PAL.html https://www.isa-afp.org/entries/PAL.html Christoph Benzmüller, Sebastian Reiche 08 Nov 2021 00:00:00 +0000 We present a shallow embedding of public announcement logic (PAL) with relativized general knowledge in HOL. We then use PAL to obtain an elegant encoding of the wise men puzzle, which we solve automatically using sledgehammer. Factorization of Polynomials with Algebraic Coefficients https://www.isa-afp.org/entries/Factor_Algebraic_Polynomial.html https://www.isa-afp.org/entries/Factor_Algebraic_Polynomial.html Manuel Eberl, René Thiemann 08 Nov 2021 00:00:00 +0000 The AFP already contains a verified implementation of algebraic numbers. However, it is has a severe limitation in its factorization algorithm of real and complex polynomials: the factorization is only guaranteed to succeed if the coefficients of the polynomial are rational numbers. In this work, we verify an algorithm to factor all real and complex polynomials whose coefficients are algebraic. The existence of such an algorithm proves in a constructive way that the set of complex algebraic numbers is algebraically closed. Internally, the algorithm is based on resultants of multivariate polynomials and an approximation algorithm using interval arithmetic. Szemerédi's Regularity Lemma https://www.isa-afp.org/entries/Szemeredi_Regularity.html https://www.isa-afp.org/entries/Szemeredi_Regularity.html Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson 05 Nov 2021 00:00:00 +0000 <a href="https://en.wikipedia.org/wiki/Szemerédi_regularity_lemma">Szemerédi's regularity lemma</a> is a key result in the study of large graphs. It asserts the existence of an upper bound on the number of parts the vertices of a graph need to be partitioned into such that the edges between the parts are random in a certain sense. This bound depends only on the desired precision and not on the graph itself, in the spirit of Ramsey's theorem. The formalisation follows online course notes by <a href="https://www.dpmms.cam.ac.uk/~par31/notes/tic.pdf">Tim Gowers</a> and <a href="https://yufeizhao.com/gtac/gtac.pdf">Yufei Zhao</a>. Quantum and Classical Registers https://www.isa-afp.org/entries/Registers.html https://www.isa-afp.org/entries/Registers.html Dominique Unruh 28 Oct 2021 00:00:00 +0000 A formalization of the theory of quantum and classical registers as developed by (Unruh, Quantum and Classical Registers). In a nutshell, a register refers to a part of a larger memory or system that can be accessed independently. Registers can be constructed from other registers and several (compatible) registers can be composed. This formalization develops both the generic theory of registers as well as specific instantiations for classical and quantum registers. Belief Revision Theory https://www.isa-afp.org/entries/Belief_Revision.html https://www.isa-afp.org/entries/Belief_Revision.html Valentin Fouillard, Safouan Taha, Frédéric Boulanger, Nicolas Sabouret 19 Oct 2021 00:00:00 +0000 The 1985 paper by Carlos Alchourrón, Peter Gärdenfors, and David Makinson (AGM), “On the Logic of Theory Change: Partial Meet Contraction and Revision Functions” launches a large and rapidly growing literature that employs formal models and logics to handle changing beliefs of a rational agent and to take into account new piece of information observed by this agent. In 2011, a review book titled "AGM 25 Years: Twenty-Five Years of Research in Belief Change" was edited to summarize the first twenty five years of works based on AGM. This HOL-based AFP entry is a faithful formalization of the AGM operators (e.g. contraction, revision, remainder ...) axiomatized in the original paper. It also contains the proofs of all the theorems stated in the paper that show how these operators combine. Both proofs of Harper and Levi identities are established. X86 instruction semantics and basic block symbolic execution https://www.isa-afp.org/entries/X86_Semantics.html https://www.isa-afp.org/entries/X86_Semantics.html Freek Verbeek, Abhijith Bharadwaj, Joshua Bockenek, Ian Roessle, Timmy Weerwag, Binoy Ravindran 13 Oct 2021 00:00:00 +0000 This AFP entry provides semantics for roughly 120 different X86-64 assembly instructions. These instructions include various moves, arithmetic/logical operations, jumps, call/return, SIMD extensions and others. External functions are supported by allowing a user to provide custom semantics for these calls. Floating-point operations are mapped to uninterpreted functions. The model provides semantics for register aliasing and a byte-level little-endian memory model. The semantics are purposefully incomplete, but overapproximative. For example, the precise effect of flags may be undefined for certain instructions, or instructions may simply have no semantics at all. In those cases, the semantics are mapped to universally quantified uninterpreted terms from a locale. Second, this entry provides a method to symbolic execution of basic blocks. The method, called ''se_step'' (for: symbolic execution step) fetches an instruction and updates the current symbolic state while keeping track of assumptions made over the memory model. A key component is a set of theorems that prove how reads from memory resolve after writes have occurred. Thirdly, this entry provides a parser that allows the user to copy-paste the output of the standard disassembly tool objdump into Isabelle/HOL. A couple small and explanatory examples are included, including functions from the word count program. Several examples can be supplied upon request (they are not included due to the running time of verification): functions from the floating-point modulo function from FDLIBM, the GLIBC strlen function and the CoreUtils SHA256 implementation. Algebras for Iteration, Infinite Executions and Correctness of Sequential Computations https://www.isa-afp.org/entries/Correctness_Algebras.html https://www.isa-afp.org/entries/Correctness_Algebras.html Walter Guttmann 12 Oct 2021 00:00:00 +0000 We study models of state-based non-deterministic sequential computations and describe them using algebras. We propose algebras that describe iteration for strict and non-strict computations. They unify computation models which differ in the fixpoints used to represent iteration. We propose algebras that describe the infinite executions of a computation. They lead to a unified approximation order and results that connect fixpoints in the approximation and refinement orders. This unifies the semantics of recursion for a range of computation models. We propose algebras that describe preconditions and the effect of while-programs under postconditions. They unify correctness statements in two dimensions: one statement applies in various computation models to various correctness claims. Verified Quadratic Virtual Substitution for Real Arithmetic https://www.isa-afp.org/entries/Virtual_Substitution.html https://www.isa-afp.org/entries/Virtual_Substitution.html Matias Scharager, Katherine Cordwell, Stefan Mitsch, André Platzer 02 Oct 2021 00:00:00 +0000 This paper presents a formally verified quantifier elimination (QE) algorithm for first-order real arithmetic by linear and quadratic virtual substitution (VS) in Isabelle/HOL. The Tarski-Seidenberg theorem established that the first-order logic of real arithmetic is decidable by QE. However, in practice, QE algorithms are highly complicated and often combine multiple methods for performance. VS is a practically successful method for QE that targets formulas with low-degree polynomials. To our knowledge, this is the first work to formalize VS for quadratic real arithmetic including inequalities. The proofs necessitate various contributions to the existing multivariate polynomial libraries in Isabelle/HOL. Our framework is modularized and easily expandable (to facilitate integrating future optimizations), and could serve as a basis for developing practical general-purpose QE algorithms. Further, as our formalization is designed with practicality in mind, we export our development to SML and test the resulting code on 378 benchmarks from the literature, comparing to Redlog, Z3, Wolfram Engine, and SMT-RAT. This identified inconsistencies in some tools, underscoring the significance of a verified approach for the intricacies of real arithmetic. Soundness and Completeness of an Axiomatic System for First-Order Logic https://www.isa-afp.org/entries/FOL_Axiomatic.html https://www.isa-afp.org/entries/FOL_Axiomatic.html Asta Halkjær From 24 Sep 2021 00:00:00 +0000 This work is a formalization of the soundness and completeness of an axiomatic system for first-order logic. The proof system is based on System Q1 by Smullyan and the completeness proof follows his textbook "First-Order Logic" (Springer-Verlag 1968). The completeness proof is in the Henkin style where a consistent set is extended to a maximal consistent set using Lindenbaum's construction and Henkin witnesses are added during the construction to ensure saturation as well. The resulting set is a Hintikka set which, by the model existence theorem, is satisfiable in the Herbrand universe. Complex Bounded Operators https://www.isa-afp.org/entries/Complex_Bounded_Operators.html https://www.isa-afp.org/entries/Complex_Bounded_Operators.html Jose Manuel Rodriguez Caballero, Dominique Unruh 18 Sep 2021 00:00:00 +0000 We present a formalization of bounded operators on complex vector spaces. Our formalization contains material on complex vector spaces (normed spaces, Banach spaces, Hilbert spaces) that complements and goes beyond the developments of real vectors spaces in the Isabelle/HOL standard library. We define the type of bounded operators between complex vector spaces (cblinfun) and develop the theory of unitaries, projectors, extension of bounded linear functions (BLT theorem), adjoints, Loewner order, closed subspaces and more. For the finite-dimensional case, we provide code generation support by identifying finite-dimensional operators with matrices as formalized in the <a href="Jordan_Normal_Form.html">Jordan_Normal_Form</a> AFP entry. A Formalization of Weighted Path Orders and Recursive Path Orders https://www.isa-afp.org/entries/Weighted_Path_Order.html https://www.isa-afp.org/entries/Weighted_Path_Order.html Christian Sternagel, René Thiemann, Akihisa Yamada 16 Sep 2021 00:00:00 +0000 We define the weighted path order (WPO) and formalize several properties such as strong normalization, the subterm property, and closure properties under substitutions and contexts. Our definition of WPO extends the original definition by also permitting multiset comparisons of arguments instead of just lexicographic extensions. Therefore, our WPO not only subsumes lexicographic path orders (LPO), but also recursive path orders (RPO). We formally prove these subsumptions and therefore all of the mentioned properties of WPO are automatically transferable to LPO and RPO as well. Such a transformation is not required for Knuth–Bendix orders (KBO), since they have already been formalized. Nevertheless, we still provide a proof that WPO subsumes KBO and thereby underline the generality of WPO. Extension of Types-To-Sets https://www.isa-afp.org/entries/Types_To_Sets_Extension.html https://www.isa-afp.org/entries/Types_To_Sets_Extension.html Mihails Milehins 06 Sep 2021 00:00:00 +0000 In their article titled From Types to Sets by Local Type Definitions in Higher-Order Logic and published in the proceedings of the conference Interactive Theorem Proving in 2016, Ondřej Kunčar and Andrei Popescu propose an extension of the logic Isabelle/HOL and an associated algorithm for the relativization of the type-based theorems to more flexible set-based theorems, collectively referred to as Types-To-Sets. One of the aims of their work was to open an opportunity for the development of a software tool for applied relativization in the implementation of the logic Isabelle/HOL of the proof assistant Isabelle. In this article, we provide a prototype of a software framework for the interactive automated relativization of theorems in Isabelle/HOL, developed as an extension of the proof language Isabelle/Isar. The software framework incorporates the implementation of the proposed extension of the logic, and builds upon some of the ideas for further work expressed in the original article on Types-To-Sets by Ondřej Kunčar and Andrei Popescu and the subsequent article Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL that was written by Fabian Immler and Bohua Zhan and published in the proceedings of the International Conference on Certified Programs and Proofs in 2019. IDE: Introduction, Destruction, Elimination https://www.isa-afp.org/entries/Intro_Dest_Elim.html https://www.isa-afp.org/entries/Intro_Dest_Elim.html Mihails Milehins 06 Sep 2021 00:00:00 +0000 The article provides the command mk_ide for the object logic Isabelle/HOL of the formal proof assistant Isabelle. The command mk_ide enables the automated synthesis of the introduction, destruction and elimination rules from arbitrary definitions of constant predicates stated in Isabelle/HOL. Conditional Transfer Rule https://www.isa-afp.org/entries/Conditional_Transfer_Rule.html https://www.isa-afp.org/entries/Conditional_Transfer_Rule.html Mihails Milehins 06 Sep 2021 00:00:00 +0000 This article provides a collection of experimental utilities for unoverloading of definitions and synthesis of conditional transfer rules for the object logic Isabelle/HOL of the formal proof assistant Isabelle written in Isabelle/ML. Conditional Simplification https://www.isa-afp.org/entries/Conditional_Simplification.html https://www.isa-afp.org/entries/Conditional_Simplification.html Mihails Milehins 06 Sep 2021 00:00:00 +0000 The article provides a collection of experimental general-purpose proof methods for the object logic Isabelle/HOL of the formal proof assistant Isabelle. The methods in the collection offer functionality that is similar to certain aspects of the functionality provided by the standard proof methods of Isabelle that combine classical reasoning and rewriting, such as the method auto, but use a different approach for rewriting. More specifically, these methods allow for the side conditions of the rewrite rules to be solved via intro-resolution. Category Theory for ZFC in HOL III: Universal Constructions https://www.isa-afp.org/entries/CZH_Universal_Constructions.html https://www.isa-afp.org/entries/CZH_Universal_Constructions.html Mihails Milehins 06 Sep 2021 00:00:00 +0000 The article provides a formalization of elements of the theory of universal constructions for 1-categories (such as limits, adjoints and Kan extensions) in the object logic ZFC in HOL of the formal proof assistant Isabelle. The article builds upon the foundations established in the AFP entry Category Theory for ZFC in HOL II: Elementary Theory of 1-Categories. Category Theory for ZFC in HOL I: Foundations: Design Patterns, Set Theory, Digraphs, Semicategories https://www.isa-afp.org/entries/CZH_Foundations.html https://www.isa-afp.org/entries/CZH_Foundations.html Mihails Milehins 06 Sep 2021 00:00:00 +0000 This article provides a foundational framework for the formalization of category theory in the object logic ZFC in HOL of the formal proof assistant Isabelle. More specifically, this article provides a formalization of canonical set-theoretic constructions internalized in the type V associated with the ZFC in HOL, establishes a design pattern for the formalization of mathematical structures using sequences and locales, and showcases the developed infrastructure by providing formalizations of the elementary theories of digraphs and semicategories. The methodology chosen for the formalization of the theories of digraphs and semicategories (and categories in future articles) rests on the ideas that were originally expressed in the article Set-Theoretical Foundations of Category Theory written by Solomon Feferman and Georg Kreisel. Thus, in the context of this work, each of the aforementioned mathematical structures is represented as a term of the type V embedded into a stage of the von Neumann hierarchy. diff --git a/web/statistics.html b/web/statistics.html --- a/web/statistics.html +++ b/web/statistics.html @@ -1,303 +1,303 @@ Archive of Formal Proofs

Statistics

- +

Number of Articles:	651
Number of Authors:	419
Number of lemmas:	~191,200
Lines of Code:	~3,299,900
Lines of Code:	~3,299,700

Most used AFP articles:

	Name	Used by ? articles
1.	List-Index	20
2.	Show	14
3.	Collections	13
4.	Coinductive	12
	Jordan_Normal_Form	12
	Regular-Sets	12
5.	Landau_Symbols	11
	Polynomial_Factorization	11
6.	Abstract-Rewriting	10
	Automatic_Refinement	10
	Deriving	10

Knight's Tour Revisited Revisited

Statistics

Statistics

Most used AFP articles:

Growth in number of articles:

Growth in lines of code:

Growth in number of authors:

Size of articles: