Searching for circles of pure proofs

When given a set of properties or conditions (say, three) that are claimed to be equivalent, the claim can be verified by supplying what we call acircle of proofs. In the case in point, one proves the second property or condition from the first, the third from the second, and the first from the third. If the proof that 1 implies 2 does not rely on 3, then we say that the proof is pure with respect to 3, or simply say theproof is pure. If one can renumber the three properties or conditions in such a way that one can find a circle of three pure proofs — technically, each proof pure with respect to the condition that is neither the hypothesis nor the conclusion — then we say that acircle of pure proofs has been found. Here we study the specific question of the existence of a circle of pure proofs for the thirteen shortest single axioms for equivalential calculus, subject to the requirement that condensed detachment be used as the rule of inference. For an indication of the difficulty of answering the question, we note that a single application of condensed detachment to the (shortest single) axiom known asP4 (also known asUM) with itself yields the (shortest single) axiomP5 (also known asXGF), and two applications of condensed detachment beginning withP5 as hypothesis yieldsP4. Therefore, except forP5, one cannot find a pure proof of any of the twelve shortest single axioms when usingP4 as hypothesis or axiom, for the first application of condensed detachment must focus on two copies ofP4, which results in the deduction ofP5, forcingP5 to be present in all proofs that useP4 as the only axiom. Further, the close proximity in the proof sense ofP4 when using as the only axiomP5 threatens to make impossible the discovery of a circle of pure proofs for the entire set of thirteen shortest single axioms. Perhaps more important than our study of pure proofs, and of a more general nature, we also present the methodology used to answer the cited specific question, a methodology that relies on various strategies and features offered by W. McCune's automated reasoning programOtter. The strategies and features ofOtter we discuss here offer researchers the needed power to answer deep questions and solve difficult problems. We close this article (in the last two sections) with some challenges and some topics for research and (in the Appendix) with a sample input file and some proofs for study.Author supported by the Mathematical, Information, and Computational Sciences Division, Subprogram of the Office of Computational and Technology Research, U.S. Department of Energy, under Contract W-31-109-Eng-38.     

Automated proofs of the moufang identities in alternative rings

In this paper we present automatic proofs of the Moufang identities in alternative rings. Our approach is based on the term rewriting (Knuth-Bendix completion) method, enforced with various features. Our proofs seem to be the first computer proofs of these problems done by a general purpose theorem prover. We also present a direct proof of a certain property of alternative rings without employing any auxiliary functions. To our knowledge our computer proof seems to be the first direct proof of this property, by human or by a computer.On leave from the Department of Computer Science, UNYY at Stony Brook, New York. Research supported in part by NSF grants CCR-8805734, INT-8715231, and CCR-8901322.     

Automating the Search for Elegant Proofs

The research reported in this article was spawned by a colleague's request to find an elegant proof (of a theorem from Boolean algebra) to replace his proof consisting of 816 deduced steps. The request was met by finding a proof consisting of 100 deduced steps. The methodology used to obtain the far shorter proof is presented in detail through a sequence of experiments. Although clearly not an algorithm, the methodology is sufficiently general to enable its use for seeking elegant proofs regardless of the domain of study. In addition to (usually) being more elegant, shorter proofs often provide the needed path to constructing a more efficient circuit, a more effective algorithm, and the like. The methodology relies heavily on the assistance of McCune's automated reasoning program OTTER. Of the aspects of proof elegance, the main focus here is on proof length, with brief attention paid to the type of term present, the number of variables required, and the complexity of deduced steps. The methodology is iterative, relying heavily on the use of three strategies: the resonance strategy, the hot list strategy, and McCune's ratio strategy. These strategies, as well as other features on which the methodology relies, do exhibit tendencies that can be exploited in the search for shorter proofs and for other objectives. To provide some insight regarding the value of the methodology, I discuss its successful application to other problems from Boolean algebra and to problems from lattice theory. Research suggestions and challenges are also offered.     

The power of combining resonance with heat

In this article, I present experimental evidence of the value of combining two strategies each of which has proved powerful in various contexts. The resonance strategy gives preference (for directing a program's reasoning) to equations or formulas that have the same shape (ignoring variables) as one of the patterns supplied by the researcher to be used as a resonator. The hot list strategy rearranges the order in which conclusions are drawn, the rearranging caused by immediately visiting and, depending on the value of the heat parameter, even immediately revisiting a set of input statements chosen by the researcher; the chosen statements are used to complete applications of inference rules rather than to initiate them. Combining these two strategies often enables an automated reasoning program to attack deep questions and hard problems with far more effectiveness than using either alone. The use of this combination in the context of cursory proof checking produced most unexpected and satisfying results, as I show here. I present the material (including commentary) in the spirit of excerpts from an experimenter's notebook, thus meeting the frequent request to illustrate how a researcher can make wise choices from among the numerous options offered by McCune's automated reasoning program OTTER. I include challenges and topics for research and, to aid the researcher, in the Appendix a sample input file and a number of intriguing proofs.This work was supported by the Mathematical, Information, and Computational Sciences Division subprogram of the Office of Computational and Technology Research, U.S. Department of Energy, under Contract W-31-109-Eng-38.     

Missing Proofs Found

For close to a century, despite the efforts of fine minds that include Hilbert and Ackermann, Tarski and Bernays, ukasiewicz, and Rose and Rosser, various proofs of a number of significant theorems have remained missing – at least not reported in the literature – amply demonstrating the depth of the corresponding problems. The types of such missing proofs are indeed diverse. For one example, a result may be guaranteed provable because of being valid, and yet no proof has been found. For a second example, a theorem may have been proved via metaargument, but the desired axiomatic proof based solely on the use of a given inference rule may have eluded the experts. For a third example, a theorem may have been announced by a master, but no proof was supplied. The finding of missing proofs of the cited types, as well as of other types, is the focus of this article. The means to finding such proofs rests with heavy use of McCune's automated reasoning program OTTER, reliance on a variety of powerful strategies this program offers, and employment of diverse methodologies. Here we present some of our successes and, because it may prove useful for circuit design and program synthesis as well as in the context of mathematics and logic, detail our approach to finding missing proofs. Well-defined and unmet challenges are included.     

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.     

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.     

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.     

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.     

Invariant computations for analytic projective geometry

This paper focuses on two underlying questions for symbolic computations in projective geometry:

I How should a projective geometric property be written analytically? A first order formula in the language of fields which expresses a “projective geometric property” is translated, by an algorithm, into a restricted class of formulas in the analytic geometric language of brackets (or invariants). This special form corresponds to statements in synthetic projective geometry and the algorithm is a basic step towards translation back into synthetic geometry.

II How are theorems of analytic geometry proven? Axioms for the theorems of analytic projective geometry are given in the invariant language. Identities derived form Hubert's Nullstellensatz then play a central role in the proof. Prom a proof of an open theorem about “geometric properties”, over all fields, or over ordered fields, an algorithm derives Nullstellensatz identities — giving maximal algebraic simplicity, and maximal information in the proof.

The results support the proposal that computational analytic projective geometry should be carried out directly with identities in the invariant language.     

Induction=I-Axiomatization+First-Order Consistency

In the early 1980s, there was a number of papers on what should be called proofs by consistency. They describe how to perform inductive proofs, without using an explicit induction scheme, in the context of equational specifications and ground-convergent rewrite systems. The method was explicitly stated as a first-order consistency proof in the case of pure equational, constructor-based specifications. In this paper, we show how, in general, inductive proofs can be reduced to first-order consistency and hence be performed by a first-order theorem prover. Moreover, we extend previous methods, allowing nonequational specifications (even non-Horn specifications) and designing some specific strategies. Finally, we also show how to drop the ground convergence requirement (which is called Saturatedness for general clauses).     

Process algebra with guards: Combining Hoare logic with process algebra

We extend process algebra with guards, comparable to the guards in guarded commands or conditions in common programming constructs such as if — then — else — fi and while — do — od.The extended language is provided with an operational semantics based on transitions between pairs of a process and a (data-)state. The data-states are given by a data environment that also defines in which data-states guards hold and how atomic actions (non-deterministically) transform these states. The operational semantics is studied modulo strong bisimulation equivalence. For basic process algebra (without operators for parallelism) we present a small axiom system that is complete with respect to a general class of data environments. Given a particular data environmentL we add three axioms to this system, which is then again complete, provided weakest preconditions are expressible andL is sufficiently deterministic.Then we study process algebra with parallelism and guards. A two phase-calculus is provided that makes it possible to prove identities between parallel processes. Also this calculus is complete. In the last section we show that partial correctness formulas can easily be expressed in this setting. We use process algebra with guards to prove the soundness of a Hoare logic for linear processes by translating proofs in Hoare logic into proofs in process algebra.Supported by ESPRIT Basic Research Action no. 3006 (CONCUR) and by RACE project no. 1046 (SPECS).Supported by RACE project no. 1046 (SPECS).     

A Duality in Proof Systems for Recursive Type Equality and for Bisimulation Equivalence on Cyclic Term Graphs

This paper is concerned with a proof-theoretic observation about two kinds of proof systems for regular cyclic objects. It is presented for the case of two formal systems that are complete with respect to the notion of “recursive type equality” on a restricted class of recursive types in μ-term notation. Here we show the existence of an immediate duality with a geometrical visualization between proofs in a variant of the coinductive axiom system due to Brandt and Henglein and “consistency-unfoldings” in a variant of a 'syntactic-matching' proof system for testing equations between recursive types due to Ariola and Klop.Finally we sketch an analogous result of a duality between a similar pair of proof systems for bisimulation equivalence on equational specifications of cyclic term graphs.     

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.     

Meeting the challenge of fifty years of logic

In this article, we tell a story of good fortune. The good fortune concerns the discovery of a systematic approach to compress 50 years of excellent research in logic into a single day's use of an automated reasoning program. The discovery resulted from a colleague's experiment with a new representation and a new use of the weighting strategy. The experiment focused on an attempt—which I knew would fail—to prove one of the benchmark theorems that had eluded us for years. Fortunately, I was wrong; my colleague's attempt was successful, and a proof was found. The proof led to proving in one day 13 theorems, theorems that resulted from 50 years of excellent research in logic. We present these theorems as intriguing problems to test the power of a reasoning program or to evaluate the effectiveness of a new idea. In addition to the challenge problems, we discuss a possible approach to finding short proofs and the results achieved with it.This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under Contract W-31-109-Eng-38.     

PROPOSITIONAL DYNAMIC LOGIC FOR REASONING ABOUT FIRST‐CLASS AGENT INTERACTION PROTOCOLS

For agents to fulfill their potential of being intelligent and adaptive, it is useful to model their interaction protocols as executable entities that can be referenced, inspected, composed, shared, and invoked between agents, all at runtime. We use the term first‐class protocol to refer to such protocols. Rather than having hard‐coded decision‐making mechanisms for choosing their next move, agents can inspect the protocol specification at runtime to do so, increasing their flexibility. In this article, we show that propositional dynamic logic (PDL) can be used to represent and reason about the outcomes of first‐class protocols. We define a proof system for PDL that permits reasoning about recursively defined protocols. The proof system is divided into two parts: one for reasoning about terminating protocols, and one for reasoning about nonterminating protocols. We prove that proofs about terminating protocols can be automated, while proofs about nonterminating protocols are unable to be automated in some cases. We prove that, for a restricted class of nonterminating protocols, proofs about them can be transformed to proofs about terminating protocols, making them automatable.     

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.     

DynamiCS: An Actor-Based Framework for Negotiating Mobile Agents

In this article, a framework to integrate negotiation capabilities—particularly, components implementing a negotiation strategy—into mobile agents is described. This approach is conceptually based on the notion of an actor system which decomposes an application component into autonomously executing subcomponents cooperating with each other. Technically, the framework is based on a plug-in mechanism enabling a dynamic composition of negotiating agents. Additionally, this contribution describes how interaction-oriented rule mechanisms can be deployed to control the behavior of strategy actors.