Integrating Computer Algebra into Proof Planning

Mechanized reasoning systems and computer algebra systems have different objectives. Their integration is highly desirable, since formal proofs often involve both of the two different tasks proving and calculating. Even more important, proof and computation are often interwoven and not easily separable.In this article we advocate an integration of computer algebra into mechanized reasoning systems at the proof plan level. This approach allows us to view the computer algebra algorithms as methods, that is, declarative representations of the problem-solving knowledge specific to a certain mathematical domain. Automation can be achieved in many cases by searching for a hierarchic proof plan at the method level by using suitable domain-specific control knowledge about the mathematical algorithms. In other words, the uniform framework of proof planning allows us to solve a large class of problems that are not automatically solvable by separate systems.Our approach also gives an answer to the correctness problems inherent in such an integration. We advocate an approach where the computer algebra system produces high-level protocol information that can be processed by an interface to derive proof plans. Such a proof plan in turn can be expanded to proofs at different levels of abstraction, so the approach is well suited for producing a high-level verbalized explication as well as for a low-level, machine-checkable, calculus-level proof.We present an implementation of our ideas and exemplify them using an automatically solved example.Changes in the criterion of rigor of the proof' engender major revolutions in mathematics. H. Poincaré, 1905     

The notion of proof in hardware verification

Recent advances in the field of hardware verification have raised some fresh (and some familiar) issues concerning the scope and limitations of formal proof. In this article, we discuss in detail some of these issues. We focus particularly on which aspects of hardware and software one can verify, in contrast to the claims that are sometimes made in that regard. Since we consider verification to be one of the more important and promising applications of automated theorem proving — our research has been concerned with this application for a number of years — a precise understanding of verification must be addressed. Although the context for our discussion is the Viper verification project, our remarks apply generally. Viper is a microprocessor designed by W. J. Cullyer, C. Pygott, and J. Kershaw of the Royal Signals and Radar Establishment of the U.K. Ministry of Defence, for use in safety-critical applications. Much to their credit, the designers intended from the start that Viper be formally verified; they presented Viper's more abstract specifications in a language suitable for formal reasoning, and they placed the design in the public domain. Since Viper microprocessors are currently being marketed as verified chips, the need exists to identify precisely to what extent verification is possible. The formal proof aspects of the verification work have been carried out at the Computer Laboratory of the University of Cambridge. To date, some important properties of a register-transfer level model of Viper, relative to a more abstract functional specification, have been proved (by the author) using the HOL proof generating system. Verified systems such as Viper seem likely to become commonplace in the near future. While proofs about the abstract models of such systems are obviously a vital contribution to our trust in them, it is also important (not least in safety-critical applications) that the limitations of the approach be understood.     

HANDLING INFORMATION LOGICS IN A GRAPHICAL PROOF EDITOR

In order to provide a background for rough set modeling of uncertainty, two types of incompleteness of information are discussed. Representation of uncertain knowledge acquired from incomplete information is outlined within the framework of information logics. Relational proof theory for the information logics is presented. It is shown how these logics and their proof systems can be handled in the GLEFATINF (Graphical & Logical Editing Framework) system. This computer program is a key component of the inference laboratory Atelier d'Inféence (ATINF) developed at LIFIA-IMAG, our lab. It provides a general framework, independent of logic and proof systems, for combining inference tools, editing, and checking proofs. The basic principles of its design and implementation are given and its capabilities are discussed. Its application to define the information logics and their proof systems and to present proofs in these proof systems is discussed and illustrated.     

Formal Verification of a Distributed Computer System

Modeling distributed computer systems is known to be a challenging enterprise. Typically, distributed systems are comprised of large numbers of components whose coordination may require complex interactions. Modeling such systems more often than not leads to the nominal intractability of the resulting state space. Various formal methods have been proposed to address the modeling of coordination among distributed systems components. For the most part, however, these methods do not support formal verification mechanisms. By way of contrast, the L-automata/L-processes model supports formal verification mechanisms which in many examples can successfully circumvent state space explosion problems, and allow verification proofs to be extended to an arbitrary number of components. After reviewing L-automata/L-processes formalisms, we present here the formal specification of a fault-tolerant algorithm for a distributed computer system. We also expose the L-automata/L-processes verification of the distributed system, demonstrating how various techniques such as homomorphic reduction, induction, and linearization, can be used to overcome various problems which surface as one models large, complex systems.     

Focusing and polarization in linear,intuitionistic, and classical logics

A focused proof system provides a normal form to cut-free proofs in which the application of invertible and non-invertible inference rules is structured. Within linear logic, the focused proof system of Andreoli provides an elegant and comprehensive normal form for cut-free proofs. Within intuitionistic and classical logics, there are various different proof systems in the literature that exhibit focusing behavior. These focused proof systems have been applied to both the proof search and the proof normalization approaches to computation. We present a new, focused proof system for intuitionistic logic, called LJF, and show how other intuitionistic proof systems can be mapped into the new system by inserting logical connectives that prematurely stop focusing. We also use LJF to design a focused proof system LKF for classical logic. Our approach to the design and analysis of these systems is based on the completeness of focusing in linear logic and on the notion of polarity that appears in Girard’s LC and LU proof systems.     

A correctness proof of an indenting program

The correctness of an indenting program for Pascal is proved at an intermediate level of rigour. The specifications of the program are given in the companion paper.¹ The program is approximately 330 lines long and consists of four modules: io, lex, stack and indent. We prove first that the individual procedures contained in these modules meet their specifications as given by the entry and exit assertions. A global proof of the main routine then establishes that the interaction between modules is such that the main routine meets the specification of the entire program. We argue that correctness proofs at the level of rigour used here serve very well to transfer one's understanding of a program to others. We believe proofs at this level should become commonplace before more formal proofs can take over to reduce traditional testing to an inconsequential place.     

Solving Open Questions and Other Challenge Problems Using Proof Sketches

In this article, we describe a set of procedures and strategies for searching for proofs in logical systems based on the inference rule condensed detachment. The procedures and strategies rely on the derivation of proof sketches – sequences of formulas that are used as hints to guide the search for sound proofs. In the simplest case, a proof sketch consists of a subproof – key lemmas to prove, for example – and the proof is completed by filling in the missing steps. In the more general case, a proof sketch consists of a sequence of formulas sufficient to find a proof, but it may include formulas that are not provable in the current theory. We find that even in this more general case, proof sketches can provide valuable guidance in finding sound proofs. Proof sketches have been used successfully for numerous problems coming from a variety of problem areas. We have, for example, used proof sketches to find several new two-axiom systems for Boolean algebra using the Sheffer stroke.     

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.     

A Framework for Proof Systems

Linear logic can be used as a meta-logic to specify a range of object-level proof systems. In particular, we show that by providing different polarizations within a focused proof system for linear logic, one can account for natural deduction (normal and non-normal), sequent proofs (with and without cut), and tableaux proofs. Armed with just a few, simple variations to the linear logic encodings, more proof systems can be accommodated, including proof system using generalized elimination and generalized introduction rules. In general, most of these proof systems are developed for both classical and intuitionistic logics. By using simple results about linear logic, we can also give simple and modular proofs of the soundness and relative completeness of all the proof systems we consider.     

Reducing the size of resolution proofs in linear time

DPLL-based SAT solvers progress by implicitly applying binary resolution. The resolution proofs that they generate are used, after the SAT solver’s run has terminated, for various purposes. Most notable uses in formal verification are: extracting an unsatisfiable core, extracting an interpolant, and detecting clauses that can be reused in an incremental satisfiability setting (the latter uses the proof only implicitly, during the run of the SAT solver). Making the resolution proof smaller can benefit all of these goals: it can lead to smaller cores, smaller interpolants, and smaller clauses that are propagated to the next SAT instance in an incremental setting. We suggest two methods that are linear in the size of the proof for doing so. Our first technique, called Recycle-Units uses each learned constant (unit clause) (x) for simplifying resolution steps in which x was the pivot, prior to when it was learned. Our second technique, called   simplifies proofs in which there are several nodes in the resolution graph, one of which dominates the others, that correspond to the same pivot. Our experiments with industrial instances show that these simplifications reduce the core by ≈5% and the proof by ≈13%. It reduces the core less than competing methods such as run- till- fix, but whereas our algorithms are linear in the size of the proof, the latter and other competing techniques are all exponential as they are based on SAT runs. If we consider the size of the proof (the resolution graph) as being polynomial in the number of variables (it is not necessarily the case in general), this gives our method an exponential time reduction comparing to existing tools for small core extraction. Our experiments show that this result is evident in practice more so for the second method: rarely it takes more than a few seconds, even when competing tools time out, and hence it can be used as a cheap proof post-processing procedure.     

Canonical systems which produce periodic sets

Canonical systems with productions of the forma x,b x c x andxa xc are shown to produce only the periodic sets. Thus, these systems are equivalent to finite-state grammars.     

A Proof Search Specification of the π-Calculus

We present a meta-logic that contains a new quantifier (for encoding “generic judgments”) and inference rules for reasoning within fixed points of a given specification. We then specify the operational semantics and bisimulation relations for the finite π-calculus within this meta-logic. Since we restrict to the finite case, the ability of the meta-logic to reason within fixed points becomes a powerful and complete tool since simple proof search can compute this one fixed point. The quantifier helps with the delicate issues surrounding the scope of variables within π-calculus expressions and their executions (proofs). We shall illustrate several merits of the logical specifications we write: they are natural and declarative; they contain no side conditions concerning names of variables while maintaining a completely formal treatment of such variables; differences between late and open bisimulation relations are easy to see declaratively; and proof search involving the application of inference rules, unification, and backtracking can provide complete proof systems for both one-step transitions and for bisimulation.     

Case studies of Z-module reasoning: Proving benchmark theorems from ring theory

A new method, called Z-module reasoning, was formulated for proving and discovering theorems from ring theory. In a case study, the ZMR system designed to implement this method was used to prove the benchmark x ³ ring theorem from associative ring theory. The system proved the theorem quite efficiently. The system was then used to prove the x ⁴ ring theorem from associative ring theory. Again, a proof was produced easily. These proofs, together with the successes in proving other difficult theorems from ring theory suggest that the Z-module reasoning method is useful for solving a class of problems relying on equality reasoning. This paper illustrates the Z-module reasoning method, and analyzes the computer proof of the x ³ ring theorem.This reasearch was supported in part by the Applied Mathematical Sciences subprogram of the office of Energy Research, U.S. Department of Energy, under contract W-31-109-Eng-38.     

Validation of HOL Proofs by Proof Checking

Formal proofs generated by mechanised theorem proving systems may consist of a large number of inferences. As these theorem proving systems are usually very complex, it is extremely difficult if not impossible to formally verify them. This calls for an independent means of ensuring the consistency of mechanically generated proofs. This paper describes a method of recording HOL proofs in terms of a sequence of applications of inference rules. The recorded proofs can then be checked by an independent proof checker. Also described in this paper is an implementation of a proof checker which is able to check a practical proof consisting of thousands of inference steps.     

The Strategy of Cramming

Offered in this article is a new strategy, cramming, that can serve well in an attempt to answer an open question or in an attempt to find a shorter proof. Indeed, when the question can be answered by proving a conjunction, cramming can provide substantial assistance. The basis of the strategy rests with forcing so many steps of a subproof into the remainder of the proof that the desired answer is obtained. As for reduction in proof length, the literature shows that proof shortening (proof abridgment) was indeed of interest to some of the masters of logic, masters that include C. A. Meredith, A. Prior, and I. Thomas. The problem of proof shortening (as well as other aspects of simplification) is also central to the recent discovery by R. Thiele of Hilbert's twenty-fourth problem. Although that problem was not included in his 1900 Paris lecture (because he had not yet sufficiently formulated it), Hilbert stressed at various times in his life the importance of finding simpler proofs. Because a sharp reduction in proof length (of constructive proofs) is correlated with a significant reduction in the complexity of the object being constructed, the cramming strategy is relevant to circuit design and program synthesis. The most impressive success with the use of the cramming strategy concerns an abridgment of the Meredith–Prior abridging of the ukasiewicz proof for his shortest single axiom for the implicational fragment of two-valued sentential (or classical propositional) calculus. In the context of answering open questions, the most satisfying examples to date concern the study of the right-group calculus and the study of the modal logic C5. Various challenges are offered here.     

On the Role of OpenMath in Interactive Mathematical Documents

The standard OpenMath is an enabling technology for creating an integrated computer environment in which software packages for computer algebra and for proof checking can be combined. Here we demonstrate how OpenMath can be employed for generating interactive mathematical documents containing primality proofs. Our case study takes place within a browser; once a prime number is specified, a document appears summarizing the proof in a number of assertions. By clicking an assertion regarding the truth of an arithmetic equality, a computer algebra calculation is invoked verifying the equality. By clicking an assertion regarding a specific mathematical lemma called Pocklington’s Criterion, a verification of the corresponding formal proof is carried out by a proof checker. Moreover, the whole document is structured in such a way that it can be easily translated to a formal proof object. OpenMath supports the interaction between the document as it appears in the browser and the mathematical software packages. This paper begins with an introduction to OpenMath and a brief comparison with MathML.