Relations between diagonalization,proof systems,and complexity gaps

In this paper we study diagonal processes over time bounded computations of one-tape Turing machines by diagonalizing only over those machines for which there exist formal proofs that they operate in the given time bound. This replaces the traditional “clock” in resource bounded diagonalization by formal proofs about running times and establishes close relations between properties of proof systems and existence of sharp time bounds for one-tape Turing machine complexity classes. These diagonalization methods also show that the Gap Theorem for resource bounded computations can hold only for those complexity classes which differ from the corresponding provable complexity classes. Furthermore, we show that there exist recursive time bounds T(n) such that the class of languages for which we can formally prove the existence of Turing machines which accept them in time T(n) differs from the class of languages accepted by Turing machines for which we can prove formally that they run in time T(n). We also investigate the corresponding problems for tape bound computations and discuss the difference time and tapebounded computations.     

Abstract abstract reduction

We propose novel algebraic proof techniques for rewrite systems. Church–Rosser theorems and further fundamental statements that do not mention termination are proved in Kleene algebra. Certain reduction and transformation theorems for termination that depend on abstract commutation, cooperation or simulation properties are proved in an extension with infinite iteration. Benefits of the algebraic approach are simple concise calculational proofs by equational reasoning, connection with automata-based decision procedures and a natural formal semantics for rewriting diagrams. It is therefore especially suited for mechanization and automation.     

A shared-variable concurrency analysis of multi-threaded object-oriented programs

In this paper a proof outline logic is introduced for the partial correctness of multi-threaded object-oriented programs like in Java. The main contribution is a generalization of the Owicki& Gries proof method for shared-variable concurrency to dynamic thread creation. This paper also provides a formal justification of this generalization in terms of soundness and completeness proofs.     

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.     

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.     

On a new formal proof model for RFID location privacy

We discuss a recently proposed formal proof model for RFID location privacy. We show that protocols which intuitively and in several other models are considered not to be location private, are provably location private in this model. Conversely, we also show that protocols which obviously are location private, are not considered location private in this model.Specifically, we prove a protocol in which every tag transmits the same constant message to not be location private in the proposed model. Then we prove a protocol in which a tag's identity is transmitted in clear text to be weakly location private in the model.     

Mechanizing structural induction part I: Formal system

Inductive methods are basic to program proving and this paper presents the formal part of a theorem-proving system for automating mildly complex proofs by structural induction. Its features are motivated by the pragmatics of proof finding. Its syntax includes a typed language and an induction rule using a lexicographic ordering based on a substructure ordering. The domain of interpretation is a many-sorted word algebra generated by the empty set. The carriers of the algebra are ordered and functions are defined by k-recursion over them. Finally, the soundness and the weak completeness of the system are proved. The main quality of the language is its system of types and its correspondingly general induction rule.     

Cut-elimination and Redundancy-elimination by Resolution

A new cut-elimination method for Gentzen’s LK is defined. First cut-elimination is generalized to the problem of redundancy-elimination. Then the elimination of redundancy in LK-proofs is performed by a resolution method in the following way. A set of clauses C is assigned to an LK-proof ψ and it is shown that C is always unsatisfiable. A resolution refutation of C then serves as a skeleton of an LK-proof ψ′ with atomic cuts;ψ′ can be constructed from the resolution proof and ψ by a projection method. In the final step the atomic cuts are eliminated and a cut-free proof is obtained. The complexity of the method is analyzed and it is shown that a non-elementary speed-up over Gentzen’s method can be achieved. Finally an application to automated deduction is presented: it is demonstrated how informal proofs (containing pseudo-cuts) can be transformed into formal ones by the method of redundancy-elimination; moreover, the method can even be used to transform incorrect proofs into correct ones.     

Lifting lower bounds for tree-like proofs

It is known that constant-depth Frege proofs of some tautologies require exponential size. No such lower bound result is known for more general proof systems. We consider tree-like sequent calculus proofs in which formulas can contain modular connectives and only the cut formulas are restricted to be of constant depth. Under a plausible hardness assumption concerning small-depth Boolean circuits, we prove exponential lower bounds for such proofs. We prove these lower bounds directly from the computational hardness assumption. We start with a lower bound for cut-free proofs and “lift” it so it applies to proofs with constant-depth cuts. By using the same approach, we obtain the following additional results. We provide a much simpler proof of a known unconditional lower bound in the case where modular connectives are not used. We establish a conditional exponential separation between the power of constant-depth proofs that use different modular connectives. We show that these tree-like proofs with constant-depth cuts cannot polynomially simulate similar dag-like proofs, even when the dag-like proofs are cut-free. We present a new proof of the non-finite axiomatizability of the theory of bounded arithmetic I Δ₀(R). Finally, under a plausible hardness assumption concerning the polynomial-time hierarchy, we show that the hierarchy \({G_i^*}\) of quantified propositional proof systems does not collapse.     

A hoare-like proof system for analysing the computation time of programs

Versions of Hoare logic have been introduced to prove partial and total correctness properties of programs. In this paper it is shown how a Hoare-like proof system for while programs may be extended to prove properties of the computation time as well. It should be stressed that the system does not require the programs to be modified by inserting explicit operations upon a clock variable. We generalize the notions of arithmetically sound and complete and show that the proof system satisfies these. Also we derive formal rules corresponding to the informal rules for determining the computation time of while programs. The applicability of the proof system is illustrated by an example, the bubble sorting algorithm.     

Certifying Term Rewriting Proofs in ELAN

Term rewriting has been shown to be a good environment for both programming and proving. For analysing and debugging rule-based programs, we propose in this work a formalism based on the rewriting calculus with explicit substitutions (ρσ-calculus). This formalism also allows us to build the proof terms of rewriting derivations. Therefore, term rewriting proofs can be exported to other systems by translating them into the corresponding syntaxes. That is, using a proof checker, one can certify these proofs and vice versa, this method allows us to get term rewriting in proof assistants using an external system. Our method not only works with syntactic rewriting but also with rewriting modulo a set of axioms (e.g. associativity-commutativity).     

Incompleteness of relational simulations in the blocking paradigm

Refinement is the notion of development between formal specifications. For specifications given in a relational formalism, downward and upward simulations are the standard method to verify that a refinement holds, their usefulness based upon their soundness and joint completeness. This is known to be true for total relational specifications and has been claimed to hold for partial relational specifications in both the non-blocking and blocking interpretations.In this paper we show that downward and upward simulations in the blocking interpretation, where domains are “guards”, are not jointly complete. This contradicts earlier claims in the literature. We illustrate this with an example (based on one recently constructed by Reeves and Streader) and then construct a proof to show why joint completeness fails in general.     

A formal proof of the ε-optimality of absorbing continuous pursuit algorithms using the theory of regular functions

The most difficult part in the design and analysis of Learning Automata (LA) consists of the formal proofs of their convergence accuracies. The mathematical techniques used for the different families (Fixed Structure, Variable Structure, Discretized etc.) are quite distinct. Among the families of LA, Estimator Algorithms (EAs) are certainly the fastest, and within this family, the set of Pursuit algorithms have been considered to be the pioneering schemes. Informally, if the environment is stationary, their ε-optimality is defined as their ability to converge to the optimal action with an arbitrarily large probability, if the learning parameter is sufficiently small/large. The existing proofs of all the reported EAs follow the same fundamental principles, and to clarify this, in the interest of simplicity, we shall concentrate on the family of Pursuit algorithms. Recently, it has been reported Ryan and Omkar (J Appl Probab 49(3):795–805, 2012) that the previous proofs for ε-optimality of all the reported EAs have a common flaw. The flaw lies in the condition which apparently supports the so-called “monotonicity” property of the probability of selecting the optimal action, which states that after some time instant t ₀, the reward probability estimates will be ordered correctly forever. The authors of the various proofs have rather offered a proof for the fact that the reward probability estimates are ordered correctly at a single point of time after t ₀, which, in turn, does not guarantee the ordering forever, rendering the previous proofs incorrect. While in Ryan and Omkar (J Appl Probab 49(3):795–805, 2012), a rectified proof was presented to prove the ε-optimality of the Continuous Pursuit Algorithm (CPA), which was the pioneering EA, in this paper, a new proof is provided for the Absorbing CPA (ACPA), i.e., an algorithm which follows the CPA paradigm but which artificially has absorbing states whenever any action probability is arbitrarily close to unity. Unlike the previous flawed proofs, instead of examining the monotonicity property of the action probabilities, it rather examines their submartingale property, and then, unlike the traditional approach, invokes the theory of Regular functions to prove that the probability of converging to the optimal action can be made arbitrarily close to unity. We believe that the proof is both unique and pioneering, and adds insights into the convergence of different EAs. It can also form the basis for formally demonstrating the ε-optimality of other Estimator algorithms which are artificially rendered absorbing.     

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.     

Structured calculational proof

We propose a new format for writing proofs, calledstructured calculational proof. The format resembles the calculational style already familiar to many computer scientists, but extends it to allow the hierarchical decomposition of larger proofs into smaller ones. Structured calculation is actually an alternative presentation of natural deduction, a style of reasoning which uses hierarchical decomposition to great effect, but which is traditionally expressed in a notation that is inconvenient for writing calculational proofs. The hierarchical nature of structured calculational proofs can be used for browsing proofs in electronic publications.     

Proof by analogy in mural

An important advantage of using a formal method of developing software is that one can prove that development steps are correct with respect to their specification. Conducting proofs by hand, however, can be time consuming to the extent that designers have to judge whether a proof of a particular obligation is worth conducting. Even if hand proofs are worth conducting, how do we know that they are correct? One approach to overcoming this problem is to use an automatic theorem proving system to develop and check our proofs. However, in order to enable present day theorem provers to check proofs, one has to conduct them in much more detail than hand proofs. Carrying out more detailed proofs is of course more time consuming. This paper describes the use of proof by analogy in an attempt to reduce the time spent on proofs. We develop and implement a proof follower based on analogy and present an example to illustrate its characteristics. The example shows that even when the follower fails to complete a proof, it can provide a hint that enables the user to complete a proof.     

Structured derivations: a unified proof style for teaching mathematics

Structured derivations were introduced by Back and von Wright as an extension of the calculational proof style originally proposed by E. W. Dijkstra and his colleagues. Structured derivations added nested subderivations and inherited assumptions to this style. This paper introduces further extensions of the structured derivation format, and gives a precise syntax and semantics for the extended proof style. The extensions provide a unification of the three main proof styles used in mathematics today: Hilbert-style forward chaining proofs, Gentzen-style backward chaining proofs and algebraic derivations and calculations (in particular, Dijkstra’s calculational proof style). Each of these proof styles can now be directly presented as a structured derivation. Even more importantly, the three proof styles can be freely intermixed in a single structured derivation, allowing different proof styles to be used in different parts of the derivation, each time choosing the proof style that is most suitable for the (sub)problem at hand. We describe here (extended) structured derivations, feature by feature, and illustrate each feature with examples. We show how to model the three main proof styles as structured derivations. We give an exact syntax for structured derivations and define their semantics by showing how a structured derivation can be automatically translated into an equivalent Gentzen-style sequent calculus derivation. Structured derivations have been primarily developed for teaching mathematics at the secondary and tertiary education level. The syntax of structured derivations determines the general structure of the proof, but does not impose any restrictions on how the basic notions of the underlying mathematical domain are treated. Hence, the style can be used for any kind of proofs, calculations, derivations, and general problem solving found in mathematics education at these levels. The precise syntax makes it easy to provide computer support for structured derivations.     

Davis-Putnam resolution versus unrestricted resolution

A resolution proof of an unsatisfiable propositional formula in conjunctive normal form is a Davis-Putnam resolution proof iff there exists a sequence of the variables of the formula such thatx is eliminated (with the resolution rule) beforey on any branch of the proof tree representing the resolution proof, only ifx is beforey in this sequence. Davis-Putnam resolution is one of several resolution restrictions. It is complete.We present an infinite family of unsatisfiable propositional formulas and show: These formulas have unrestricted resolution proofs whose length is polynomial in their size. All Davis-Putnam resolution proofs of these formulas are of superpolynomial length. In the terminology of [4, definition 1.5]: Davis-Putnam resolution does notp-simulate unrestricted resolution.     

A modal logic internalizing normal proofs

In the proof-theoretic study of logic, the notion of normal proof has been understood and investigated as a metalogical property. Usually we formulate a system of logic, identify a class of proofs as normal proofs, and show that every proof in the system reduces to a corresponding normal proof. This paper develops a system of modal logic that is capable of expressing the notion of normal proof within the system itself, thereby making normal proofs an inherent property of the logic. Using a modality △ to express the existence of a normal proof, the system provides a means for both recognizing and manipulating its own normal proofs. We develop the system as a sequent calculus with the implication connective ⊃ and the modality △, and prove the cut elimination theorem. From the sequent calculus, we derive two equivalent natural deduction systems.