The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar

MMLKG: Knowledge Graph for Mathematical Definitions, Statements and Proofs

Nowadays, Knowledge Graphs (KGs) are important and developing in different areas. However, there is a lack of genuinely interoperable datasets representing mathematics that allow for information exchange between datasets in the Web ecosystem. In this paper, we address this matter based on the Mizar Mathematical Library (MML), a collection of articles written in the Mizar language. MML includes definitions and theorems with proofs to which authors can easily refer from newly written Mizar articles. However, extracting information directly from Mizar scripts by external projects is not very straightforward. Therefore, we propose a new data storage and retrieval approach based on the Knowledge Organization System (KOS) model and the KG concept that provides a way to organize and access knowledge. We present Mizar Mathematical Library Knowledge Graph (MMLKG), a thesaurus for describing mathematical objects. MMLKG supports semantic interoperability and allows linking data from different sources, e.g., Wikidata. Moreover, it satisfies the FAIR data principles. The data is publicly available via a Cypher endpoint.

Combining Higher-Order Logic with Set Theory Formalizations

The Isabelle Higher-order Tarski-Grothendieck object logic includes in its foundations both higher-order logic and set theory, which allows importing the libraries of Isabelle/HOL and Isabelle/Mizar. The two libraries, however, define all the basic concepts independently, which means that the results in the two are disconnected. In this paper, we align significant parts of these two libraries, by defining isomorphisms between their concepts, including the real numbers and algebraic structures. The isomorphisms allow us to transport theorems between the foundations and use the results from the libraries simultaneously.

Learning to Guide a Saturation-Based Theorem Prover

Traditional automated theorem provers have relied on manually tuned heuristics to guide how they perform proof search. Recently, however, there has been a surge of interest in the design of learning mechanisms that can be integrated into theorem provers to improve their performance automatically. In this work, we describe TRAIL (Trial Reasoner for AI that Learns), a deep learning-based approach to theorem proving that characterizes core elements of saturation-based theorem proving within a neural framework. TRAIL leverages (a) an effective graph neural network for representing logical formulas, (b) a novel neural representation of the state of a saturation-based theorem prover in terms of processed clauses and available actions, and (c) a novel representation of the inference selection process as an attention-based action policy. We show through a systematic analysis that these components allow TRAIL to significantly outperform previous reinforcement learning-based theorem provers on two standard benchmark datasets (up to 36% more theorems proved). In addition, to the best of our knowledge, TRAIL is the first reinforcement learning-based approach to exceed the performance of a state-of-the-art traditional theorem prover on a standard theorem proving benchmark (solving up to 17% more theorems).

The Divergence of the Sum of Prime Reciprocals

This is Erdős’s proof of the divergence of the sum of prime reciprocals, using the Mizar system [2], [3], as reported in “Proofs from THE BOOK” [1].

The Role of Computer Remote Monitoring Technology for Nursing Care in Elderly Breast Cancer Complications

Geriatric patients undergoing mastectomy have a weakened organism and slow recovery of gastrointestinal function after surgery, which may lead to various complications, affect the absorption of intestinal nutrients, and prolong the healing rate of wounds. Therefore, it is necessary to find an effective nursing program to promote the recovery of gastrointestinal function and prevent postoperative complications in elderly patients undergoing mastectomy. With the continuous development and advancement of computer and communication technologies, telecare is gaining more and more attention and has become an important part of medical information technology construction. Falls endanger the elderly and other special populations, especially after a sudden but unassisted fall, which may be life-threatening. Timely fall detection and rescue can win valuable time for treatment and rescue, which is very important to protect users' health and improve medical monitoring. In order to provide better medical care to the elderly population and reduce the harm caused by falls, this paper will focus on the fall problem of the elderly in telecare. In order to facilitate the detection of falls of the elderly, we design an Android sensor-based data acquisition scheme, using the built-in acceleration sensor in the Android system to collect the human acceleration information, and through the JMS middleware technology, the collected data are transmitted to MATLAB for analysis and processing in real time. This paper preprocesses and synthesizes the collected human body data and visualizes the acceleration changes of various typical daily activities of the human body and breast cancer, then extracts the relevant data features according to the synthesized SVM curve, constructs a pattern recognition algorithm using the extracted features, and verifies the effectiveness of the pattern recognition algorithm through experiments.

Formal verification of Matrix based MATLAB models using interactive theorem proving

MATLAB is a software based analysis environment that supports a high-level programing language and is widely used to model and analyze systems in various domains of engineering and sciences. Traditionally, the analysis of MATLAB models is done using simulation and debugging/testing frameworks. These methods provide limited coverage due to their inherent incompleteness. Formal verification can overcome these limitations, but developing the formal models of the underlying MATLAB models is a very challenging and time-consuming task, especially in the case of higher-order-logic models. To facilitate this process, we present a library of higher-order-logic functions corresponding to the commonly used matrix functions of MATLAB as well as a translator that allows automatic conversion of MATLAB models to higher-order logic. The formal models can then be formally verified in an interactive theorem prover. For illustrating the usefulness of the proposed library and approach, we present the formal analysis of a Finite Impulse Response (FIR) filter, which is quite commonly used in digital signal processing applications, within the sound core of the HOL Light theorem prover.

Enhancement of properties in Mizar

A "property" in the Mizar proof-assistant is a construction that can be used to register chosen features of predicates (e.g., "reflexivity", "symmetry"), operations (e.g., "involutiveness", "commutativity") and types (e.g., "sethoodness") declared at the definition stage. The current implementation of Mizar allows using properties for notions with a specific number of visible arguments (e.g., reflexivity for a predicate with two visible arguments and involutiveness for an operation with just one visible argument). In this paper we investigate a more general approach to overcome these limitations. We propose an extension of the Mizar language and a corresponding enhancement of the Mizar proof-checker which allow declaring properties of notions of arbitrary arity with respect to explicitly indicated arguments. Moreover, we introduce a new property-the "fixedpoint-free" property of unary operations-meaning that the result of applying the operation to its argument always differs from the argument. Results of tests conducted on the Mizar Mathematical Library are presented.