ABSTRACT. Parts of human proofs which are discharged by formulations like ``it is easy to check'', ``clearly'' or ``one can see'' often require nontrivial effort in formalization. We discuss several tools we use to automatize such routine tasks in our library of results in combinatorics on words.

ABSTRACT. Every statement about lists has naturally a reversed version (changing prefix to suffix for example). We want to obtain such reversed variant automatically in Isabelle. We have developed a custom attribute for this task in our library of combinatorics on words. In this contribution we discuss our alternative attempts to use the Transfer package to achieve this goal, and related difficulties.

ABSTRACT. Sledgehammer, a component of the interactive proof assistant Isabelle, aims to increase proof automation by automatically discharging proof goals with the help of external provers. Among these provers are a group of satisfiability modulo theories (SMT) solvers with support for the SMT-LIB input language. Despite existing formalizations of IEEE floating-point arithmetic in both Isabelle/HOL and SMT-LIB, Sledgehammer employs an abstract translation of floating-point types and constants, depriving the SMT solvers of the opportunity to make use of their dedicated decision procedures for floating-point arithmetic.

We show that, by extending the translation from the language of Isabelle/HOL into SMT-LIB with an interpretation of floating-point types and constants, floating-point reasoning in SMT solvers can be made available to Isabelle. Our main contribution is a description and implementation of such an extension. An evaluation of the extended translation shows a significant increase of Sledgehammer's success rate on proof goals involving floating-points. In particular, this enhancement enables Sledgehammer to prove more non-trivial goals -- thereby increasing proof automation for floating-point arithmetic in Isabelle.

ABSTRACT. In this paper we present the verification of an imperative implementation of the ubiquitous B+-Tree data structure in the interactive theorem prover Isabelle/HOL. The implementation supports membership test, insertion and range queries with efficient binary search for intra-node navigation. The imperative implementation is verified in two steps: an abstract set interface is refined to an executable but inefficient purely functional implementation which is further refined to the efficient imperative implementation.

ABSTRACT. We describe selected axiomatic systems for classical propositional logic and show how Isabelle/HOL helps investigate such systems. We consider systems based on implication and falsity, implication and negation, and disjunction and negation.

ABSTRACT. I sketch preliminary work on formalizing the termination of a tableau calculus for basic hybrid logic, whose soundness and completeness have already been formally verified. The formalization includes some crucial theorems, but omits others.

ABSTRACT. We present our recent experiences teaching two courses on formal methods which use Isabelle/Pure and Isabelle/HOL. We explain our overall approach and our experiences with implementing beginner-friendly tools to help students understand how Isabelle works. We also describe the issues that we often see students struggle with when attempting to learn how to program and prove theorems using Isabelle, and suggest ideas for potential solutions to some of these concerns.

ABSTRACT. This is a technology preview of the forthcoming release Isabelle2022, which is anticipated for October 2022. It will include a fully integrated Isabelle/VSCode Prover IDE based on a bundled distribution of VSCodium, which is an open-source branch of Microsoft's VSCode project. VSCode is based on Electron, which is a desktop application framework with Chromium browser and Node.js environment. Careful patching and repackaging of VSCodium exposes Electron and Node.js for other Isabelle applications. Thus we gain access to high-end web technologies for Isabelle/PIDE browsing and editing, for example a cross-platform PDF viewer with custom URLs for Isabelle/PIDE commands.

ABSTRACT. We revisit the pending problem of accessibility and usability of mathematics for visually impaired individuals. The context is formal mathematics as represented by the proof assistant Isabelle, with the particular Prover IDE front-end Isabelle/VSCode. The broader context of software for mathematics education is provided by ISAC. Leveraging the work that Microsoft and Google have invested into accessibility of VSCode and its underlying Chromium engine, we hope to deliver a properly accessible Mathematics Working Environment (MAWEN) within the Isabelle ecosystem. An important part of this research is to figure out where standard text editing techniques end, and where specific mathematics editing starts, especially calculations and proofs.

ABSTRACT. In interactive theorem proving, formalization quality is a key factor for maintainability and re-usability of developments and can also impact proof-checking performance. Commonly, anti-patterns that cause quality issues are known to experienced users. However, in many theorem prover systems, there are no automatic tools to check for their presence and make less experienced users aware of them. We attempt to fill this gap in the Isabelle environment by developing a linter as a publicly available add-on component. The linter offers basic configurability, extensibility, Isabelle/jEdit integration, and a standalone command-line tool. We uncovered 480 potential problems in Isabelle/HOL, 14016 in other formalizations of the Isabelle distribution, and an astonishing 59573 in the AFP. With a specific lint bundle for AFP submissions, we found that submission guidelines were violated in 1595 cases. We set out to alleviate problems in Isabelle/HOL and solved 168 of them so far; we found that high-severity lints corresponded to actual problems most of the time, individual users often made the same mistakes in many places, and that solving those problems retrospectively amounts to a substantial amount of work. In contrast, solving these problems interactively for new developments usually incurs only little overhead, as we found in a quantitative user survey with 22 participants (less than a minute for more than 60% of participants). We also found that a good explanation of problems is key to the users’ ease of solving these problems (correlation coefficient 0.48), and their satisfaction with the end result (correlation coefficient 0.62).

ABSTRACT. This paper presents a detailed verification of the Gale-Shapley algorithm for stable matching (or marriage). The verification proceeds by stepwise refinement. The initial steps are on the level of imperative programs, ending in a linear time algorithm. An executable functional program is obtained in a last step. The emphasis is on the stepwise refinement and the required invariants.

ABSTRACT. We report on our work to develop an Isabelle-formalization of a proof by Lev Gordeev. That proof aims at showing that the NP-complete problem CLIQUE is not contained in P, since any Boolean circuit that solves CLIQUE will have super-polynomial size.

Initially, minor flaws have been identified and could quickly be repaired by mild adjustments of definitions and statements. However, there also have been more serious problems, where then we multiple times contacted Gordeev, who proposed more severe changes in the definitions and statements. In every iteration, Isabelle quickly pointed us to those proof steps that then needed to be adjusted, without having to perform a tedious manual rechecking of all proofs.

Although the overall proof is still in a broken state, the problems are restricted to those parts that handle negations in circuits. Consequently the super-polynomial lower bound is valid for monotone circuits: if any such circuit solves CLIQUE for graphs with $m$ vertices, then the size of the circuit is at least $\sqrt[7]{m}^{\sqrt[8]{m}}$ for sufficiently large $m$.

ABSTRACT. As we grant artificial intelligence increasing power and independence in contexts like healthcare, policing, and driving, AI faces moral dilemmas but lacks the tools to solve them. Warnings from regulators, philosophers, and computer scientists about the dangers of unethical artificial intelligence have spurred interest in automated ethics—i.e., the development of machines that can perform ethical reasoning. However, previous work in automated ethics rarely engages with existing philosophical literature. Philosophically sophisticated ethical theories are necessary for nuanced and reliable judgements, but faithfully translating these complex ethical theories from natural language to the rigid syntax of a computer program poses technical and philosophical challenges. In this paper, I present an implementation of automated Kantian ethics in Isabelle that is faithful to the Kantian philosophical tradition. I formalize Kant's categorical imperative in Carmo and Jones's Dyadic Deontic Logic, implement this formalization in Isabelle, and develop a testing framework to evaluate how well my implementation coheres with expected properties of Kantian ethics, as established in the literature. I present philosophical insights that I derived using this implementation of automated ethics to motivate computational ethics, or the use of automated tools like Isabelle to spark philosophical progress. Finally, I document my experience implementing automated ethics in Isabelle, despite my lack of prior experience using interactive theorem provers. This work demonstrates that Isabelle can be used to implement sophisticated ethical reasoning.