Autarkic Computations in Formal Proofs

Formal proofs in mathematics and computer science are being studied because these objects can be verified by a very simple computer program. An important open problem is whether these formal proofs can be generated with an effort not much greater than writing a mathematical paper in, say, LATEX. Modern systems for proof development make the formalization of reasoning relatively easy. However, formalizing computations in such a manner that the results can be used in formal proofs is not immediate. In this paper we show how to obtain formal proofs of statements such as Prime(61) in the context of Peano arithmetic or (x+1)(x+1)=x ²+2x+1 in the context of rings. We hope that the method will help bridge the gap between the efficient systems of computer algebra and the reliable systems of proof development.     

Constraint Solving for Proof Planning

Proof planning is an application of AI planning to theorem proving that employs plan operators that encapsulate mathematical proof techniques. Many proofs require the instantiation of variables; that is, mathematical objects with certain properties have to be constructed. This is particularly difficult for automated theorem provers if the instantiations have to satisfy requirements specific for a mathematical theory, for example, for finite sets or for real numbers, because in this case unification is insufficient for finding a proper instantiation. Often, constraint solving can be employed for this task. We describe a framework for the integration of constraint solving into proof planning that combines proof planners and stand-alone constraint solvers. Proof planning has some peculiar requirements that are not met by any off-the-shelf constraint-solving system. Therefore, we extended an existing propagation-based constraint solver in a generic way. This approach generalizes previous work on tackling the problem. It provides a more principled way and employs existing AI technology.     

基于Z3的Coq自动证明策略的设计和实现

形式化验证方法被认为是一种构建高可信软件系统的有效手段.在定理证明工具通过手动写证明脚本来验证系统软件的功能正确性,这种验证方式表达力强,可以证明复杂系统,但是自动化程度低、验证代价比较高,而使用程序验证器接受经过规范标注的源代码生成验证条件,并将验证条件交给约束求解器自动求解,这种方式自动化程度高,缺点在于它很难验证复杂系统软件的全部功能的正确性.本文结合上述两种方式的优点,在定理证明工具Coq中实现了一个自动证明策略smt4coq,它通过在Coq中调用约束求解器Z3自动证明32位机器整数相关的数学命题,提高了自动化验证的程度,减轻用户手动验证程序的开销.     

Incorporating Decision Procedures in Implicit Induction

In this paper we present an approach to integrating reasoning specialists into cover set induction based on constraint contextual rewriting. The approach has been successfully used to incorporate decision procedures into theSPIKE prover. Computer experiments on non-trivial verification problems illustrating the effectiveness of the proposed technique are given. The generality of the approach allows for the integration of computer algebra algorithms and techniques into induction theorem provers. To illustrate this, we discuss the integration of the Buchberger algorithm into our framework.     

Comparing Approaches to the Exploration of the Domain of Residue Classes

We report on a case study on combining proof planning with computer algebra systems. We construct proofs for basic algebraic properties of residue classes as well as for isomorphisms between residue classes using different proof techniques, which are implemented as strategies in a multi-strategy proof planner. The search space of the proof planner can be drastically reduced by employing computations of two computer algebra systems during the planning process. To test the effectiveness of our approach we carried out a large number of experiments and also compared it with some alternative approaches. In particular, we experimented with substituting computer algebra by model generation and by proving theorems with a first-order equational theorem prover instead of a proof planner.     

Premise Selection for Mathematics by Corpus Analysis and Kernel Methods

Smart premise selection is essential when using automated reasoning as a tool for large-theory formal proof development. This work develops learning-based premise selection in two ways. First, a fine-grained dependency analysis of existing high-level formal mathematical proofs is used to build a large knowledge base of proof dependencies, providing precise data for ATP-based re-verification and for training premise selection algorithms. Second, a new machine learning algorithm for premise selection based on kernel methods is proposed and implemented. To evaluate the impact of both techniques, a benchmark consisting of 2078 large-theory mathematical problems is constructed, extending the older MPTP Challenge benchmark. The combined effect of the techniques results in a 50 % improvement on the benchmark over the state-of-the-art Vampire/SInE system for automated reasoning in large theories.     

A Large-Scale Experiment in Executing Extracted Programs

It is a well-known fact that algorithms are often hidden inside mathematical proofs. If these proofs are formalized inside a proof assistant, then a mechanism called extraction can generate the corresponding programs automatically. Previous work has focused on the difficulties in obtaining a program from a formalization of the Fundamental Theorem of Algebra inside the Coq proof assistant. In theory, this program allows one to compute approximations of roots of polynomials. However, as we show in this work, there is currently a big gap between theory and practice. We study the complexity of the extracted program and analyze the reasons of its inefficiency, showing that this is a direct consequence of the approach used throughout the formalization.     

Combining Proof Plans with Partial Order Planning for Imperative Program Synthesis

The structured programming literature provides methods and a wealth of heuristic knowledge for guiding the construction of provably correct imperative programs. We investigate these methods and heuristics as a basis for mechanizing program synthesis. Our approach combines proof planning with conventional partial order planning. Proof planning is an automated theorem proving technique which uses high-level proof plans to guide the search for proofs. Proof plans are structured in terms of proof methods, which encapsulate heuristics for guiding proof search. We demonstrate that proof planning provides a local perspective on the synthesis task. In particular, we show that proof methods can be extended to represent heuristics for guiding program construction. Partial order planning complements proof planning by providing a global perspective on the synthesis task. This means that it allows us to reason about the order in which program fragments are composed. Our hybrid approach has been implemented in a semi-automatic system called Bertha. Bertha supports partial correctness and has been tested on a wide range of non-trivial programming examples.     

An Integrated Approach to High Integrity Software Verification

Using automated reasoning techniques, we tackle the niche activity of proving that a program is free from run-time exceptions. Such a property is particularly valuable in high integrity software, for example, safety- or security-critical applications. The context for our work is the SPARK Approach for the development of high integrity software. The SPARK Approach provides a significant degree of automation in proving exception freedom. Where this automation fails, however, the programmer is burdened with the task of interactively constructing a proof and possibly also having to supply auxiliary program annotations. We minimize this burden by increasing the automation, through an integration of proof planning and a program analysis oracle. We advocate a ‘cooperative’ integration, where proof-failure analysis directly constrains the search for auxiliary program annotations. The approach has been successfully tested on industrial data.     

Making a productive use of failure to generate witnesses for coinduction from divergent proof attempts

Coinduction is a proof rule. It is the dual of induction. It allows reasoning about non-well-founded structures such as lazy lists or streams and is of particular use for reasoning about equivalences. A central difficulty in the automation of coinductive proof is the choice of a relation (called a bisimulation). We present an automation of coinductive theorem proving. This automation is based on the idea of proof planning [7]. Proof planning constructs the higher level steps in a proof, using knowledge of the general structure of a family of proofs and exploiting this knowledge to control the proof search. Part of proof planning involves the use of failure information to modify the plan by the use of a proof critic [23] which exploits the information gained from the failed proof attempt. Our approach to the problem was to develop a strategy that makes an initial simple guess at a bisimulation and then uses generalisation techniques, motivated by a critic, to refine this guess, so that a larger class of coinductive problems can be automatically verified. The implementation of this strategy has focused on the use of coinduction to prove the equivalence of programs in a small lazy functional language which is similar to Haskell [22]. We have developed a proof plan for coinduction and a critic associated with this proof plan. These have been implemented in CoCLAM, an extended version of CLAM [9], with encouraging results. The planner has been successfully tested on a number of theorems. This revised version was published online in June 2006 with corrections to the Cover Date.     

On Automating Diagrammatic Proofs of Arithmetic Arguments

Theorems in automated theorem proving are usually proved by formal logical proofs. However, there is a subset of problems which humans can prove by the use of geometric operations on diagrams, so called diagrammatic proofs. Insight is often more clearly perceived in these proofs than in the corresponding algebraic proofs; they capture an intuitive notion of truthfulness that humans find easy to see and understand. We are investigating and automating such diagrammatic reasoning about mathematical theorems. Concrete, rather than general diagrams are used to prove particular concrete instances of the universally quantified theorem. The diagrammatic proof is captured by the use of geometric operations on the diagram. These operations are the inference steps of the proof. An abstracted schematic proof of the universally quantified theorem is induced from these proof instances. The constructive -rule provides the mathematical basis for this step from schematic proofs to theoremhood. In this way we avoid the difficulty of treating a general case in a diagram. One method of confirming that the abstraction of the schematic proof from the proof instances is sound is proving the correctness of schematic proofs in the meta-theory of diagrams. These ideas have been implemented in the system, called Diamond, which is presented here.     

Implementing tactics and tacticals in a higher-order logic programming language

We argue that a logic programming language with a higher-order intuitionistic logic as its foundation can be used both to naturally specify and implement tactic-style theorem provers. The language extends traditional logic programming languages by replacing first-order terms with simply-typed -terms, replacing first-order unification with higher-order unification, and allowing implication and universal quantification in queries and the bodies of clauses. Inference rules for a variety of inference systems can be naturally specified in this language. The higher-order features of the language contribute to a concise specification of provisos concerning variable occurrences in formulas and the discharge of assumptions present in many inference systems. Tactics and tacticals, which provide a framework for high-level control over search for proofs, can be directly and naturally implemented in the extended language. This framework serves as a starting point for implementing theorem provers and proof systems that can integrate many diversified operations on formulas and proofs for a variety of logics. We present an extensive set of examples that have been implemented in the higher-order logic programming language Prolog.     

Practical Reflection for Sequent Logics

It is well-known that adding reflective reasoning can tremendously increase the power of a proof assistant. In order for this theoretical increase of power to become accessible to users in practice, the proof assistant needs to provide a great deal of infrastructure to support reflective reasoning. In this paper we explore the problem of creating a practical implementation of such a support layer.Our implementation takes a specification of a logical theory (which is identical to how it would be specified if we were simply going to reason within this logical theory, instead of reflecting it) and automatically generates the necessary definitions, lemmas, and proofs that are needed to enable the reflected meta-reasoning in the provided theory.One of the key features of our approach is that the structure of a logic is preserved when it is reflected. In particular, all variables, including meta-variables, are preserved in the reflected representation. This also allows the preservation of proof automation—there is a structure-preserving one-to-one map from proof steps in the original logic to proof step in the reflected logic.To enable reasoning about terms with sequent context variables, we develop a principle for context induction, called teleportation.This work is fully implemented in the MetaPRL theorem prover.     

A Proof Environment for Teaching Mathematics

The EPGY Theorem Proving Environment is a computer program used by students to write mathematical proofs in a selection of computer-based, proof-intensive mathematics courses at the high-school and university level. The system allows easy input of mathematical expressions, application of standard proof strategies and logical inference rules, application of mathematical rules, and verification of logical inference. Each course has its own language, database of theorems, and mathematical rules. The system uses a combination of automated reasoning and symbolic computation to verify individual proof steps. The proof environment has been used by over 170 students who have taken the EPGY high-school geometry course. In addition to providing a general overview of the system, we describe what we have learned from student use of the Theorem Proving Environment in the EPGY geometry course.     

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.     

Reasoning about almost-certain convergence properties using Event-B

We propose an approach for proving that a system guarantees to establish a given property eventually with probability one. Using Event-B as our modelling language, our correctness reasoning is a combination of termination proofs (in terms of probabilistic convergence), deadlock-freedom and invariant techniques. We illustrate the approach by formalising some non-trivial algorithms, including the duelling cowboys, Herman’s probabilistic self-stabilisation and Rabin’s choice coordination. We extend the supporting Rodin Platform (Rodin) of Event-B to generate appropriate proof obligations for our reasoning, then subsequently (automatically/interactively) discharge the obligations using the built-in provers of Rodin.     

From a domain analysis to the specification and detection of code and design smells

Code and design smells are recurring design problems in software systems that must be identified to avoid their possible negative consequences on development and maintenance. Consequently, several smell detection approaches and tools have been proposed in the literature. However, so far, they allow the detection of predefined smells but the detection of new smells or smells adapted to the context of the analysed systems is possible only by implementing new detection algorithms manually. Moreover, previous approaches do not explain the transition from specifications of smells to their detection. Finally, the validation of the existing approaches and tools has been limited on few proprietary systems and on a reduced number of smells. In this paper, we introduce an approach to automate the generation of detection algorithms from specifications written using a domain-specific language. This language is defined from a thorough domain analysis. It allows the specification of smells using high-level domain-related abstractions. It allows the adaptation of the specifications of smells to the context of the analysed systems. We specify 10 smells, generate automatically their detection algorithms using templates, and validate the algorithms in terms of precision and recall on Xerces v2.7.0 and GanttProject v1.10.2, two open-source object-oriented systems. We also compare the detection results with those of a previous approach, iPlasma.     

Computers,Justification, and Mathematical Knowledge

The original proof of the four-color theorem by Appel and Haken sparked a controversy when Tymoczko used it to argue that the justification provided by unsurveyable proofs carried out by computers cannot be a priori. It also created a lingering impression to the effect that such proofs depend heavily for their soundness on large amounts of computation-intensive custom-built software. Contra Tymoczko, we argue that the justification provided by certain computerized mathematical proofs is not fundamentally different from that provided by surveyable proofs, and can be sensibly regarded as a priori. We also show that the aforementioned impression is mistaken because it fails to distinguish between proof search (the context of discovery) and proof checking (the context of justification). By using mechanized proof assistants capable of producing certificates that can be independently checked, it is possible to carry out complex proofs without the need to trust arbitrary custom-written code. We only need to trust one fixed, small, and simple piece of software: the proof checker. This is not only possible in principle, but is in fact becoming a viable methodology for performing complicated mathematical reasoning. This is evinced by a new proof of the four-color theorem that appeared in 2005, and which was developed and checked in its entirety by a mechanical proof system.

Middle-out reasoning for synthesis and induction

We develop two applications of middle-out reasoning in inductive proofs: logic program synthesis and the selection of induction schemes. Middle-out reasoning as part of proof planning was first suggested by Bundy et al. Middle-out reasoning uses variables to represent unknown terms and formulae. Unification instantiates the variables in the subsequent planning, while proof planning provides the necessary search control. Middle-out reasoning is used for synthesis by planning the verification of an unknown logic program: The program body is represented with a meta-variable. The planning results both in an instantiation of the program body and a plan for the verification of that program. If the plan executes successfully, the synthesized program is partially correct and complete. Middle-out reasoning is also used to select induction schemes. Finding an appropriate induction scheme during synthesis is difficult because the recursion of the program, which is unknown at the outset, determines the induction in the proof. In middle-out induction, we set up a schematic step case by representing the constructors that are applied to induction variables with meta-variables. Once the step case is complete, the instantiated variables correspond to an induction appropriate to the recursion of the program. We have implemented these techniques as an extension of the proof planning system CL ^A M, called Periwinkle, and synthesized a variaety of programs fully automatically. Supported by the Swiss National Science Foundation and ARC Project BC/DAAD Grant 438. The work described in this paper was carried out while the first author was at the Department of Artificial Intelligence of the University of Edinburgh. Supported by the German Ministry for Research and Technology (BMFT) under grant ITS 9102 and ARC Project BC/DAAD Grant 438. Responsibility for the contents of this publication lies with the authors. Supported by SERC grant GR/J/80702, ESPRIT BRP grant 6810, ESPRIT BRP grant EC-US 019-76094, and ARC Project BC/DAAD Grant 438.