Archive of Formal Proofs

Verified SAT-Based AI Planning

Mohammad Abdulaziz, Friedrich Kurz — 29 Oct 2020 00:00:00 +0000

We present an executable formally verified SAT encoding of classical AI planning that is based on the encodings by Kautz and Selman and the one by Rintanen et al. The encoding was experimentally tested and shown to be usable for reasonably sized standard AI planning benchmarks. We also use it as a reference to test a state-of-the-art SAT-based planner, showing that it sometimes falsely claims that problems have no solutions of certain lengths. The formalisation in this submission was described in an independent publication.

AI Planning Languages Semantics

Mohammad Abdulaziz, Peter Lammich — 29 Oct 2020 00:00:00 +0000

This is an Isabelle/HOL formalisation of the semantics of the multi-valued planning tasks language that is used by the planning system Fast-Downward, the STRIPS fragment of the Planning Domain Definition Language (PDDL), and the STRIPS soundness meta-theory developed by Vladimir Lifschitz. It also contains formally verified checkers for checking the well-formedness of problems specified in either language as well the correctness of potential solutions. The formalisation in this entry was described in an earlier publication.

A Sound Type System for Physical Quantities, Units, and Measurements

Simon Foster, Burkhart Wolff — 20 Oct 2020 00:00:00 +0000

The present Isabelle theory builds a formal model for both the International System of Quantities (ISQ) and the International System of Units (SI), which are both fundamental for physics and engineering. Both the ISQ and the SI are deeply integrated into Isabelle's type system. Quantities are parameterised by dimension types, which correspond to base vectors, and thus only quantities of the same dimension can be equated. Since the underlying "algebra of quantities" induces congruences on quantity and SI types, specific tactic support is developed to capture these. Our construction is validated by a test-set of known equivalences between both quantities and SI units. Moreover, the presented theory can be used for type-safe conversions between the SI system and others, like the British Imperial System (BIS).

A Formal Model of the Safely Composable Document Object Model with Shadow Roots

Achim D. Brucker, Michael Herzberg — 28 Sep 2020 00:00:00 +0000

In this AFP entry, we extend our formalization of the safely composable DOM with Shadow Roots. This is a proposal for Shadow Roots with stricter safety guarantess than the standard compliant formalization (see "Shadow DOM"). Shadow Roots are a recent proposal of the web community to support a component-based development approach for client-side web applications. Shadow roots are a significant extension to the DOM standard and, as web standards are condemned to be backward compatible, such extensions often result in complex specification that may contain unwanted subtleties that can be detected by a formalization. Our Isabelle/HOL formalization is, in the sense of object-orientation, an extension of our formalization of the core DOM and enjoys the same basic properties, i.e., it is extensible, i.e., can be extended without the need of re-proving already proven properties and executable, i.e., we can generate executable code from our specification. We exploit the executability to show that our formalization complies to the official standard of the W3C, respectively, the WHATWG.

A Formal Model of the Document Object Model with Shadow Roots

Achim D. Brucker, Michael Herzberg — 28 Sep 2020 00:00:00 +0000

In this AFP entry, we extend our formalization of the core DOM with Shadow Roots. Shadow roots are a recent proposal of the web community to support a component-based development approach for client-side web applications. Shadow roots are a significant extension to the DOM standard and, as web standards are condemned to be backward compatible, such extensions often result in complex specification that may contain unwanted subtleties that can be detected by a formalization. Our Isabelle/HOL formalization is, in the sense of object-orientation, an extension of our formalization of the core DOM and enjoys the same basic properties, i.e., it is extensible, i.e., can be extended without the need of re-proving already proven properties and executable, i.e., we can generate executable code from our specification. We exploit the executability to show that our formalization complies to the official standard of the W3C, respectively, the WHATWG.

A Formalization of Safely Composable Web Components

Achim D. Brucker, Michael Herzberg — 28 Sep 2020 00:00:00 +0000

While the (safely composable) DOM with shadow trees provide the technical basis for defining web components, it does neither defines the concept of web components nor specifies the safety properties that web components should guarantee. Consequently, the standard also does not discuss how or even if the methods for modifying the DOM respect component boundaries. In AFP entry, we present a formally verified model of safely composable web components and define safety properties which ensure that different web components can only interact with each other using well-defined interfaces. Moreover, our verification of the application programming interface (API) of the DOM revealed numerous invariants that implementations of the DOM API need to preserve to ensure the integrity of components. In comparison to the strict standard compliance formalization of Web Components in the AFP entry "DOM_Components", the notion of components in this entry (based on "SC_DOM" and "Shadow_SC_DOM") provides much stronger safety guarantees.

A Formalization of Web Components

Achim D. Brucker, Michael Herzberg — 28 Sep 2020 00:00:00 +0000

While the DOM with shadow trees provide the technical basis for defining web components, the DOM standard neither defines the concept of web components nor specifies the safety properties that web components should guarantee. Consequently, the standard also does not discuss how or even if the methods for modifying the DOM respect component boundaries. In AFP entry, we present a formally verified model of web components and define safety properties which ensure that different web components can only interact with each other using well-defined interfaces. Moreover, our verification of the application programming interface (API) of the DOM revealed numerous invariants that implementations of the DOM API need to preserve to ensure the integrity of components.

The Safely Composable DOM

Achim D. Brucker, Michael Herzberg — 28 Sep 2020 00:00:00 +0000

In this AFP entry, we formalize the core of the Safely Composable Document Object Model (SC DOM). The SC DOM improve the standard DOM (as formalized in the AFP entry "Core DOM") by strengthening the tree boundaries set by shadow roots: in the SC DOM, the shadow root is a sub-class of the document class (instead of a base class). This modifications also results in changes to some API methods (e.g., getOwnerDocument) to return the nearest shadow root rather than the document root. As a result, many API methods that, when called on a node inside a shadow tree, would previously ``break out'' and return or modify nodes that are possibly outside the shadow tree, now stay within its boundaries. This change in behavior makes programs that operate on shadow trees more predictable for the developer and allows them to make more assumptions about other code accessing the DOM.

Syntax-Independent Logic Infrastructure

Andrei Popescu, Dmitriy Traytel — 16 Sep 2020 00:00:00 +0000

We formalize a notion of logic whose terms and formulas are kept abstract. In particular, logical connectives, substitution, free variables, and provability are not defined, but characterized by their general properties as locale assumptions. Based on this abstract characterization, we develop further reusable reasoning infrastructure. For example, we define parallel substitution (along with proving its characterizing theorems) from single-point substitution. Similarly, we develop a natural deduction style proof system starting from the abstract Hilbert-style one. These one-time efforts benefit different concrete logics satisfying our locales' assumptions. We instantiate the syntax-independent logic infrastructure to Robinson arithmetic (also known as Q) in the AFP entry Robinson_Arithmetic and to hereditarily finite set theory in the AFP entries Goedel_HFSet_Semantic and Goedel_HFSet_Semanticless, which are part of our formalization of Gödel's Incompleteness Theorems described in our CADE-27 paper A Formally Verified Abstract Account of Gödel's Incompleteness Theorems.

Robinson Arithmetic

Andrei Popescu, Dmitriy Traytel — 16 Sep 2020 00:00:00 +0000

We instantiate our syntax-independent logic infrastructure developed in a separate AFP entry to the FOL theory of Robinson arithmetic (also known as Q). The latter was formalised using Nominal Isabelle by adapting Larry Paulson’s formalization of the Hereditarily Finite Set theory.

An Abstract Formalization of Gödel's Incompleteness Theorems

Andrei Popescu, Dmitriy Traytel — 16 Sep 2020 00:00:00 +0000

We present an abstract formalization of Gödel's incompleteness theorems. We analyze sufficient conditions for the theorems' applicability to a partially specified logic. Our abstract perspective enables a comparison between alternative approaches from the literature. These include Rosser's variation of the first theorem, Jeroslow's variation of the second theorem, and the Swierczkowski–Paulson semantics-based approach. This AFP entry is the main entry point to the results described in our CADE-27 paper A Formally Verified Abstract Account of Gödel's Incompleteness Theorems. As part of our abstract formalization's validation, we instantiate our locales twice in the separate AFP entries Goedel_HFSet_Semantic and Goedel_HFSet_Semanticless.

From Abstract to Concrete Gödel's Incompleteness Theorems—Part II

Andrei Popescu, Dmitriy Traytel — 16 Sep 2020 00:00:00 +0000

We validate an abstract formulation of Gödel's Second Incompleteness Theorem from a separate AFP entry by instantiating it to the case of finite consistent extensions of the Hereditarily Finite (HF) Set theory, i.e., consistent FOL theories extending the HF Set theory with a finite set of axioms. The instantiation draws heavily on infrastructure previously developed by Larry Paulson in his direct formalisation of the concrete result. It strengthens Paulson's formalization of Gödel's Second from that entry by not assuming soundness, and in fact not relying on any notion of model or semantic interpretation. The strengthening was obtained by first replacing some of Paulson’s semantic arguments with proofs within his HF calculus, and then plugging in some of Paulson's (modified) lemmas to instantiate our soundness-free Gödel's Second locale.

From Abstract to Concrete Gödel's Incompleteness Theorems—Part I

Andrei Popescu, Dmitriy Traytel — 16 Sep 2020 00:00:00 +0000

We validate an abstract formulation of Gödel's First and Second Incompleteness Theorems from a separate AFP entry by instantiating them to the case of finite sound extensions of the Hereditarily Finite (HF) Set theory, i.e., FOL theories extending the HF Set theory with a finite set of axioms that are sound in the standard model. The concrete results had been previously formalised in an AFP entry by Larry Paulson; our instantiation reuses the infrastructure developed in that entry.

A Formal Model of Extended Finite State Machines

Michael Foster, Achim D. Brucker, Ramsay G. Taylor, John Derrick — 07 Sep 2020 00:00:00 +0000

In this AFP entry, we provide a formalisation of extended finite state machines (EFSMs) where models are represented as finite sets of transitions between states. EFSMs execute traces to produce observable outputs. We also define various simulation and equality metrics for EFSMs in terms of traces and prove their strengths in relation to each other. Another key contribution is a framework of function definitions such that LTL properties can be phrased over EFSMs. Finally, we provide a simple example case study in the form of a drinks machine.

Inference of Extended Finite State Machines

Michael Foster, Achim D. Brucker, Ramsay G. Taylor, John Derrick — 07 Sep 2020 00:00:00 +0000

In this AFP entry, we provide a formal implementation of a state-merging technique to infer extended finite state machines (EFSMs), complete with output and update functions, from black-box traces. In particular, we define the subsumption in context relation as a means of determining whether one transition is able to account for the behaviour of another. Building on this, we define the direct subsumption relation, which lifts the subsumption in context relation to EFSM level such that we can use it to determine whether it is safe to merge a given pair of transitions. Key proofs include the conditions necessary for subsumption to occur and that subsumption and direct subsumption are preorder relations. We also provide a number of different heuristics which can be used to abstract away concrete values into registers so that more states and transitions can be merged and provide proofs of the various conditions which must hold for these abstractions to subsume their ungeneralised counterparts. A Code Generator setup to create executable Scala code is also defined.

Practical Algebraic Calculus Checker

Mathias Fleury, Daniela Kaufmann — 31 Aug 2020 00:00:00 +0000

Generating and checking proof certificates is important to increase the trust in automated reasoning tools. In recent years formal verification using computer algebra became more important and is heavily used in automated circuit verification. An existing proof format which covers algebraic reasoning and allows efficient proof checking is the practical algebraic calculus (PAC). In this development, we present the verified checker Pastèque that is obtained by synthesis via the Refinement Framework. This is the formalization going with our FMCAD'20 tool presentation.

Some classical results in inductive inference of recursive functions

Frank J. Balbach — 31 Aug 2020 00:00:00 +0000

This entry formalizes some classical concepts and results from inductive inference of recursive functions. In the basic setting a partial recursive function ("strategy") must identify ("learn") all functions from a set ("class") of recursive functions. To that end the strategy receives more and more values $f(0), f(1), f(2), \ldots$ of some function $f$ from the given class and in turn outputs descriptions of partial recursive functions, for example, Gödel numbers. The strategy is considered successful if the sequence of outputs ("hypotheses") converges to a description of $f$. A class of functions learnable in this sense is called "learnable in the limit". The set of all these classes is denoted by LIM.

Other types of inference considered are finite learning (FIN), behaviorally correct learning in the limit (BC), and some variants of LIM with restrictions on the hypotheses: total learning (TOTAL), consistent learning (CONS), and class-preserving learning (CP). The main results formalized are the proper inclusions $\mathrm{FIN} \subset \mathrm{CP} \subset \mathrm{TOTAL} \subset \mathrm{CONS} \subset \mathrm{LIM} \subset \mathrm{BC} \subset 2^{\mathcal{R}}$, where $\mathcal{R}$ is the set of all total recursive functions. Further results show that for all these inference types except CONS, strategies can be assumed to be total recursive functions; that all inference types but CP are closed under the subset relation between classes; and that no inference type is closed under the union of classes.

The above is based on a formalization of recursive functions heavily inspired by the Universal Turing Machine entry by Xu et al., but different in that it models partial functions with codomain nat option. The formalization contains a construction of a universal partial recursive function, without resorting to Turing machines, introduces decidability and recursive enumerability, and proves some standard results: existence of a Kleene normal form, the s-m-n theorem, Rice's theorem, and assorted fixed-point theorems (recursion theorems) by Kleene, Rogers, and Smullyan.

Relational Disjoint-Set Forests

Walter Guttmann — 26 Aug 2020 00:00:00 +0000

We give a simple relation-algebraic semantics of read and write operations on associative arrays. The array operations seamlessly integrate with assignments in the Hoare-logic library. Using relation algebras and Kleene algebras we verify the correctness of an array-based implementation of disjoint-set forests with a naive union operation and a find operation with path compression.

Extensions to the Comprehensive Framework for Saturation Theorem Proving

Jasmin Blanchette, Sophie Tourret — 25 Aug 2020 00:00:00 +0000

This Isabelle/HOL formalization extends the AFP entry Saturation_Framework with the following contributions:

an application of the framework to prove Bachmair and Ganzinger's resolution prover RP refutationally complete, which was formalized in a more ad hoc fashion by Schlichtkrull et al. in the AFP entry Ordered_Resultion_Prover;
generalizations of various basic concepts formalized by Schlichtkrull et al., which were needed to verify RP and could be useful to formalize other calculi, such as superposition;
alternative proofs of fairness (and hence saturation and ultimately refutational completeness) for the given clause procedures GC and LGC, based on invariance.

Putting the `K' into Bird's derivation of Knuth-Morris-Pratt string matching

Peter Gammie — 25 Aug 2020 00:00:00 +0000

Richard Bird and collaborators have proposed a derivation of an intricate cyclic program that implements the Morris-Pratt string matching algorithm. Here we provide a proof of total correctness for Bird's derivation and complete it by adding Knuth's optimisation.

Amicable Numbers

Angeliki Koutsoukou-Argyraki — 04 Aug 2020 00:00:00 +0000

This is a formalisation of Amicable Numbers, involving some relevant material including Euler's sigma function, some relevant definitions, results and examples as well as rules such as Thābit ibn Qurra's Rule, Euler's Rule, te Riele's Rule and Borho's Rule with breeders.

Ordinal Partitions

Lawrence C. Paulson — 03 Aug 2020 00:00:00 +0000

The theory of partition relations concerns generalisations of Ramsey's theorem. For any ordinal $\alpha$, write $\alpha \to (\alpha, m)^2$ if for each function $f$ from unordered pairs of elements of $\alpha$ into $\{0,1\}$, either there is a subset $X\subseteq \alpha$ order-isomorphic to $\alpha$ such that $f\{x,y\}=0$ for all $\{x,y\}\subseteq X$, or there is an $m$ element set $Y\subseteq \alpha$ such that $f\{x,y\}=1$ for all $\{x,y\}\subseteq Y$. (In both cases, with $\{x,y\}$ we require $x\not=y$.) In particular, the infinite Ramsey theorem can be written in this notation as $\omega \to (\omega, \omega)^2$, or if we restrict $m$ to the positive integers as above, then $\omega \to (\omega, m)^2$ for all $m$. This entry formalises Larson's proof of $\omega^\omega \to (\omega^\omega, m)^2$ along with a similar proof of a result due to Specker: $\omega^2 \to (\omega^2, m)^2$. Also proved is a necessary result by Erdős and Milner: $\omega^{1+\alpha\cdot n} \to (\omega^{1+\alpha}, 2^n)^2$.

A Formal Proof of The Chandy--Lamport Distributed Snapshot Algorithm

Ben Fiedler, Dmitriy Traytel — 21 Jul 2020 00:00:00 +0000

We provide a suitable distributed system model and implementation of the Chandy--Lamport distributed snapshot algorithm [ACM Transactions on Computer Systems, 3, 63-75, 1985]. Our main result is a formal termination and correctness proof of the Chandy--Lamport algorithm and its use in stable property detection.

Relational Characterisations of Paths

Walter Guttmann, Peter Höfner — 13 Jul 2020 00:00:00 +0000

Binary relations are one of the standard ways to encode, characterise and reason about graphs. Relation algebras provide equational axioms for a large fragment of the calculus of binary relations. Although relations are standard tools in many areas of mathematics and computing, researchers usually fall back to point-wise reasoning when it comes to arguments about paths in a graph. We present a purely algebraic way to specify different kinds of paths in Kleene relation algebras, which are relation algebras equipped with an operation for reflexive transitive closure. We study the relationship between paths with a designated root vertex and paths without such a vertex. Since we stay in first-order logic this development helps with mechanising proofs. To demonstrate the applicability of the algebraic framework we verify the correctness of three basic graph algorithms.

A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles

Albert Rizaldi, Fabian Immler — 01 Jun 2020 00:00:00 +0000

The Vienna Convention on Road Traffic defines the safe distance traffic rules informally. This could make autonomous vehicle liable for safe-distance-related accidents because there is no clear definition of how large a safe distance is. We provide a formally proven prescriptive definition of a safe distance, and checkers which can decide whether an autonomous vehicle is obeying the safe distance rule. Not only does our work apply to the domain of law, but it also serves as a specification for autonomous vehicle manufacturers and for online verification of path planners.

A verified algorithm for computing the Smith normal form of a matrix

Jose Divasón — 23 May 2020 00:00:00 +0000

This work presents a formal proof in Isabelle/HOL of an algorithm to transform a matrix into its Smith normal form, a canonical matrix form, in a general setting: the algorithm is parameterized by operations to prove its existence over elementary divisor rings, while execution is guaranteed over Euclidean domains. We also provide a formal proof on some results about the generality of this algorithm as well as the uniqueness of the Smith normal form. Since Isabelle/HOL does not feature dependent types, the development is carried out switching conveniently between two different existing libraries: the Hermite normal form (based on HOL Analysis) and the Jordan normal form AFP entries. This permits to reuse results from both developments and it is done by means of the lifting and transfer package together with the use of local type definitions.

The Nash-Williams Partition Theorem

Lawrence C. Paulson — 16 May 2020 00:00:00 +0000

In 1965, Nash-Williams discovered a generalisation of the infinite form of Ramsey's theorem. Where the latter concerns infinite sets of n-element sets for some fixed n, the Nash-Williams theorem concerns infinite sets of finite sets (or lists) subject to a “no initial segment” condition. The present formalisation follows a monograph on Ramsey Spaces by Todorčević.

A Formalization of Knuth–Bendix Orders

Christian Sternagel, René Thiemann — 13 May 2020 00:00:00 +0000

We define a generalized version of Knuth–Bendix orders, including subterm coefficient functions. For these orders we formalize several properties such as strong normalization, the subterm property, closure properties under substitutions and contexts, as well as ground totality.

Irrationality Criteria for Series by Erdős and Straus

Angeliki Koutsoukou-Argyraki, Wenda Li — 12 May 2020 00:00:00 +0000

We formalise certain irrationality criteria for infinite series of the form: \[\sum_{n=1}^\infty \frac{b_n}{\prod_{i=1}^n a_i} \] where $\{b_n\}$ is a sequence of integers and $\{a_n\}$ a sequence of positive integers with $a_n >1$ for all large n. The results are due to P. Erdős and E. G. Straus [1]. In particular, we formalise Theorem 2.1, Corollary 2.10 and Theorem 3.1. The latter is an application of Theorem 2.1 involving the prime numbers.

Recursion Theorem in ZF

Georgy Dunaev — 11 May 2020 00:00:00 +0000

This document contains a proof of the recursion theorem. This is a mechanization of the proof of the recursion theorem from the text Introduction to Set Theory, by Karel Hrbacek and Thomas Jech. This implementation may be used as the basis for a model of Peano arithmetic in ZF. While recursion and the natural numbers are already available in Isabelle/ZF, this clean development is much easier to follow.