Strategies on Wednesday, August 16th

Introductory Remarks (09:15‑09:30)

Invited Talk (09:30‑10:30)

09:30‑10:30

Georges Gonthier (Microsoft Research) Internal Deduction and Decision Procedures of the 4-Colour Theorem [ppt] Our recent formalization of the proof of the Four Colour Theorem in Coq made very little use of the standard automation features of Coq: we made limited use of tacticals and of proof search, and did not use any of the advanced arithmetic or propositional decision procedures (nor did we add any). This may seem surprising, since this proof is famous for employing massive case enumerations that require computer checking. Indeed, our proof does use some advanced decision procedures, including multiway decision diagram-based model checking and Davies-Putnam and alpha-beta search. We implemented all these algorithms internally in the computational fragment of the Coq logic; our initial motivation was to limit the size of the proof objects through the use of reflection. Because these internalized decision procedures incorporated domain knowledge and were proved correct they could outperform native built-in. Furthermore, most of the basic steps of the correctness proofs could be done by simply stepping the procedures. This form of internal deduction, which we've called short-scale reflection, turned out to be so effective that we adopted it for the mathematical sections of the proof, where it became instrumental.

Break (10:30‑11:00)

Session 1 (11:00‑12:30)

11:00‑11:30	Adam Chlipala (UC Berkeley CS Division) George Necula (University of California) Cooperative Integration of an Interactive Proof Assistant and an Automated Prover We propose a mechanism for semi-automated proving of theorems, using a tactic for the Coq proof assistant that consults a proof-generating Nelson-Oppen-style automated prover. Instead of simply proving or failing to prove a goal, our tactic decides on relevant case splits using theory-specific axioms, proves some of the resulting cases, and returns the remainder to the Coq user as subgoals. These subgoals can then be proved using inductions and lemma instantiations that are beyond the capabilities of the automated prover. We show that the Coq tactic language provides an excellent way to script this process to an extent not supported by current Nelson-Oppen provers. Like with any Coq proof, a separately checkable proof term in a core calculus is produced at the end of any successful proving session where our method is used, and we take advantage of the "proof by reflection" technique to translate the specialized first-order proofs of the automated prover into compact Coq representations.
11:30‑12:00	Hongping Lim (Massachusetts Institute of Technology) Myla Archer (Naval Research Laboratory) Translation Templates to Support Strategy Development in PVS In presenting specifications and specification properties to a theorem prover, there is a tension between convenience for the user and convenience for the theorem prover. A choice of specification formulation that is most natural to a user may not be the ideal formulation for reasoning about that specification in a theorem prover. However, when the theorem prover is being integrated into a system development framework, a desirable goal of the integration is to make use of the theorem prover as easy as possible for the user. In such a context, it is possible to have the best of both worlds: specifications that are natural for a system developer to write in the language of the development framework, and representations of these specifications that are well matched to the reasoning techniques provided in the prover. In a tactic-based prover, these reasoning techniques include the use of tactics (or strategies) that can rely on certain structural elements in the theorem prover's representation of specifications. This paper illustrates how translation techniques used in integrating PVS into the TIOA (Timed Input/Output Automata) system development framework produce PVS specifications structured to support development of PVS strategies that implement reasoning steps appropriate for proving TIOA specification properties.
12:00‑12:30	Florent Kirchner (LIX / INRIA - Futurs) Cesar Munoz (National Institute of Aerospace) PVS#: Streamlined Tacticals for PVS The semantics of a proof language relies on the representation of the state of a proof after a logical rule has been applied. This information, which is usually meaningless from a logical point of view, is fundamental to describe the control mechanism of the proof search provided by the language. In this paper, we propose a datatype, called proof monad, to represent the state information of a proof and we illustrate its use in PVS. Furthermore, we show how this representation can be used to design a new set of powerful PVS tacticals that have simple and clear semantics. The implementation of these tacticals is called PVS#.

Lunch break (12:30‑14:00)

Session 2 (14:00‑15:30)

14:00‑14:30	Moa Johansson (University of Edinburgh) Alan Bundy (University of Edinburgh) Lucas Dixon (University of Edinburgh) Best-First Rippling Rippling is a form of rewriting that guides search by only performing steps that reduce the differences between formulae. Termination is normally ensured by a defined measure that is required to decrease with each step. Because of the restrictions on rippling proofs about, for example, mutual recursion will fail as steps that temporarily increase the differences are necessary. Best-first rippling is an extension to rippling where the restrictions have been recast as heuristic scores for use in best-first search. If nothing better is available, previously illegal steps can be considered, making best-first rippling more flexible than ordinary rippling. We have implemented best-first rippling in the IsaPlanner system together with a mechanism for caching proof-states that helps remove symmetries in the search space, and machinery to ensure termination based on term embeddings. Our experiments show that the implementation of best-first rippling is faster on average than IsaPlanner's version of traditional depth-first rippling, and solves a range of problems where ordinary rippling fails.
14:30‑15:00	Maria Paola Bonacina (Universita` degli Studi di Verona) Mnacho Echenim (Università degli Studi di Verona) Rewrite-Based Decision Procedures The rewrite-based approach to satisfiability modulo theories consists of using generic theorem-proving strategies, based on the superposition calculus, SP. If one can prove that, starting from the presentation T of a theory and a finite set of ground unit clauses, the superposition calculus generates a finite saturated set, then any fair superposition-based strategy can be used as a T-satisfiability procedure. This approach makes it conceptually simple to combine several theories, under the variable-inactive condition. In this paper, we introduce a number of sufficient conditions that allow us to generalize the entire framework of rewrite-based T-satisfiability procedures, to obtain rewrite-based T-decision procedures. These conditions will allow us to give simple proofs that SP yields T-decision procedures for several theories, including the theory of arrays and two of its extensions. We show that the theories satisfying these conditions are guaranteed to be variable-inactive, and can therefore all be combined.
15:00‑15:30	William McCune (argonne national laboratory) Semantic Guidance with Carefully Chosen Interpretations We use finite interpretations to guide searches in first-order and equational theorem provers. The interpretations are carefully chosen and based on expert knowledge of the problem area of the conjecture. The method has been implemented in the Prover9 system, and equational examples are given the areas of lattice theory, Boolean algebras, and modular ortholattices.

Break (15:30‑16:00)

Invited Talk (16:00‑17:00)

16:00‑17:00

José Meseguer (University of Illinois at Urbana-Champaign) Specifying and Implementing Strategies in Rewriting Logic [pdf] By J. Meseguer, S. Eker, N. Martí-Oliet, and A. Verdejo Rewriting logic is a simple logical framework in which the inference rules of a logic or of any deductive procedure can be easily expressed as conditional rewrite rules. This allows a modular separation between the inference rules themselves and their control through strategies. In this way, one can reason, for example, about key correctness properties of an inference system while leaving open various control issues on how to apply the inference rules in an optimal way. This is a much better way to specify an inference system than the traditional algorithmic descriptions of deductive procedures in which the declarative and control aspects are merged and confused together in a mass of pointers. An interesting feature of rewriting logic is that, thanks to its reflective capabilities, strategies themselves can also be specified in a declarative way by means of rewrite rules at the metalevel. That is, by rewrite rules that guide one level up how the inference rules of the system we are interested in are applied at the ``object level.'' This reflective approach supports reasoning about metalevel features by means of reflective reasoning techniques. The Maude language maintains this modular distinction between rewrite rules and strategies to execute them: a Maude system module is a rewrite theory with no strategy information. In general, the same rewrite theory describing an inference system may be executed with different strategies, which may each have specific advantages depending on the purpose at hand. Therefore, in Maude strategies can be defined by rules at the metalevel in its META-LEVEL module. There is great freedom to define in this way different strategy languages, which we can then use to specify and execute strategies for any object theory of interest. More recently, we have undertaken the project of providing a basic strategy language for Maude. To make the language easier to use we have made it available at the object level instead of at the metalevel. Our first prototype implementation defined the language at the metalevel in the usual reflective way, while keeping the user interface at the object level for ease and convenience. Our strategy language allows the definition of strategy expressions that control the way a term is rewritten. Our design is based on a strict separation between the rewrite rules and the strategy expressions, that are specified in separate modules. Thus, in our proposal it is not possible to use strategy expressions in the rewrite rules of a system module. In fact, this separation makes possible defining different strategy modules to control in different ways the rewrites of a single system module. A strategy is described as an operation that, when applied to a given term, produces a set of terms as a result, given that the process is nondeterministic in general. The basic strategies consist of the application of a rule (identified by the corresponding rule label) to a given term, and allowing variables in a rule to be instantiated before its application by means of a substitution. For conditional rules, rewrite conditions can be controlled also by means of strategies. Basic strategies are combined by means of, among others, typical regular expression constructions (concatenation, union, and iteration), if-then-else, combinators to control the way subterms of a given term are rewritten, and recursion. In addition to several short examples, the language has been successfully used in the implementation of the operational semantics of the ambient calculus, the two-level operational semantics of the parallel functional programming language Eden, and basic completion algorithms. After validating our language design experimentally, we have then developed a direct implementation of our strategy language at the C++ level, at which the Maude system itself is implemented, to make the language a stable new feature of Maude, and to allow a more efficient execution.

Final Remarks (17:00‑17:30)