MPTP – Motivation, Implementation, First Experiments

We describe a number of new possibilities for current theorem provers that arise with the existence of large integral bodies of formalized mathematics. Then we describe the implementation of the MPTP system, which makes the largest existing corpus of formalized mathematics available to theorem provers. MPTP (Mizar Problems for Theorem Proving) is a system for translating the Mizar Mathematical Library (MML) into untyped first-order format suitable for automated theorem provers and for generating theorem-proving problems corresponding to MML. The first version generates about 30,000 problems from complete proofs of Mizar theorems and about 630,000 problems from the simple (one-step) justifications done by the Mizar checker. We describe the design and structure of the system, the main problems encountered in this kind of system, their solutions, current limitations, and planned extensions. We present results of first experiments with re-proving the MPTP problems with theorem provers. We also describe first implementation of the Mizar Proof Advisor (MPA) used for selecting suitable axioms from the large library for an arbitrary problem and, again, present first results of this combined MPA/ATP architecture on MPTP.     

MPTP 0.2: Design, Implementation, and Initial Experiments

This paper describes the second version of the Mizar Problems for Theorem Proving (MPTP) system and first experimental results obtained with it. The goal of the MPTP project is to make the large formal Mizar Mathematical Library (MML) available to current first-order automated theorem provers (ATPs) (and vice versa) and to boost the development of domain-based, knowledge-based, and generally AI-based ATP methods. This version of MPTP switches to a generic extended TPTP syntax that adds term-dependent sorts and abstract (Fraenkel) terms to the TPTP syntax. We describe these extensions and explain how they are transformed by MPTP to standard TPTP syntax using relativization of sorts and deanonymization of abstract terms. Full Mizar proofs are now exported and also encoded in the extended TPTP syntax, allowing a number of ATP experiments. This covers, for example, consistent handling of proof-local constants and proof-local lemmas and translating of a number of Mizar proof constructs into the TPTP formalism. The proofs using second-order Mizar schemes are now handled by the system, too, by remembering (and, if necessary, abstracting from the proof context) the first-order instances that were actually used. These features necessitated changes in Mizar, in the Mizar-to-TPTP exporter, and in the problem-creating tools. Mizar has been reimplemented to produce and use natively a detailed XML format, suitable for communication with other tools. The Mizar-to-TPTP exporter is now just a XSLT stylesheet translating the XML tree to the TPTP syntax. The problem creation and other MPTP processing tasks are now implemented in about 1,300 lines of Prolog. All these changes have made MPTP more generic, more complete, and more correct. The largest remaining issue is the handling of the Mizar arithmetical evaluations. We describe several initial ATP experiments, both on the easy and on the hard MML problems, sometimes assisted by machine learning. It is shown that on the nonarithmetical problems, countersatisfiability (completions) is no longer detected by the ATP systems, suggesting that the ‘Mizar deconstruction’ done by MPTP is in this case already complete. About every fifth nonarithmetical theorem is proved in a fully autonomous mode, in which the premises are selected by a machine-learning system trained on previous proofs. In 329 of these cases, the newly discovered proofs are shorter than the MML originals and therefore are likely to be used for MML refactoring. This situation suggests that even a simple inductive or deductive system trained on formal mathematics can be sometimes smarter than MML authors and usable for general discovery in mathematics.     

Custom Automations in Mizar

The central aim of the Mizar project is to produce strictly formalized mathematical statements with mechanically certified proofs. When writing a Mizar formalization, a significant amount of the user’s time typically goes into browsing the Mizar Mathematical Library (MML) for the already-proved results he needs. Here a few techniques to reduce this time are illustrated.     

On the Structure of Mizar Types

The aim of this paper is to develop a formal theory of Mizar types. The examples are extracted from Mizar Mathematical Library (MML), some of them are simplified or presented in a bit different way. The presented theory is an approach to the structure of Mizar types as a sup-semilattice with widening (subtyping) relation as the order. It is an abstraction from the existing implementation of the Mizar verifier by Andrzej Trybulec and Czesław Byliński. The theory describes the structure of types of the base fragment of Mizar language.     

A Comparison of Mizar and Isar

The mathematical proof checker Mizar by Andrzej Trybulec uses a proof input language that is much more readable than the input languages of most other proof assistants. This system also differs in many other respects from most current systems. John Harrison has shown that one can have a Mizar mode on top of a tactical prover, allowing one to combine a mathematical proof language with other styles of proof checking. Currently the only fully developed Mizar mode in this style is the Isar proof language for the Isabelle theorem prover. In fact the Isar language has become the official input language to the Isabelle system, even though many users still use its low-level tactical part only. In this paper we compare Mizar and Isar. A small example, Euclid's proof of the existence of infinitely many primes, is shown in both systems. We also include slightly higher-level views of formal proof sketches. Moreover, a list of differences between Mizar and Isar is presented, highlighting the strengths of both systems from the perspective of end-users. Finally, we point out some key differences of the internal mechanisms of structured proof processing in either system.     

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

The Mizar system is one of the pioneering systems aimed at supporting mathematical proof development on a computer that have laid the groundwork for and eventually have evolved into modern interactive proof assistants. We claim that an important milestone in the development of these systems was the creation of organized libraries accumulating all previously available formalized knowledge in such a way that new works could effectively re-use all previously collected notions. In the case of Mizar, the turning point of its development was the decision to start building the Mizar Mathematical Library as a centrally-managed knowledge base maintained together with the formalization language and the verification system. In this paper we show the process of forming this library, the evolution of its design principles, and also present some data showing its current use with the modern version of the Mizar proof checker, but also as a rich corpus of semantically linked mathematical data in various areas including web-based and natural language proof presentation, maths education, and machine learning based automated theorem proving.     

Designing Mathematical Libraries Based on Requirements for Theorems

Theorems can be considered independent of abstract domains; a theorem rather depends on a set of properties necessary to prove the theorem correct. Following this observation theorems can be formulated and proven more generally thereby improving reuse of mathematical theorems. We discuss how this view influences the design of mathematical libraries and illustrate our approach with examples written in the Mizar language. We also argue that this approach allows for both stating requirements of generic algorithms and checking whether particular instantiations of generic algorithms are semantically correct.     

Eliciting Implicit Assumptions of Mizar Proofs by Property Omission

When formalizing proofs with proof assistants, it often happens that background knowledge about mathematical concepts is employed without the formalizer explicitly requesting it. Such mechanisms are warranted in the context of discovery because they can make prover sessions more efficient (less time searching the library) and can compress proofs (the more knowledge that is implicitly available, the less needs to be explicitly said by the formalizer). In the context of justification, though, implicit knowledge may need to be made explicit. To study implicit knowledge in proof assistants, one must first characterize what implicit knowledge should be made explicit. Then, once a class of implicit background knowledge is identified, one needs to determine how to extract it from proofs. When a class of implicit knowledge is made explicit, we may then inquire to what extent the implicit knowledge is needed for any particular proof; it often happens that proofs can be successful even if some of the implicit knowledge is omitted. In this note we describe an experiment conducted on the Mizar Mathematical Library (MML) of formal mathematical proofs concerning a particular class of implicit background knowledge, namely, properties of functions and relations (e.g., commutativity, asymmetry, etc.). In our experiment we separate, for each theorem of the MML, the needed function and relation properties from the unneeded ones. Special attention is paid to those function and relation properties that are significant in discussions of foundations of mathematics.     

Integrating Searching and Authoring in Mizar

The vision of a computerized assistant to mathematicians has existed since the inception of theorem-proving systems. The Alcor system has been designed to investigate and explore how a mathematician might interact with such an assistant by providing an interface to Mizar and the Mizar Mathematical Library. Our current research focuses on the integration of searching and authoring while proving. In this paper we use a scenario to elaborate on the nature of the interaction. We abstract from the scenario two distinct styles of searching and describe how the Alcor interface implements these with a keyword and LSI-based search. Though Alcor is still in its early stages of development, there are clear implications for the general problem of integrating searching and authoring, as well as technical issues with Mizar.     

On Equivalents of Well-Foundedness

Four statements equivalent to well-foundedness (well-founded induction, existence of recursively defined functions, uniqueness of recursively defined functions, and absence of descending -chains) have been proved in Mizar and the proofs mechanically checked for correctness. It seems not to be widely known that the existence (without the uniqueness assumption) of recursively defined functions implies well-foundedness. In the proof we used regular cardinals, a fairly advanced notion of set theory. The theory of cardinals in Mizar was developed earlier by G. Bancerek. With the current state of the Mizar system, the proofs turned out to be an exercise with only minor additions at the fundamental level. We would like to stress the importance of a systematic development of a mechanized data base for mathematics in the spirit of the QED Project. 12pt ENOD – Experience, Not Only DoctrineG. Kreisel     

Experiences from Exporting Major Proof Assistant Libraries

The interoperability of proof assistants and the integration of their libraries is a highly valued but elusive goal in the field of theorem proving. As a preparatory step, in previous work, we translated the libraries of multiple proof assistants, specifically the ones of Coq, HOL Light, IMPS, Isabelle, Mizar, and PVS into a universal format: OMDoc/MMT. Each translation presented great theoretical, technical, and social challenges, some universal and some system-specific, some solvable and some still open. In this paper, we survey these challenges and compare and evaluate the solutions we chose. We believe similar library translations will be an essential part of any future system interoperability solution, and our experiences will prove valuable to others undertaking such efforts.

     

The ILTP Problem Library for Intuitionistic Logic

The Intuitionistic Logic Theorem Proving (ILTP) library provides a platform for testing and benchmarking automated theorem proving (ATP) systems for intuitionistic propositional and first-order logic. It includes about 2,800 problems in a standardized syntax from 24 problem domains. For each problem an intuitionistic status and difficulty rating were obtained by running comprehensive tests of currently available intuitionistic ATP systems on all problems in the library. Thus, for the first time, the testing and evaluation of ATP systems for intuitionistic logic have been put on a firm basis.     

基于ISA95的MES集成接口研究

ISA95标准使计划管理系统与MES之间获得了良好的集成,而B2MML规范基于XML创建了通信规范的一种实现方式,用于文本信息交换。基于Web Service、ISA95、B2MML技术设计并实现了一种MES集成接口方案。该方案实现了跨平台、跨地域、低成本的数据接口,具有良好的开放性和可扩展性。     

An autonomous multistrategy theorem proving system using knowledge-based techniques

Most general-purpose theorem-proving systems have weak search control. There is no alternative to the use of a large number of heuristics or strategies for search guidance. Choosing appropriate strategies for solving a given problem may require the knowledge of different strategies and may involve a lot of painstaking trial-and-error. To encourage the widespread use of computer reasoning systems, it is important that a theorem prover be usable by those with little knowledge of problem-solving strategies, and that a theorem prover be able to select good strategies for the user. An autonomous multistrategy theorem-proving system is developed, using knowledge-based techniques, to entirely free the user from the necessity of understanding the system or the merits of different strategies. All the user has to do is input his or her problem in first-order logic, and the system solves the problem efficiently for him or her without any manual intervention. The system embodies much of expert knowledge about how to solve problems. The knowledge is represented as metarules in knowledge base which guide a hyperlinking theorem prover to solve problems automatically and efficiently.     

Optimal Hankel-norm model reductions: Multivariable systems

This paper represents a first attempt to derive a closed-form (Hankel-norm) optimal solution for multivariable system reduction problems. The basic idea is to extend the scalar ease approach in [5] to deal with the multivariable systems. The major contribution lies in the development of a minimal degree approximation (MDA) theorem and a computation algorithm. The main theorem describes a closed-form formulation for the optimal approximants, with the optimality verified by a complete error analysis. In deriving the main theorem, some useful singular value/vector properties associated with block-Hankel matrices are explored and a key extension theorem is also developed. Imbedded in the polynomial-theoretic derivation of the extension theorem is an efficient approximation algorithm. This algorithm consists of three steps: i) compute the minimal basis solution of a polynomial matrix equation; ii) solve an algebraic Riccati equation; and iii) find the partial fraction expansion of a rational matrix.     

Estimation of Potentially Unphysical Maps

When standard methods of process (black-box) estimation are applied straightforwardly then it may happen that some sets of experimental data result in unphysical estimations of the corresponding channels (maps) describing the process. To prevent this problem, one can use the method of maximum likelihood (MML), which provides an efficient scheme for reconstruction of quantum channels. This scheme always results in estimations of channels that are fully physical, e.g. the corresponding maps are linear, positive and completely positive. To show this property, we use the MML for a derivation of physical approximations of truly unphysical operations. In particular, we analyze physical approximations of the universal-NOT gate, the quantum nonlinear polarization rotation and the map ρ → ρ². Given the result of MML, we examine retrospectively the quality of the experiment. Depending on the resulting value of the MML functional we can determine (physical) consistency of the input data.     

The impossibility of boosting distributed service resilience

We study f-resilient services, which are guaranteed to operate as long as no more than f of the associated processes fail. We prove three theorems asserting the impossibility of boosting the resilience of such services. Our first theorem allows any connection pattern between processes and services but assumes these services to be atomic (linearizable) objects. This theorem says that no distributed system in which processes coordinate using f-resilient atomic objects and reliable registers can solve the consensus problem in the presence of f+1 undetectable process stopping failures. In contrast, we show that it is possible to boost the resilience of some systems solving problems easier than consensus: for example, the 2-set-consensus problem is solvable for 2n processes and 2n-1 failures (i.e., wait-free) using n-process consensus services resilient to n-1 failures (wait-free). Our proof is short and self-contained.We then introduce the larger class of failure-oblivious services. These are services that cannot use information about failures, although they may behave more flexibly than atomic objects. An example of such a service is totally ordered broadcast. Our second theorem generalizes the first theorem and its proof to failure-oblivious services.Our third theorem allows the system to contain failure-aware services, such as failure detectors, in addition to failure-oblivious services. This theorem requires that each failure-aware service be connected to all processes; thus, f+1 process failures overall can disable all the failure-aware services. In contrast, it is possible to boost the resilience of a system solving consensus using failure-aware services if arbitrary connection patterns between processes and services are allowed: consensus is solvable for any number of failures using only 1-resilient 2-process perfect failure detectors.As far as we know, this is the first time a unified framework has been used to describe both atomic and non-atomic objects, and the first time boosting analysis has been performed for services more general than atomic objects.     

Automated proofs of equality problems in Overbeek's competition

This paper reports the detailed computer proofs of nine equality problems in Overbeek's competition obtained by Herky, a completion-based theorem prover developed by the author. Advanced techniques implemented in Herky made it a high-performance theorem prover for equational reasoning. Herky is able to prove the first nine of the ten equality problems in the competition (the tenth is an open problem). These equality problems are likely to serve as good exercises for theorem provers based on different approaches, and the proofs of these problems may help people to solve them using their own theorem provers.     

Label distribution for multimodal machine learning

Multimodal machine learning(MML)aims to understand the world from multiple related modalities.It has attracted much attention as multimodal data has become increasingly available in real-world application.It is shown that MML can perform better than single-modal machine learning,since multi-modalities containing more information which could complement each other.However,it is a key challenge to fuse the multi-modalities in MML.Different from previous work,we further consider the side-information,which reflects the situation and influences the fusion of multi-modalities.We recover multimodal label distribution(MLD)by leveraging the side-information,representing the degree to which each modality contributes to describing the instance.Accordingly,a novel framework named multimodal label distribution learning(MLDL)is proposed to recover the MLD,and fuse the multimodalities with its guidance to learn an in-depth understanding of the jointly feature representation.Moreover,two versions of MLDL are proposed to deal with the sequential data.Experiments on multimodal sentiment analysis and disease prediction show that the proposed approaches perform favorably against state-of-the-art methods.