ABSTRACT. Combinatorial design theory is the study of set systems with certain balance and symmetry properties. Designs have numerous applications in computer science and mathematics; however, have not previously been formalised in any theorem prover. This paper presents a modular approach to formalising designs in Isabelle using locales, Isabelle’s module system, and assesses the usability of a locale centric approach to formalisations of mathematical structures. We demonstrate how locales can be used to precisely define numerous types of designs and their hierarchy. The resulting library also includes formal definitions and proofs for many fundamental properties, operations, and theorems on designs, with a focus on block designs. This work demonstrates that locales can be used to establish a concise, yet easily extendable and adaptable library while also noting some current limitations.

ABSTRACT. The natural proof assistant Naproche accepts input texts in the controlled natural language ForTheL for mathematics. Some ForTheL texts which are proof-checked by the Naproche system come close to ordinary mathematical writing. Naproche has been included as a bundled component in the latest edition of the Isabelle prover platform. In this paper we present some formalization examples from number theory, set theory and lattice theory which are included in Isabelle 2021. These short texts demonstrate the potential to write mathematics in a natural yet completely formal language and to delegate tedious organisatorial details and simple proof steps to strong automated theorem proving so that mathematical lines of thought and "beauty" of proofs become visible.

ABSTRACT. We formalize soundness and completeness proofs for a number of axiomatic systems for propositional logic in the proof assistant Isabelle/HOL.

ABSTRACT. Premise selection is a fundamental task for automated reasoning in large theories. A recently proposed approach formulates premise selection as a sequence to sequence problem, called stateful premise selection. Given a theorem statement, the goal of a stateful premise selection method is to predict the set of premises that would be useful in proving it. In this work we use the Transformer architecture for learning the stateful premise selection method. We outperform the existing recurrent neural network baseline and achieve new state of the art on a recently proposed dataset.

ABSTRACT. In this paper we present a set of benchmarks for automated theorem provers that require inductive reasoning. Motivated by the need to compare first-order theorem provers, SMT solvers and inductive theorem provers, the setting of our examples follows the SMT-LIB standard. Our benchmark set contains problems with inductive data types as well as integers. In addition to SMT-LIB encodings we provide translations to some other less common input formats.

ABSTRACT. In this work, we are developing formal foundations for the analysis of the policies by which a client can gain more confidence about the protection of his data and code running on a remote platform. The focus is on the development of a tool that can automatically verify that certain properties (such as integrity and confidentiality) hold for the data and code at all times. A potential use case is for the ``Deutsche Bahn" to ensure the safety of the passengers in the driverless trains using cloud services.

ABSTRACT. The central inquiry in many safety-critical systems is to assess the probability of all possible risk consequences that can occur in a system and its subsystems. The two main methods commonly used by planners/designers for evaluating the risk assessment probabilities are Event Tree Analysis (ETA) and Fault Tree Analysis (FTA). In this research, we use the higher-order logic theorem prover HOL4 to formalize Event Trees (ET), Functional Block Diagrams (FBD) and Cause Consequence Diagrams (CCD) based on Fault Trees (FT) as well as on Reliability Block Diagrams (RBD), as a novel approach. Moreover, we developed a Functional Block Diagrams and Event Trees Modeling and Analysis (FETMA) software tool in Python, which provides user-friendly features and graphical interfaces for industrial design engineers. We applied our methods and tools on several real-world case studies from the smart grid power systems sector, such as an IEEE 118-Bus Transmission Power Network, an Interconnected Micro-Grids System, a Nuclear Power Plant, etc.