NASA/CP-2003-212448 

Design and Application of Strategies/Tactics 

in Higher Order Logics 

Edited by 

Myla Archer 

Naval Research Laboratory, Washington, D. C. 

Ben Di Vito 

Langley Research Center, Harnpton, Virginia 

C&ar Murloz 

National Institute of Aerospace, Harnpton, Virginia 

1 September 2003 

1 
The NASA STI Program Office . . . in Profile 

Since its founding, NASA has been dedicated 

to the advancement of aeronautics and space 

science. The NASA Scientific and Technical 

Information (STI) Program Office plays a 

key part in helping NASA maintain this 

important role. 

The NASA STI Program Office is operated 

by Langley Research Center, the lead center 

for NASA’s scientific and technical 

information. The NASA STI Program Office 

provides access to the NASA STI Database, 

the largest collection of aeronautical and 

space science STI in the world. The Program 

Office is also NASA’s institutional 

mechanism for disseminating the results of 

its research and development activities. 

These results are published by NASA in the 

NASA STI Report Series, which includes the 

following report types: 

TECHNICAL PUBLICATION. Reports of 

completed research or a major significant 

phase of research that present the results 

of NASA programs and include extensive 

data or theoretical analysis. Includes 

compilations of significant scientific and 

technical data and information deemed to 

be of continuing reference value. NASA 

counterpart of peer-reviewed formal 

professional papers, but having less 

stringent limitations on manuscript length 

and extent of graphic presentations. 

TECHNICAL MEMORANDUM. 

Scientific and technical findings that are 

preliminary or of specialized interest, e.g., 

quick release reports, working papers, and 

bibliographies that contain minimal 

annotation. Does not contain extensive 

analysis. 

CONTRACTOR REPORT. Scientific and 

technical findings by NASA-sponsored 

contractors and grantees. 

0 CONFERENCE PUBLICATION. 

Collected papers from scientific and 

technical conferences, symposia, seminars, 

or other meetings sponsored or 

co-sponsored by NASA. 

technical, or historical information from 

NASA programs, projects, and missions, 

often concerned with subjects having 

substantial public interest. 

0 TECHNICAL TRANSLATION. Englishlanguage translations of foreign scientific 

and technical material pertinent to 

NASA’s mission. 

0 SPECIAL PUBLICATION. Scientific, 

Specialized services that complement the 

STI Program Office’s diverse offerings 

include creating custom thesauri, building 

customized databases, organizing and 

publishing research results . . . even 

providing videos. 

For more information about the NASA STI 

Program Office, see the following: 

0 Access the NASA STI Program Home 

Page at http://www.sti.nasa.gov 

help@sti.nasa.gov 

Desk at (301) 621-0134 

6214390 

0 Write to: 

0 E-mail your question via the Internet to 

0 Fax your question to the NASA STI Help 

0 Phone the NASA STI Help Desk at (301) 

NASA STI Help Desk 

NASA Center for Aerospace Information 

7121 Standard Drive 

Hanover, MD 21076-1320 
NAS A/CP-2003-2 12448 

Design and Application of Strategies/Tactics 

in Higher Order Logics 

Edited by 

Myla Archer 

Naval Research Laboratory, Washington, D. C. 

Ben Di Vito 

Langley Research Center, Hampton, Virginia 

Char Muiioz 

National Institute of Aerospace, Hampton, Virginia 

Proceedings of a workshop sponsored by the Naval 

%search Laboratory, the National Aeronautics and 

Space Administration, and the National Institute of 

Aerospace and held in &me, Italy 

September 8, 2003 

National Aeronautics and 

Space Administration 

Langley Research Center 

Hampton, Virginia 23681-2199 

I September 2003 
Available from: 

NASA Center for Aerospace Information (CASI) 

7121 Standard Drive 

Hanover, MD 21076-1320 

(301) 621-0390 

National Technical Information Service (NTIS) 

5285 Port Royal Road 

Springfield, VA 22161-2171 

(703) 605-6000 
Preface 

The topic of theorem proving strategies has generated considerable interest in the theorem proving community. In particular, there is an ongoing series of workshops associated with CADE entitled Strategies 

in Automated Deduction, as well as a special issue of Annals of Mathematics and Artificial Intelligence 

with the same title. More information on this workshop series and the special issue can be found at 

http://www.logic.at/strategies/. Much of the emphasis in the Strategies in Automated Deduction workshops has been on proof strategies and heuristic based proof search/planning in first-order automatic theorem 

proving. 

In principle, first-order theorem proving does not require user guidance; strategies in this context aim at 

faster proof discovery. By contrast, theorem proving in higher-order logics typically requires interactive user 

guidance. Thus, although strategies in higher-order logics are also sometimes intended for automatic theorem 

proving, they are also commonly aimed at providing bases for more efficient interactive proof construction. 

Higher order logic theorem provers support interactive reasoning by providing the user with a set of basic 

proof commands. For reasons of efficiency, the effects of these commands may include reasoning based on 

anticipate, and thus interfere with fine control in user strategies; however, it does allow simple strategies to 

be relatively powerful. Moreover, considerable support for fine control in user strategies in higher-order logic 

theorem provers is provided by their expressive proof scripting languages that include powerful capabilities, 

e.g., pattern matching formulas in a sequent, or as in PVS, tracking the history of formulas through formula 

labels. 

As a result of the different flavor of theorem proving in higher-order logics versus theorem proving in 

first order logic, the art of strategy writing in PVS and other higher-order logic theorem provers is worth 

studying in its own right. Current knowledge about writing PVS strategies in particular has been limited to 

folklore, despite the powerful capabilities provided in PVS for implementing user-defined strategies. Thus, 

our first Workshop on The Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 

2003) is focused on PVS. For PVS, we wish to distill what is known from successful efforts, move beyond 

the folklore stage, and spawn more widespread practice of the strategic arts. 

This Proceedings includes both a paper from the implementors of PVS providing guidance for PVS strategy writers and a tutorial on PVS strategy writing distilled from the experience of three PVS users who have 

written extensive sets of PVS user strategies. Following these are three full papers from the higher-order logic 

theorem proving community that discuss PVS strategies to enhance arithmetic and other interactive reasoning in PVS; implementing first-order tactics in higher-order provers; and a proposed technique for specifying 

small step semantics that can be used in multiple higher order logic theorem provers, with illustrations from 

both Coq and PVS. The Proceedings concludes with three position papers for a panel session that discuss 

three settings in which development of PVS strategies is worth while. 

I decision procedures. This can make the precise effects of these commands on proof goals sometimes hard to 

I 

... 

111 
Organization 

STRATA 2003 is organized by the Naval Research Laboratory (NRL), NASA Langley Research Center 

(NASA LaRC), and the National Institute of Aerospace (NIA). 

STRATA 2003 Organizing Committee 

Conference Chair: Myla Archer (NRL) 

Ben Di Vito (NASA) 

Cksar A. Muiioz (NIA) 

iv 
Table of Contents 

Invited Papers 

Writing PVS Proof Strategies .............................................................. 

Sam Owre, Natarajan Shanlcar 

Developing User Strategies in PVS: A Tutorial.. .............................................. 

Myla Archer, Ben Di Vito, Char Muiioz 

1 

16 

Regular Papers 

Strategy-Enhanced Interactive Proving and Arithmetic Simplification for PVS .................... 

Ben L. Di Vito 

43 

First,-Order Proof Tactics in Higher-Order Logic Theorem Provers. .............................. 

Joe Hurd 

56 

Coq Tacticals and PVS Strategies: A Small Step Semantics ..................................... 

Florent Kirchner 

69 

Position Papers 

Rippling in PVS .......................................................................... 84 

A. A. Adams, L. A. Dennis 

Generating Proof-Specific Strategies for PVS ................................................. 

Pertti Kellomaki 

91 

Developing Strategies for Specialized Theorem Proving about Untimed, Timed, and Hybrid 1/0 

Automata.. .............................................................................. 103 

Sayan Mitra, Myla Archer 

Author Index ........................................................................ 109 

V 
Writing PVS Proof Strategies* 

Sam Owre and Natarajan Shankar 

Computer Science Laboratory 

SRI International 

Menlo Park CA 94025 USA 

{owre, shankar}@csl.sri.com 

http://vuu.csl.sri.com/"{owre, "shankar} 

Phone: +1 (650) 859-(5114, 5272) Fax: +1 (650) 859-2844 

Abstract. PVS (Prototype Verification System) is a comprehensive framework for writing formal 

logical specifications and constructing proofs. An interactive proof checker is a key component of PVS. 

The capabilities of this proof checker can be extended by defining proof strategies that are similar to 

LCF-style tactics. Commonly used proof strategies include those for discharging typechecking proof 

obligations, simplification and rewriting using decision procedures, and various forms of induction. We 

describe the basic building blocks of PVS proof strategies and provide a pragmatic guide for writing 

sophisticated strategies. 

1 Introduction 

Writing correct proofs is an activity that combines creativity and tedium. The creative aspect of proof 

development is in the construction of definitions, lemmas, and theorems, the choice of high-level proof ideas, 

and in recovering gracefully from failed proof attempts. The tedium is in checking that all the low-level details 

have been worked out correctly. Automated proof checkers are meant to verify the low-level proof steps 

corresponding to the high-level proof guidance given interactively. Automated theorem provers, on the other 

hand, are required to discover both the high-level outline and the low-level details required to prove or refute a 

given conjecture. Such theorem provers have yet to achieve the level of sophistication needed to reliably tackle 

conjectures with interesting mathematical content. Early proof checkers required proofs to be given entirely 

in terms of low-level inferences (such as modus ponens or instantiation) [McC62,dB80,BB74]. The second 

generation of proof checkers included a language for defining compound proof steps that could be justified 

solely in terms of primitive inferences. PVS builds on these prior approaches. PVS employs an expressive 

specification language based on higher-order logic with a type system that includes predicate subtypes, 

dependent types, and abstract datatypes. These features not only allow mathematical ideas to be captured 

with cogency, but they also interact synergistically with the inference procedures. PVS allows complex proof 

strategies to be built up from quite sophisticated primitive inference steps that employ arithmetic decision 

procedures, rewriting, and simplification. The advantage of the PVS approach is that it exploits the efficiency 

of modern automated deduction technologies in the construction of powerful and flexible proof strategies. 

The drawback is that the trusted code base is fairly large since it includes the typechecker and several 

complex inference procedures. 

PVS has a simple language for defining proof strategies. A number of PVS users have used the PVS strategy 

language for defining customized proof strategies for a variety of applications. Typically, a user builds up 

a significant body of domain knowledge in a field like finite set theory, analysis, graph theory, algebra, or 

trigonometry. Proofs in specific applications use this domain knowledge in a stylized format. Proof strategies 

are defined to package such patterns of usage so that they can be used by non-experts. The PC/DC system [SS94] provided a front-end to PVS that contained various proof strategies for reasoning with a real-time 

interval temporal logic called the duration calculus. The TAME system [ArcOO] from the US Naval Research 

Funded by Naval Research Laboratory Contract N00173-00-C-2086 and National Aeronautical and Space Agency 

Contract NASA NAG-1-02101. 
2 Sam Owe and Natarajan Shankar 

Laboratory provides a collection of custom proof strategies for carrying out proofs of 1/0 automata at a 

level of detail that is reasonably faithful to the original hand proofs. The LOOP project [vdBJOl] at the 

University of Nijmegen is another example of a substantial investment in PVS proof strategies for automating proofs of Java code. Work on PVS strategies at the NASA Langley Research Center has yielded the 

Manip package [Vit02] for algebraic simplification strategies and the Field package [MMOl] (modeled on 

the eponymous Coq library) for simplifying subgoals involving real arithmetic. 

User-defined proof strategies are thus an important mechanism for customizing the proof-checking capabilities 

of PVS toward specific domains. This paper is a brief tutorial on writing advanced proof strategies in PVS. 

It is directed primarily at PVS users who are interested in achieving greater levels of automation and 

customization. We first provide some background on proof checking in general (Section 2), and on PVS 

in particular (Section 3). Some of the PVS internal data structures are reviewed in Section 4. Section 5 

introduces the strategy language. We explain the construction of some simple proof strategies in Section 6, 

and cover more advanced techniques in Section 7. Conclusions and future directions are sketched in Section 8. 

Due to space limitations, the discussion of strategies and PVS interfaces here contains many gaps. A larger 

document [OS031 covering the PVS application programmer interface is currently under development. 

2 Background 

Automated proof checking has an illustrious history. In the seventeenth century, Gottfried Leibniz had already 

conceived of a language in which knowledge could be systematized so that a logic engine could be used to 

resolve arguments. A similar fancy inspired Boole in the development of Boolean algebra. The mechanization 

of mathematics started to seem more realistic with the formalization of various branches of mathematics at 

the dawn of the twentieth century through the work of Dedekind, Peano, Cantor, Frege, Russell, Whitehead, 

and Hilbert. At the beginning of his celebrated article on the incompleteness theorem [God92], Godel explicitly acknowledges the possibility of mechanically checking mathematical proofs. Turing’s article Computing 

Machinery and Intelligence [Tur63] also proposed the use of computers as proof engines. Bush’s famous 

article As We May Think [Bus451 asserts the centrality of verified reasoning in scientific computing.’ 

Automated reasoning was actively investigated in the 1950s through the work of Davis, Newell, Shaw, and 

Simon, Wang, Gilmore, and Prawitz. These works were not concerned with proof checking. The earliest 

work on this topic is due to McCarthy [McC62] in the 1960s. The AUTOMATH project was initiated by 

de Bruijn [dB807NGdV94] in the mid-1960s and introduced many key ideas. Jutting [vBJ79] used AUTOMATH to verify Landau’s Foundations of Analysis [LanSO]. Bledsoe’s IMPLY system [BB74] was developed during the late 1960s and early 1970s and applied to proofs in set theory and analysis. The LCF 

family of systems [GMW79] includes such systems as Nuprl [CAB+86], HOL [GM93], Coq [CCF+95], Isabelle [Pau94], HOL-Lite [HarOO], and LEG0 [LP92]. LCF is best known for introducing the ML programming language [GMM+77,MTH90] as a way of defining proof tactics and tacticals. The Mizar proof 

checker [Rud92] constitutes one of the most sustained and coordinated efforts at mechanizing a large body 

of mathematics. 

3 Brief Overview of PVS 

Work on the PVS proof checker began at SRI International in 1990. PVS has been strongly influenced in 

its design by its immediate predecessor, the EHDM system [EHD93]. PVS also builds on the prior work 

in automated proof checking, especially the work of Bledsoe and the LCF family of systems, the work by 

Shostak [Sho84] and Nelson and Oppen [NO791 on ground decision procedures, and the proof strategies 

employed by the Boyer-Moore theorem prover [BM79,BM88]. Like HOL and EHDM, the PVS specification 

To quote Bush: Logic can become enormously dificult, and it would undoubtedly be well to produce more assurance 

in its use. . . . We may some day click off arguments on a machine with the same assurance that we now enter sales 

on a cash register. 
Writing PVS Proof Strategies 3 

language is based on classical higher-order logic but with added features like predicate subtypes, dependent 

types, and abstract datatypes. Features similar to subtypes and dependent types also appear in other logics, 

but in PVS, the decision procedures provide crucial support for processing specifications that exploit these 

features. With predicate subtyping, typechecking is undecidable in general, but the PVS typechecker verifies 

simple type correctness and generates proof obligations corresponding to the subtypes. These proof obligations can be proved automatically or interactively, and the majority of them succumb easily to simple proof 

strategies that rely heavily on the PVS decision procedures. 

We will use the simple example of the language equivalence between deterministic and nondeterministic 

finite automata to illustrate both the PVS language and proof strategies. A PVS specification is a collection 

of theories. A theory is a list of declarations of types, constants, and formulas. The declarations of types 

and constants can include definitions. Declarations without definitions are said to be uninterpreted. A theory 

can also take parameters that are types, individuals, or (instances of) theories. The DATATYPE declaration 

list introduces an abstract datatype with two constructors: null representing the empty list, and cons 

which adds an element to the front of a list. The accessors corresponding to cons are car, which returns 

the leading element, and cdr which represents the remainder of the list minus the leading element. The 

list datatype when typechecked, generates several theories that contain a various axioms and operations, 

including induction principles and recursion operators. The list datatype is introduced in the PVS prelude 

which contains formalizations of a number of basic datatypes. 

list IT: TYPE]: DATATYPE 

BEGIN 

null: null? 

cons (car: T, cdr:list):cons? 

END list 

The theory DFA formalizes deterministic automata where the number of states is not necessarily finite. The 

states of the automata are drawn from the uninterpreted type state in which there is a distinguished start 

state, and a designated set of final states final?. The type set [state] is an abbreviation for the predicate 

type [state -> bool] . The automaton operates on an alphabet Sigma, and the transition function delta 

maps a given alphabet and source state to a target state. The operation DELTA iterates delta and is defined 

to take a string of alphabets from Sigma and a source state and return a target state. DAccept? is a 

predicate that accepts a string if the final state returned by DELTA is a valid final state. 

DFA : THEORY 

BEGIN 

Sigma : TYPE 

state : TYPE 

start : state 

delta : [Sigma -> [state -> state]] 

final? : setCstate1 

DELTA( (string : list [Sigma] 1) ( (S : state) 1 : 

RECURSIVE state = 

(CASES string OF 

null : S, 

cons(a, x) : delta(a) (DELTA(x)(S)) 

ENDCASES) 

MEASURE length(string1 

DAccept?((string : list[Sigmal)) : bool = 

final?(DELTA(string) (start)) 

END DFA 
4 

The theory NFA for nondeterministic automata is similar to DFA. The type of ndelta differs from that 

of delta in returning a set of states rather than a single state. The recursive operation NDELTA similarly 

processes a string with respect to a state to return a set of states. The nondeterministic automaton accepts 

this string if the set of states returned by NDELTA contains a final state. 

NFA : THEORY 

Sam Owre and Natarajan Shankax 

BEGIN 

nSigma : TYPE 

nstate : TYPE 

nstart : nstate 

ndelta : [nSigma -> [nstate -> set[nstate]]] 

nf inal? : set Cnstatel 

NDELTA( (string : list [nSigmal)) ( (s : nstate) : 

RECURSIVE set [nstatel = 

(CASES string OF 

null : singleton(s), 

cons(a, x): lub(image(ndelta(a), NDELTA(x) (SI)) 

ENDCASES) 

MEASURE length (string) 

Accept?((string : list[nSigma])) : boo1 = 

member(r. NDELTAcstring) (nstart))) 

(EXISTS (r : (nfinal?)) : 

END NFA 

The language equivalence between the two automaton is captured by the theory equiv. The NFA theory 

is imported into the theory equiv. The symbols declared in NFA are used to create an instance of DFA 

that corresponds to the subset construction used to show the equivalence. Here, the alphabet Sigma is 

interpreted as nSigma, the state type is interpreted as the power set of the type nstate, and start, delta, 

and final? are also suitably defined. The resulting interpretation of the theory DFA is used to show the 

equivalence between NFA and DFA in two steps. The lemma main states the equivalence between NDELTA and 

the interpreted DELTA operation. The theorem equiv states the equivalence between the strings accepted by 

the NFA and those accepted by the corresponding DFA. 

equiv: THEORY 

BEGIN 

IMPORTING NFA 

NFADFA : THEORY = 

DFA{{Sigma = nSigma, 

state = set [nstatel , 

start = singleton(nstart1, 

delta( (symbol : nsigma)) ((s : set [nstatel 1) = 

final?( (S : set [nstatel 1) = 

lub(image(ndelta(symbol), SI), 

(EXISTS (r : (nfinal?)) : member(r, S))}} 

main: LEMMA 

(FORALL (x : list[nSigma]), (s : nstate) : 

NDELTA(x) (s) = DELTA(x) (singleton(s))) 

equiv: THEOREM 

(FORALL (string : list CnSigmal) : 

Accept?(string) IFF DAccept?(string)) 

END equiv 
Writing PVS Proof Strategies 5 

The first proposition, main, is proved by invoking the induct-and-simplif y strategy to employ list induction 

on the parameter x. The second proposition, equiv, is is proved by employing the grind strategy to apply 

rewrite rules, simplification using the decision procedures, and heuristic quantifier instantiation. 

main : 

I ------- 

(1) (FORALL (x: list[nSigma]), (s: nstate): 

NDELTA(x) (s) = DELTA(x) (singleton(s))) 

Rule? (induct-and-simplify "x") 

NDELTA rewrites NDELTA(nul1) (s! 1) 

DELTA rewrites DELTA(null)(singleton(s!l)) 

NDELTA rewrites NDELTA(cons(cons1-var!l. cons2-var!l))(s!l) 

DELTA rewrites DELTA(cons(cons1-var!l, cons2~var!l))(singleton(s!l)) 

By induction on x, and by repeatedly rewriting and simplifying, 

Q.E.D. 

to singleton(s!l) 

to singleton(s!l) 

to lub(image(ndelta(cons1-var! 11, NDELTA(cons2_var! 1) (s! 1))) 

to lub(image(ndelta(cons1-var! 11, DELTA(cons2_var!l) (singleton(s! 1)))) 

equiv : 

I ------- 

(1) (FORALL (string: list[nSigmal): Accept?(string) IFF DAccept?(string)) 

Rule? (grind :theories "equiv") 

main rewrites NDELTAbtring) (nstart) 

member rewrites member(r, DELTA(string)(singleton(nstart))) 

Accept? rewrites Accept? (string) 

member rewrites member(r, DELTA(string)(singleton(nstart))) 

DAccept? rewrites DAccept?(string) 

Trying repeated skolemization, instantiation, and if-lifting, 

Q.E.D. 

to DELTA(string)(singleton(nstart)) 

to DELTA(string)(singleton(nstart))(r) 

to EXISTS (r: (nfinal?)): DELTA(string)(singleton(nstart))(r) 

to DELTA(string1 (singleton(nstart) (r) 

to EXISTS (r: (nf inal?)) : DELTA(string1 (singleton(nstart)) (r) 

The inner workings of the grind strategy are described in Section 6, and those of induct-and-simplify 

are explained in Section 7. 

4 PVS Data Structures 

In writing sophisticated PVS strategies, it is useful to have a basic understanding of the way specifications 

are represented in PVS. Most data are maintained in the form of CLOS (Common Lisp Object System) objects. The appropriate classes are defined using a Lisp macro (defcl classname (superclasses) slots). 

Typical classes are 

1. module: Contains declarations and judgements corresponding to a PVS theory. The expression 

(get-theory "foot') returns the theory module named foo, and (show (get-theory "foo")) displays 

the slots and their contents. 
6 Sam Owre and Natarajan Shankar 

2. type-decl: Type declaration. 

3. f ormula-decl: Formula declaration. 

4. funtype: Function type. 

5. name-expr: Name expression, i.e., constants or variables. 

6. application: Application expressions. 

4.1 Proof State 

PVS proofs employ Gentzen’s sequent calculus as the basic representation. A PVS sequent has of the form 

{ - l} antecedentformuZal 

[-m] antecedentformula, 

{ l} succedentformuZal 

!- 

[n] succedentfonnula, 

Here, the negatively numbered formulas are the antecedents of the sequent, and the positively numbered 

formulas are the succedents. Proofs operate by reducing a goal sequent to subgoal sequents in response to 

a proof command. Formulas in a subgoal sequent that appear in the parent sequent are numbered within 

square brackets, and the newly introduced formulas are numbered within braces. Internally, the proof state 

is a CLOS object with slots including the current-goal sequent, the parent-proofstate, and the active 

current-subgoal. The current goal is a sequent whose main slot s-formulas holds a list of s-forms. The 

s-f orms are themselves CLOS objects with a formula field that contains the PVS expression corresponding 

to a sequent formulas. The antecedent formulas are those that are negated. The list of s-f oms interleaves 

both antecedent and succedent formulas. The proof state also contains fields corresponding to the parent 

proofstate and the subgoal proof states. The current proof state within a proof is accessible through the 

global variable *ps*. The Lisp command (show ob) displays the values of the slots of a CLOS object ob. 

5 The Strategy Language 

The core language for defining strategies is quite simple, but this does not cover the large number of syntactic 

and semantic operations that are required for writing more sophisticated strategies. A PVS proof command 

is either a primitive proof command such as flatten, split, auto-rewrite, or simplify, or a compound 

strategy that is constructed from smaller proof commands. PVS does allow new primitive inferences to be 

added, but such additions must be carried out with circumspection since they can introduce unsoundness. 

Strategies, on the other hand, are conservative, since it is possible to verify the validity of the proof when 

all the strategies have been expanded into primitive proof steps. 

The primitive proof commands in PVS include 

1. flatten for disjunctive simplification. 

2. split for conjunctive splitting. 

3. skolem for eliminating universal-strength quantifiers. 

4. inst for instantiating existential-strength quantifiers. 

5. auto-rewrite for installing rewrite rules for use during simplification. 

6. simplify for simplification using rewriting and ground decision procedures. 

PVS strategies can either be in glassbox form so that only the expanded form of the strategy is visible in 

the resulting subproof, or in blackbox form where it is applied as a single atomic proof step and the internal 

steps are not recorded. The Common Lisp constructs for defining strategies are: 
Writing PVS Proof Strategies 7 

1. (defstrat name arguments body help-string format-string): Defines a glassbox strategy 

named name with arguments given in arguments. The arguments are given as a list of required and optional arguments, where the optional ones are preceded by the keyword &optional. The definition is given 

in body. The help-string contains the documentation for the proof command, and format-string is 

a Lisp format control string that is applied to the arguments to generate the commentary that appears 

when the proof command is applied. The help-string and format-string are optional. 

2. (defrule name arguments body help-string format-string): Defines a blackbox strategy that is 

otherwise similar to def strat. 

3. (defstep name arguments body help-string format-string): Defines a blackbox strategy named 

name and a glassbox version named name$. 

The language in which the strategies are defined involves just a few constructs: 

1. (if lisp-ezpr strat-ezprl strat-ezpr2): Returns the value of strat-ezpr2 if the evaluation of 

Common Lisp expression lisp-expr (relative to the current proof state) returns nil, and the value of 

strat-exprl, otherwise. 

2. (try strat-ezprl strat-ezpr2 strat-ezpr3): First applies strat-ezprl to the current proofstate. 

This could either 

(a) Have no effect, in which case, strat-ezpr3 is invoked. 

(b) Complete the subproof and strat-ezpr2 and strat-ezpr3 are not used. 

(c) Generate a failure, which is propagated to the parent proof state. 

(d) Generate subgoals, and strat-ezpr2 is applied to these subgoals, and strat-ezpr3 is not evaluated. 

3. (let ((war1 lisp-ezprl). . . (varl lisp-ezprl)) strat-ezpr): Binds vari to the value of 

lisp-expri in strat-expr. 

4. (skip) : Does nothing. 

5. (fail) : Signals failure to trigger backtracking. 

6. (quote strat-ezpr): Evaluates to strat-ezpr but is useful when the strategy is constructed as a Lisp 

s-expression. 

Note that (try (skip) A B) is equivalent to B, whereas (try (try (fail) A B) C D) is equivalent to D. 

Definitions can also involve recursion. There are some simple strategies that are analogous to LCF tacticals 

in that they are used to direct other strategies. The else strategy applies stepl, and backtracks to step2 

if the stepl does nothing. 

(defstrat else (stepl step21 

(try stepl (skip) step2) 

“If stepl fails, then try step2, otherwise behave like stepl“ 

The repeat strategy applies step to the current goal, and recursively applies the strategy to the first 

resulting subgoal. It thus repeats a step along the “main” branch of a proof. Recall that the global variable 

*ps* captures the current proofstate relative to which the strategy is being evaluated. The simpler strategy 

repeat* repeats a step along all the branches of a proof. Either of these strategies could fail to terminate so 

it is important to ensure that they are only applied to steps that eventually do nothing. 

(defstrat repeat (step) 

(try step (if (equal (get-goalnum *ps*) 1) 

(repeat step) 

(skip) 1 

(skip) 1 

“Successively apply STEP along main branch until it does nothing.“) 

(def strat repeat* (step) 

(try step (repeat* step) (skip)) 

‘Successively apply STEP until it does nothing.”) 
8 Sam Owre and Natarajan Shankar 

The propositional simplification strategy applies disjunctive flattening to the sequent and recursively invokes 

itself on the subgoals. When disjunctive flattening is exhausted, then conjunctive splitting is employed, 

and again, the strategy is recursively invoked until there are no further top-level disjunctive or conjunctive 

connectives in the sequent. The recursive invocation of prop uses the expansive prop$. This makes it easier 

to observe the internal behavior by invoking the expansive strategy prop$. 

~~ ~ ~ ~ ~ 

(defstep prop (1 

(try (flatten) (prop$) (try (split) (prop$) (skip)) 

"A black-box rule for propositional simplification." 

''Applying propositional simplification") 

6 Simple Proof Strategies 

We now examine the construction of the grind strategy as an instance of a simple proof strategy that 

combines a number of smaller proof steps. This strategy takes a number of optional arguments with possible 

default values. The strategy installs rewrite rules from the definitions in the current sequent (and, transitively, 

the definitions used in these), the given theories and rewrites, but excluding those listed in exclude. 

This is followed by propositional simplification using the bddsimp command, and assert which carries out 

simplification using the ground decision procedures and the installed rewrite rules. The command replace* 

is used to apply the antecedent equalities in the sequent as rewrites. The reduce command (described below) 

is invoked with a number of arguments in keyword form. In a call to the strategy, the required arguments 

must be given in order but the optional arguments can be given in keyword form, as illustrated in the call 

to reduces. 

(def step grind (&optional (def s ! ) 

theories rewrites exclude (if-match t) 

(updates? t) polarity? (instantiator inst?) 

(let-reduce? t)) 

(then 

(install-rewrites$ :defs defs :theories theories 

:rewrites rewrites :exclude exclude) 

(then (bddsimp)(assert :let-reduce? let-reduce?)) 

(replace*) 

(reduce$ :if-match if-match :updates? updates? 

:polarity? polarity? :instantiator instantiator 

:let-reduce? let-reduce?)) 

IS . . . 

"Trying repeated skolemization, instantiation, and if-lifting") 

The reduce command repeatedly applies the bash command and then executes replace* on any subgoals. 

ldefstep reduce (&optional (if-match t)(updates? t) polarity? 

(instantiator inst?) (let-reduce? t)) 

(repeat* (try (bash$ :if-match if-match :updates? updates? 

:polarity? polarity? :instantiator instantiator 

:let-reduce? let-reduce?) 

(replace*) 

(skip) )) II II ... 

"Repeatedly simplifying with decision procedures, rewriting, 

propositional reasoning, quantifier instantiation, skolemization, 

if-lifting and equality replacement") 

The bash command is the core of reduce. It first executes assert, and then uses the if construct to 

selectively use an instantiator to instantiate any existential-strength quantifiers. The repeat loop contains 
Writing PVS Proof Strategies 9 

the command skolem-typepred that introduces constants for universal-strength quantifiers followed by 

disjunctive flattening. Any embedded conditionals are then lifted to the top level of the sequent with the 

lif t-if command. The updates? flag converts update expressions into conditional form. 

(defstep bash (&optional (if-match t)(updates? t) polarity? 

(instantiator inst?) (let-reduce? t)) 

(then (assert :let-reduce? let-reduce?) (bddsimp) 

(if if -match (let ((command (generate-instantiator-command 

if-match polarity? instantiator))) 

command) (skip) 

(repeat (then (skolem-typepred)(flatten))) 

(lift-if :updates? updates?)) 11 11 ... 

"Simplifying with decision procedures, rewriting, propositional 

reasoning, quantifier instantiation, skolemization, if-lifting.") 

7 Advanced Proof Strategies 

We first examine a strategy that while simple still illustrates features that are basic to the more advanced 

strategies. The strategy replace-extensionality replaces all occurrences of a term f by a term g, where 

the equality f = g holds by extensionality. The type of f and g must be either a function, record, tuple, or 

a datatype in order for a suitable extensionality scheme to be available. The optional argument expected? 

is there in the rare event that the type of f is ambiguous. The optional argument keep? is given as T when 

the equality f = g is to be retained at the end of the step. 

Arguments to strategies that are PVS expressions can be either in the form of concrete syntax as a string or 

as abstract syntax which is already parsed or even typechecked. Strategies invoked directly by the user often 

contain arguments in the form of concrete syntax, but those invoked from another strategy may have their 

arguments in a parsed and typechecked form. The operation pc-parse parses the expression if needed and its 

second argument is the expected nonterminal, usually either ' type-expr or ' expr. The operation typecheck 

typechecks the parsed expression relative to a given context. The global variable *current-context* binds 

the context corresponding to the current goal. The function pc-typecheck is a variant of typecheck that 

first looks for an occurrence of the given expression in the current sequent. Since the input expression is 

likely to occur in the sequent, this saves the expense of typechecking. The strategy applies extensionality 

step to the given expected type, if there is one. Otherwise, extensionality is applied to the type of the 

first or second argument. If the extensionality step succeeds, then it adds the appropriate extensionality 

axiom as the first antecedent formula. This formula is then instantiated with the typechecked forms of 

the f and g arguments. The instantiated axiom is then subject to conjunctive splitting. The first branch 

corresponds to the conclusion equality between f and g. The replace command is applied to this equality. 

If the keep? argument is nil, which is its default value, then equality formula is deleted. The remaining 

subgoals correspond to the conditions on the instance of the extensionality axiom, and these are discharged 

by successive applications of skolem! , beta, and assert. The instantiation step might have generated TCCs, 

and the assert step is applied to the subgoals corresponding to these TCCs. 
10 Sam Owre and Natarajan Shankar 

'defstep replace-extensionality (f g &optional expected keep?) 

(let ( (tt (when expected (typecheck (pc-parse expected 'type-expr) 

:context *current-context*)))) 

(let ((ff (pc-typecheck (pc-parse f 'expr) 

(gg (pc-typecheck (pc-parse g 'expr) 

:expected tt)) 

:expected tt))) 

(let ((tf (type ff)) 

(tg (type gg))) 

(try (if tt (extensionality tt) 

(try (extensionality tf) (skip) 

(extensionality tg))) 

(branch (inst - ff gg) 

((branch (split -1) 

((then (replace -1) 

(if keep? (skip) 

(delete -1) 1) 

(then* (skolem! 1) 

(beta 1);;changed from + to 1. 

(assert 1) 1) ) 

(assert))) 

(skip) 1) 1) I, II ... 

"Replacing 'a by -a using extensionality") 

The apply-extensionality strategy is used to prove a sequent with a consequent equality by employing 

replace-extensionality to replace the left-hand side of the equality by its right-hand side. The optional 

argument fnum is + (indicating the consequent formulas) by default. The command first selects the s-forms 

corresponding to fnum using select-seq. The first equality among these formulas is used as the candidate 

for applying replace-extens ional it y. The replace-ext ens ionalit y step can generate subgoals corresponding to TCCs, and the candidate formula can be deleted from these when the hide? flag is T. The 

skip-msg is a variant of skip that generates a comment. 
~~ 

Writing PVS Proof Strategies 11 

:defstep apply-extensionality (&optional (fnum +) keep? hide?) 

(let ( (sforms (select-seq (s-forms (current-goal *ps*)) 

(if (rnemq fnum '(* + -1) fnum 

(list fnum) 1)) 

(fmla (loop for sf in sforms thereis 

(when (equation? (formula sf)) 

(formula sf) 1 ) 

(lhs (when fmla (argsl frnla))) 

(rhs (when fmla (argsl fmla)))) 

(if fmla 

(try (replace-extensionality$ lhs rhs :keep? keep?) 

(let ( (fnums (f ind-all-sformnums (s-forms 

(then 

(current-goal *ps*)). 

'+ 

#'(lambda (x) 

(eq x frnla)))) 

(fnum (if fnums (car fnums) nil))) 

(if (and hide? fnum) (delete fnum) (skip))) 

(assert) ) 

(skip-msg "Couldn't find a suitable extensionality rule.")) 

(skip-msg "Couldn't find suitable formula for applying 

extensionality. ") ) ) 

. . . I' 

"Applying extensionality") 

The last strategy we describe is induct-and-simplify which is used in the DFA-NFA equivalence proof. 

This strategy is applied to a sequent with a consequent formula that universally quantifies the given variable 

var. Like grind, the install-rewrites strategy is used to install rewrite rules from the definitions in the 

formula, the given theories and rewrite rule names. The induct step instantiates the induction scheme: 

either the one named by name or the one that is appropriate for the variable var, and generates the base 

and induction steps. These are simplified using repeated application of skolemization, assert, propositional 

simplification, if-lifting, and instantiation. 
12 Sam Owe and Natarajan Shankm 

:def step induct-and-simplify (var &optional (fnum 1) name 

(defs t) 

(if -match best) 

theories 

rewrites 

exclude 

(instantiator inst?) 

1 

(then 

(install-rewrites$ :defs defs :theories theories 

(try (induct var fnum name) 

:rewrites rewrites :exclude exclude) 

(then 

(skosimp*) 

(assert);;To expand the functions in the induction conclusion 

(repeat (lift-if));;To lift the embedded ifs, 

;;then simplify, split, then instantiate 

;;the induction hypothesis. 

(repeat* (then (assert) 

(bddsimp) 

(skosimp*) 

(if if-match 

(let ((command 

(generate-instantiator-command 

if-match nil instantiator))) 

command) 

(skip) 1 

(lift-if)))) 

(skip) ) 1 I' . . . It 

"By induction on la, and by repeatedly rewriting and simplifying") 

The main step in the induct-and-simplif y is the induct command. This strategy first selects the candidate 

formula using select-seq with the input fnum. The induction variable is parsed and a new skolem constant 

is generated for it. This skolem constant is placed in a skolem-list corresponding to the outermost bound 

variables of the formula is generated with blanks (indicated by underscore) for those variables different from 

var. The body of the strategy is described below. 

(defstep induct (var &optional (fnum 1) name) 

(let ((fmla (let* ( (sforms (select-seq (s-forms (current-goal *ps*)) 

(list fnum)))) 

(when sforms 

(formula (car sf orms) 1) 1) 

(var (pc-parse var 'name)) 

(new-var-symbol (new-sko-symbol var *current-context*)) 

(skolem-list (if (f orall? fmla) 

(loop for x in (bindings fmla) 

collect (if (format-equal var (id x)) 

new-var-s ymbol 

'*-,,> 1

nil) 1) 

[see below]) 

II It ... 

"Inducting on "a-Q [ on formula "a-] "Q [ using induction scheme "a"] "1 

If there is a selected formula, the strategy applies simple-induct to generate a suitable instance of the 

induction scheme (determined by the type of var or the given name). The induction scheme instantiated 
Writing PVS Proof Strategies 13 

with the induction formula is beta-reduced using beta, instantiated using inst?, and conjunctively split 

using split. 

[if fmla 

(try (simple-induct var fmla name) 

(if *new-fmla-nums* 

(let ((fnum (find-sform (s-forms (current-goal *ps*)) 

'+ 

#' (lambda (sform) 

fmla) ) ) 1) 

(eq (formula sform) 

(then (beta) 

(let ((fmla 

(let ( (sf orms (select-seq 

(s-forms (current-goal *ps*)) 

(list fnum) 1) 

(when sf orms (formula (car sf orms) 1) 1) ) 

(then (let ((x (car *new-fmla-nums*))) 

(split XI)) 

(then (inst? x) 

[see below])))) 

(skip) 1 

(skip-msg "Could not find suitable induction scheme.")) 

(let ((msg (format nil "No formula corresponding to fnum "a" 

f num) 1 ) 

(skip-msg msg))) 

The position in the sequent of the original formula where induction was applied, might now be different. 

This position is recomputed. The formula, which must be universally quantified, is skolemized, and the 

corresponding universal quantifier in the induction scheme is instantiated with this skolem constant. The 

induction conclusion is discharged using prop leaving the base and induction subgoals. The residue of the 

induction formula is deleted in these subgoals. 

(let ( hum (f ind-sf orm 

(s-forms (current-goal *ps*)) 

'+ 

#' (lambda (sform) 

fmla) 1) 1) 

(eq (formula sform) 

(if (eql num fnum) 

(then (prop) 

(skolem fnum skolem-list) 

(inst - new-var-symbol) 

(prop)) 

(if num (delete num) 

(let ((newnums 

(loop for n 

in *new-fmla-nums* 

when (and (> n 0) 

collect n)) 

(<= n fnum)) 

(newfnum (+ fnum 

(delete newfnum))))) 

(length newnums)))) 
14 Sam Owe and Natarajan Shankar 

8 Conclusions 

Proof checkers, like any other usable form of software, must be programmable. User-defined proof strategies 

are a mechanism for defining common patterns of inference steps as a single proof command. Such defined 

strategies are conservative since they introduce no new unsoundness into the proof system. PVS proof 

strategies are thus similar in philosophy to LCF tactics. There are, however, some significant differences 

with LCF in that the primitive inferences in PVS encompass rewriting and the use of decision procedures. 

They are therefore much more complex than those typically employed by the LCF family of checkers. The 

PVS primitive proof commands are neither easily nor efficiently definable by means of tactics. By starting 

with powerful primitive inferences, it is possible to perform proof construction and strategy definition at a 

level of detail that is closer to that of a hand-proof. 

The core of the PVS strategy language is quite simple but writing effective strategies requires familiarity 

with Common Lisp and the underlying PVS data structures. The constructs of the strategy language are 

inspired by the recursive waterfall strategy employed by the theorem provers of Boyer and Moore. The prop 

and ground strategies are typical of such recursive waterfalls. 

Proof checking continues to pose significant challenges. There is still a lot of tedium associated with proof 

construction. These challenges can be addressed by identifying useful primitive proof steps for building proofs 

in specific domains, new techniques for building sound and efficient decision procedures, and systematic 

studies of the strategies that are used in constructing complex proofs. Proof strategies also need to be 

integrated with formalized libraries of mathematical knowledge. The PVS strategy language can be enhanced 

by means of a type system and a formal semantics (see Kirchner [Kir03]). 

References 

[ArcOO] 

[BB74] 

[BM79] 

[BM88] 

[Bus451 

[CAB+86] 

[CCF+95] 

[dB801 

[EHD93] 

[GM93] 

Myla Archer. TAME: Using PVS strategies for special-purpose theorem proving. Annals of Mathematics 

and Artificial Intelligence, 29( 1-4):139-181, 2000. 

W. W. Bledsoe and Peter Bruell. A man-machine theorem-proving system. Artificial Intelligence, 5:51-72, 

1974. 

R. S. Boyer and J S. Moore. A Computational Logic. Academic Press, New York, NY, 1979. 

R. S. Boyer and J. S. Moore. A Computational Logic Handbook. Academic Press, New York, NY, 1988. 

Vannevar Bush. As we may think. The Atlantic Monthly, 1945. Available at http: //vuu. theatlautic. 

com/unbound/flashbks/computer/bushf.htm. 

R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, 

T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith. Implementing Mathematics 

with the Nuprl Proof Development System. Prentice Hall, Englewood Cliffs, NJ, 1986. 

C. Comes, J. Courant, J.C. Filliatre, G. Huet, P. Manoury, C Paulin-Mohring, C. Munoz, C. Murthy, 

C. Parent, A. Saibi, and B. Werner. The Coq proof assistant reference manual, version 5.10. Technical 

report, INRIA, Rocquencourt, France, February 1995. 

N. G. de Bruijn. A survey of the project AUTOMATH. In J. P. Seldin and J. R. Hindley, editors, Essays 

on Combinatory Logic, Lambda Calculus and Formalism, pages 589-606. Academic Press, New York, NY, 

1980. 

Computer Science Laboratory, SRI International, Menlo Park, CA. User Guide for the EHDM Specification 

Language and Verification System, Version 6.1, February 1993. Three volumes. 

M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A Theorem Proving Environment for 

Higher-Order Logic. Cambridge University Press, Cambridge, UK, 1993. 

[GMM+77] M. Gordon, R. Milner, L. Morris, M. Newey, and C. Wadsworth. A metalanguage for interactive proof 

in LCF. Technical Report CSR-16-77, Department of Computer Science, University of Edinburgh, 1977. 

[GMW79] 

[God921 

[HarOO] 

M. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979. 

Kurt Godel. On Formally Undecidable Propositions of Principia Mathematica and Related Systems. 

Dover Publications, Inc., New York, NY, 1992. Translated by B. Meltzer, with an Introduction by R. B. 

Braithwaite. Originally published as a book in 1962. Article originally published in 1931. 

John Harrison. High-level verification using theorem proving and formalized mathematics. In David 

McAllester, editor, Automated Deduction-CADE-17, volume 1831 of Lecture Notes in Artificial Intelligence, pages 1-6, Pittsburgh, PA, June 2000. Springer-Verlag. 
Writing PVS Proof Strategies 15 

[Kir03] Florent Kirchner. Coq tacticals and PVS strategies: A small step semantics. In STRATA’U3, 2003. 

[LanGO] E. Landau. Foundations of Analysis. Chelsea, New York, NY, 1960. translated from the German original 

by F. Steinhardt. 

[LP92] Z. Luo and R. Pollack. The LEG0 proof development system: A user’s manual. Technical Report 

ECS-LFCS-92-211, University of Edinburgh, 1992. 

[McC62] J. McCarthy. Computer programs for checking mathematical proofs. In Recursive Function Theory, 

Proceedings of a Symposium in Pure Mathematics, volume V, pages 219-227, Providence, Rbode Island, 

1962. American Mathematical Society. 

C. Muiioz and M. Mayero. Real automation in the field. Technical Report NASA/CR-2001-211271 Interim 

ICASE Report No. 39, ICASE-NASA Langley, ICASE Mail Stop 132C, NASA Langley Research Center, 

Hampton VA 23681-2199, USA, December 2001. 

[MTHSO] R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. MIT Press, 1990. 

[NGdV94] R. P. Nederpelt, J. H. Geuvers, and R. C. de Vrijer. Selected Papers on Automath. North-Holland, 

[MMOl] 

[NO791 

[OS031 

[Pad41 

[Rud92] 

[Sho84] 

[SS94] 

[Tur63] 

[vBJ79] 

[vdB JO 11 

[VitOB] 

Amsterdam, 1994. 

G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures. ACM Transactions on 

Programming Languages and Systems, 1(2):245-257, 1979. 

S. Owre and N. Shankar. PVS API Reference. Computer Science Laboratory, SRI International, Menlo 

Park, CA, September 2003. 

L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. 

Springer-Verlag, 1994. 

Piotr Rudnicki. An overview of the MIZAR project. In Proceedings of the 1992 Workshop on Types for 

Proofs and Programs, pages 311-330, Bhtad, Sweden, June 1992. The complete proccedings are available 

at http: //m. cs. chalmers. se/pub/cs-reports/baastad.92/; this particular paper is also available 

separately at http://ueb.cs.ualberta.ca/”piotr/Mizar/MizaOvervieu.ps. 

Robert E. Shostak. Deciding combinations of theories. Journal of the ACM, 31(1):1-12, January 1984. 

Jens U. Skakkebzk and N. Shankar. Towards a Duration Calculus proof assistant in PVS. In H. Langmaack, W.-P. de Roever, and J. Vytopil, editors, Formal Techniques in Real-Time and Fault-Tolerant 

Systems, volume 863 of Lecture Notes in Computer Science, pages 660-679, Liibeck, Germany, September 

1994. Springer-Verlag. 

Alan Turing. Computing machinery and intelligence. In E. A. Feigenbaum and J. Feldman, editors, 

Computers and Thought. McGraw-Hill Book Company, New York, 1963. Originally published in Mind, 

Vol. LIX. No.236, October, 1950. 

L. S. van Benthem Jutting. Checking Landau’s ‘Grundlagen’ in the Automath system. Technical report, 

Mathematical Centre, Amsterdam, 1979. Mathematical Centre Tracts. 

Joachim van den Berg and Bart Jacobs. The LOOP compiler for Java and JML. In T. Margaria and 

W. Yi, editors, Tools and Algorithms for the Construction and Analysis of Systems: 7th International 

Conference, TACAS ,2001, volume 2031 of Lecture Notes in Computer Science, pages 299-312, Genova, 

Italy, April 2001. Springer-Verlag. 

Ben. L. Di Vito. A PVS prover strategy package for common manipulations. Technical Memorandum 

NASA/TM-2002-211647, NASA Langley Research Center, Hampton, Virginia, April 2002. 
Developing User Strategies in PVS: A Tutorial 

Myla Archer1, Ben Di Vito2, and Cksar Muiioz3* 

Naval Research Laboratory, Washington, DC 20375, USA 

NASA Langley Research Center, Hampton, VA 23681, USA 

National Institute of Aerospace, Hampton, VA 23666, USA 

archer@itd.nrl.navy.mil 

b.l.divitoQlarc.nasa.gov 

munozQnianet.org 

http://research.nianet.org/"munoz 

Abstract. This tutorial provides an overview of the PVS strategy language, and explains how to define 

new PVS strategies and load them into PVS, and how to create a strategy package. It then discusses 

several useful techniques that can be used in developing user strategies, and provides examples that 

illustrate many of these techniques. 

1 Introduction 

Why use strategies in PVS? There are several compelling reasons for doing so. We offer a few scenarios below 

that illustrate productive uses for strategies. 

PVS provides a core set of inference rules supplemented by decision procedures and other simplification 

heuristics. Continuing enhancements to the theorem prover gradually increase the automation available to 

interactive users. Nevertheless, the level of automation perceived by users is still much lower than desired. 

This is not a problem peculiar to PVS; similar provers suffer the same limitations. In fact, PVS is among 

the most automatic of provers in its class. 

Strategies provide an accessible means of increasing the automation available to users of the PVS prover. 

This can be done in generic form, suitable for a wide range of proving tasks, or in specific problem domains, 

yielding specialized tools suitable only in narrow contexts. Development of strategies can be performed by 

end users or specialists whose role is to create strategies for use by others. Over time, strategy development 

can lead to a reusable body of "deductive middleware." An effective division of labor in the overall conduct 

of mechanical theorem proving is a possible outcome of this process. 

In the following, we provide several examples of strategies that are likely to be beneficial to PVS users. 

- Modest strategies to streamline prover use. This is the simplest category of strategies, typically involving 

rules with just a few lines of definition. An example would be introducing rules to invoke frequently 

occurring sequences of proof commands. Consider the sequence (LIFT-IF), (SPLIT), and (ASSERT). 

One could introduce a strategy named IF-SPLIT to carry out this sequence. Such strategies are easy to 

create, although their benefit is limited to saving the effort of repetitive typing. 

- Extended forms of predefined rules. A slightly more advanced approach is to identify commonly needed 

inferences that are guided by user input. By writing strategies that accept arguments, it is possible 

to create enhanced versions or combinations of rules that already exist in the predefined set provided 

by PVS. In fact, many of the higher level predefined rules were created using the strategy mechanism. 

Consider, for example, a rule to claim that the lefthand sides of two formulae are equal, then invoke the 

appropriate CASE command. We might apply such a strategy using (CLAIM-EQ -1 -3) where CLAIM-EQ 

is the new proof rule and -1 and -3 axe the numbers of the sequent formulae to be considered. 

- Algebraic manipulation and arithmetic simplification. The PVS decision procedures handle linear arithmetic well, but have more difficulty with nonlinear expressions. In such cases, users must apply lemmas 

from the prelude or other sources. Strategies can be effective at manipulating arithmetic expressions 

when guided by user input. The package Manip [5], for instance, provides strategies for conducting userdirected manipulations of real-valued expressions. Similarly, the package Field [6] carries out higher level 

arithmetic reduction with considerable automation. 

* Funded under NASA Cooperative Agreement NCC-1-02043. 
Developing User Strategies in PVS: A Tutorial 17 

- Deduction support for specialized models or specifications. Verification or analysis tasks based on theorem 

proving often take place in the context of a specialized model of computation, such as state machines, 

hybrid automata, etc. Proofs in such contexts often have a stylized character that lends itself to automated 

proof. By capturing the proof steps and decision processes in the form of strategies, it is possible to provide 

a great deal of targeted automation to the proof effort. TAME is an example of such an approach within 

the domain of timed automata. 

- Interfaces to external proof support tools. Occasionally it is desirable to make use of additional tools that 

support the prover in the construction of large or difficult proofs. Strategies in this role can be used as a 

means of accessing the current proof state and exporting information to an external tool. After computing 

its result, the external tool can supply information to be acted on in some way, such as submitting prover 

commands. An example would be a tool that performs database searches, then returns the names of 

suitable lemmas for possible invocation. PVs’s musimp, model-check, and abstract-and-model-check 

strategies are also examples of this approach. 

- Interfaces to support external components through proving. The support relationship can work in the 

other direction as well. Under some arrangements, the prover can be used to provide support to an 

external process. For example, a computer algebra system might wish to consult a theorem prover to 

confirm that a transformation it needs to perform is valid under certain conditions. This request could 

be posed as a set of conjectures sent to the prover, where a strategy-guided proof process would attempt 

to settle the question and return a result. 

These suggested uses of PVS are by no means exhaustive. They are realistic, however. Each of these 

uses has either been implemented or is currently under development. No doubt other applications will be 

discovered. It is our hope that this tutorial might lead others to investigate new possibilities. 

The remainder of this tutorial is organized as follows. Section 2 provides the basic information needed 

for defining your own strategies and making them available in PVS. Section 3 describes and illustrates a 

set of techniques that can be used in the development of user strategies. Section 4 provides examples that 

demonstrate how to use various techniques to develop both strategies that facilitate user interaction with 

PVS and automatic strategies. Finally, Section 5 discusses some additional support that would be useful in 

to developers of PVS user strategies. 

2 The basics 

2.1 PVS commands. 

PVS commands can be either rules or strategies. A rule is a command that can be invoked by name and 

(if appropriate) applied to arguments. Rules execute as atomic steps in the PVS prover. A strategy is a 

command created by using zero or more PVS strategy-building commands to combine rule applications and 

other strategies. Thus, every rule application is also a (degenerate) strategy. Executing a strategy in the PVS 

prover causes execution of the sequence of atomic steps needed by the strategy for the current subgoal. On 

the syntactic level, the heart of a strategy definition is a strategy expression built by using strategy-building 

command names to combine rule names (applied to arguments, which may involve variable names) and other 

strategy expressions. 

A representative set of PVS strategy-building commands is listed in Table 1. For short, we will refer to 

these commands as strategicals, in analogy to the tacticals in Coq, HOL, and other theorem provers that are 

used to combine simpler tactics into more complex ones. 

A simple example strategy that is sometimes useful is: 

(THEN (LIFT-IF) (PROP) (ASSERT) (FAIL)) (1) 

Strategy (1) is useful in determining whether straightforward simplification combined with the PVS decision 

procedures will achieve a goal; if it does not, then the intended behavior of this strategy is to return to the 

proof subgoal in which it is invoked, without generating any new subgoals. Most simple sequential strategies 

do not use (FAIL); because it does so, Strategy (1) can behave badly. In particular, it causes full or partial 

proof failure if none of (LIFT-IF), (PROP), and (ASSERT) has an effect. One way to ensure the intended 
18 Myla Archer et al. 

(APPLY step) 

(THEN step1 . . . step,) 

(THEN@ step1 . . . step,) 

(IF lisp-espr step1 step21 

(TRY step1 step2 steps) 

(ELSE step1 stepz) 

(SPREAD step (step1 ... step,)) 

(BRANCH step (step1 . . . step,)) 

(REPEAT step) 

(REPEAT* step) 

(WITH-LABELS step (labs1 . . . labs,)) 

(LET ((vi lisp-esprl) . . . (w, lisp-espr,)) step) 

Turns step into a defined rule. 

Applies step1 to step, in order down all branches. 

Applies step1 to step, in order down the main proof branch. 

If lisp-ezpr evaluates to true then applies step1 . 

Otherwise, applies stepz. 

Tries stepl; if it modifies the proof state then applies stepz. 

Otherwise, applies steps. 

Behaves as (TRY step1 (SKIP) stepz). 

Applies step and spreads step1 to step, over the new subgoals. 

Like SPREAD but reuses step, on any extra subgoals. 

Iterates step until it does nothing down the main proof branch. 

Iterates step until it does nothing down all branches. 

Applies step; then labels all new formulae in the new subgoals with 

labs1 to labs,. 

Applies a new command that is just like step, but where 

vi has been replaced by the evaluation of lisp-ezpr, for 1 5 i 5 n. 

behavior of Strategy (1) is to use the strategy expression in (1) as the body of a defined rule, as described 

in Section 2.2. Another way is to “wrap” it with the command APPLY, as in: 

(APPLY (THEN (LIFT-IF) (PROP) (ASSERT) (FAIL))) (2) 

Finally, one may catch the action of FAIL with the command TRY. For more on both TRY and the use of 

wrappers, see Section 3. 

Note that the two strategicals IF and LET allow the introduction of Lisp code into a strategy. Strategies 

that incorporate Lisp code are more sophisticated than Strategies (1) and (2). The Lisp code generally uses 

information about the current proof state, though a few useful things can be done by using Lisp code to 

set and observe global variables. Strategies that use information about the proof state are discussed later in 

Section 3. 

2.2 Defined rules and strategies. 

PVS proof rules are of two kinds: primitive rules and defined rules. Both primitive and defined rules behave 

like atomic steps when applied to appropriate arguments, but, unlike a primitive rule, a defined rule is derived 

from a strategy expression. The strategy expression corresponding to a defined rule can be observed in PVS 

by typing: 

M-x help-pvs-prover-strategy 

Also, the documentation string for a strategy can be viewed within the prover via the command HELP. 

Guide [lo, 111, the format for def step is: 

A defined rule is created by applying the PVS macro defstep. Paraphrased from the PVS Prover 

(def step name 

param e ter- lis t 

strategy-expression 

documentation-string 

format-string ) 

(3) 

The parameter-list, whose precise description can be found in [lo, 111, can contain required arguments plus 

&optional and &rest parts, rather like the parameter list in a Lisp function definition. The documentationstring is generally used to describe the effect of applying the strategy; it is printed interactively as part 
Developing User Strategies in PVS: A Tutorial 19 

of the documentation of proof steps that is printed by the "help" facilities of PVS, e.g., when one types 

(HELP name) during a proof, or M-x help-pvs-prover or M-x help-pvs-prover-strategy followed by 

name at any time when using PVS. The format-string is printed interactively when the defined rule name 

succeeds, i.e., completes the proof of the current goal, or when it returns one or more subgoals. In addition 

to creating a new defined rule name, the macro defstep also creates a named strategy name$. Variants of 

def step include def helper, which does not require the documentation-string or format-string arguments, 

and defstrat, which does not require the format-string argument. The macro defhelper is intended for 

defining "internal" auxiliary steps that can be used in other strategies, while def strat defines a strategy 

without a corresponding (atomic) defined rule. 

Strategy (1) can be turned into the defined rule PROPPROBE using the definition: 

(defstep PROPPROBE (1 

(THEN (LIFT-IF) (PROP) (ASSERT) (FAIL)) (4) 

"Checks for a trivial proof (IBy simple reasoning") 

Once the definition of PROPPROBE has been loaded into PVS, the desired effect of Strategy (1) can be 

accomplished by just typing (PROPPROBE) when prompted by PVS for a proof rule. Because Strategy (1) does 

not refer to any unbound parameter names, the effect of (PROPPROBE) is equivalent to that of Strategy (1) 

wrapped in (APPLY . . .). The exact effect of Strategy (l), in which one sees all the steps in the reasoning, 

can be duplicated by typing (PROP_PROBE$) when prompted for a rule. 

By allowing the possibility of parameters, the macro def step allows a strategy (as well as its corresponding defined rule) to be applied in an environment where the parameter names are bound to specific values. 

The format-string in the definition of a rule with parameters can refer to these parameters: any inclusion 

of -a in the format string is replaced by the value of an actual parameter, with successive -a's picking up 

successive parameters. 

A simple example of a new rule with all these features is the rule suppose, whose definition is in Figure l.4 

The rule suppose incorporates formula labeling and comments into the simplest version of the PVS command 

(def step suppose (XI 

(nsuppstring 

(let ((suppstring (format nil "Suppose "a" XI) 

(format nil "Suppose not [-a] I' x> 1) 

(branch (with-labels (case x) (("Suppose") ("Suppose not"))) 

( (comment suppstring) (comment nsuppstring) 1) 1 

"For doing a simple case split and tracking the cases" 

"First supposing "a true and then supposing it false") 

Fig. 1. Definition of a rule with a parameter and a format-string that refers to it. 

CASE. The strategy expression body of suppose uses the strategicals LET, WITH-LABELS, and BRANCH. With 

LET, it incorporates Lisp code that computes two comment strings. Using WITH-LABELS, it applies the labels 

from the first list ("Supposen) to new formulae in the first new subgoal, and the labels from the second 

list ("Suppose not") to new formulae in the second new subgoal. Since each of the first and second new 

subgoals have just one new formula, and these new formulae represent, respectively, the meanings of x and 

(NOT x) , they are labeled appropriately. The second argument of BRANCH is a list of two commands, which 

will be applied respectively to the new subgoals. Each of these commands adds its argument as a comment in 

the subgoal to which it is applied; this comment will appear above the sequent when the subgoal is displayed. 

Each comment will also be recorded in the saved proof at the beginning of the new proof branch starting at 

its associated proof goal. The use of labels and comments will be discussed further in Section 3. 

Though we use a mixture of upper and lower case versions of names in this tutorial, it is safest to use only lower 

case in actual strategy files; see the PVS release notes at http://pvs.csl.sri.com. 
20 Myla Archer et al. 

2.3 

Once you have defined one or more new rules using def step, def strat, or defhelper, you can make your 

new rule(s) available in PVS by saving the definition(s) in a. file named pvs-strategies and putting it 

in the PVS context where you wish to use the new rules. The file pvs-strategies does not need to be a 

physical file, it can be a link to a file containing your definitions. This way, you can keep a set of definitions 

consistent across several contexts. 

The file pvs-strategies is loaded when the first proof in a session is being started, or when a new 

proof is being started after the content of pvs-strategies has been changed. Because pvs-strategies is 

loaded into Lisp, it can contain arbitrary Lisp code-not only rule definitions, but function definitions, global 

variable initializations, load commands, etc. One use of a load command (that is in fact employed by TAME) 

is to load a set of strategies specific to one context that can be generated from some theory in that context. 

Further, if commonstrat is a file containing a set of strategies that you use in all your developments, you 

can load those strategies by putting the line 

Adding new rules and strategies to PVS. 

(load <PATH>/commonstrat") 

in the file pvs-strategies, where <PATH> is the path where the file commonstrat is found. Section 3 

describes some possible uses of functions and global variables. 

For testing purposes, one can introduce strategy definitions directly from the command line: 

(LISP (DEFSTEP strat-name . . .)) 

To redefine one later, recall the previous command input using M-s or M-r, then edit the definition and 

resubmit it. This technique allows for quick tests or explorations of small strategies. 

2.4 Creating a strategy package. 

If a set of definitions is general enough to be used in several developments or to be used by other PVS 

users, you may want to pack them as a prelude library extension. The basic functionality of prelude library 

extensions has been available in older versions of PVS. However, it became fully operational and simple 

to use in PVS 3.1. A prelude library extension is a set of PVS theories, strategies, and Lisp code that are 

available to the user as if they were part of the PVS prelude context. As the developer of a prelude library 

extension, make a directory MyPackage and put the following files in it: 

- Files * .pvs containing PVS theories that your development requires. These theories become part of the 

- A file my-strat containing the new strategies. 

- A file pvs-lib. lisp containing 

PVS prelude theories; therefore, be careful not to introduce inconsistencies. 

(in-package :pvs) 

;; If your development requires other prelude libraries, then 

;; uncomment the following line and modify it as appropriate. 

;; (load-prelude-library "OtherPackage") 

( 1 i bload 'I my -s t ra t 'I ) 

- A file pvs-lib.el containing Emacs Lisp code that is part of your development. 

Once you have put all these files together, instruct the users of your prelude extension to 

Set the variable PVSLIBRARYSATH to point to <PATH>, where 

<PA TH>/MyPa c kag e 

is the actual location of your package. 

Invoke the Emacs command M-x load-prelude-library MyPackage the first time MyPackage is going 

to be used in a context. Next time that PVS is restarted in the same context, the prelude extension will 

be automatically reloaded in the environment. 
Developing User Strategies in PVS: A Tutorial 21 

3 Some useful techniques for strategy writing 

This section describes a set of techniques that can be used by a strategy developer to create sophisticated 

PVS strategies. These techniques include: 

1. Incorporating backtracking with TRY. 

2. Controlling standard PVS steps with appropriate arguments. 

3. Observing the proof state. 

4. Probing the CLOS structure of the proof state. 

5. Defining helper functions in Lisp. 

6. Carefully using global variables. 

7. Computing a command in Lisp, and then invoking it. 

8. Using auxiliary lemmas for rewriting and forward chaining. 

9. Using labels and comments. 

10. Using functions from PVS. 

11. Applying wrappers. 

12. Naming subexpressions of complex expressions. 

13. Using templates. 

14. Comparing proof step definitions using PVS's multiple proof feature. 

The TAME [l] strategies and the strategy packages Manip [5] and Field [6] all employ many or all of these 

techniques. Below, we illustrate how each individual technique can be used to advantage. 

3.1 Using TRY for backtracking. 

Backtracking is a powerful technique for automatic proof search. It enables the restoring of an original proof 

state after an unsuccessful proof attempt. In PVS, backtracking is achieved by a careful crafting of TRY, 

FAIL, and atomic proof rules. 

The TRY command in PVS combines a conditional and a backtracking control structure. As a conditional 

control structure, TRY performs an action based on the progress made by a proof command on the current 

proof state. For instance, the strategy expression 

(TRY (THEN (LIFT-IF) (PROP) (ASSERT)) 

(COMMENT "Progressing . . . 'I) 

(SKIP)) 

applies the proof command (THEN (LIFT-IF) (PROP) (ASSERT)). If it does something, i.e., it modifies 

the current proof state, the comment "Progressing . . . 'I is added to the new proof state. Otherwise, the 

strategy expression performs the proof command (SKIP) and does nothing else. 

On the other hand, the third argument of TRY is a backtracking alternative to failures signaled in its first 

argument. Failures in TRY'S second and third arguments are propagated out of the command. The following 

semantics, based on an informal set of rules provided by N. Shankar, exposes some technicalities of the 

behavior of TRY. 

We assume that any proof command evaluates to one of the following states: 

- skip: If the proof states remains unchanged. 

- failure: If a failure is signaled. 

- success: If the current goal is discharged. 

- subgoals: If new subgoals are generated. 

- backtracking: If backtracking is required. 

The evaluation of SKIP, FAIL, and TRY is given by the function 1.1 as follows 

- I (SKIP) I = skip. 

- I (FAIL) I = failure. 
22 Myla Archer et al. 

if [AI E {skip, backtracking} 

if (AI E {failure, success} 

if IAl = subgoals, IBI E {skip, subgoals} 

- I(TRY A B C)l = backtracking if IAl = subgoals, IBI E {failure, backtracking} r subgoals 

success if IAl = subgoals, IBI = success 

To complete the description of TRY’S behavior, it is necessary to consider that 

- The states failure and backtracking do not propagate out of atomic proof rules, i.e., if the strategy 

- At the top-level, the state failure forces the theorem prover to exit, while the state backtracking evaluates 

expression of the atomic proof rule S evaluates to either failure or backtracking, then 1st = skip. 

to skip. 

For instance, 

- I (TRY (SKIP) (ASSERT) (FAIL)) I = failure. 

- 1 (TRY (TRY (FAIL) A B) C D) I = failure. 

- I(TRY (TRY A (FAIL) B) C D)I = ID[, if IAl = subgoals. 

- I(TRY A (TRY B (FAIL) C) D)I = backtracking, if IAl = IBI = subgoals. 

The strategy expression 

(TRY (TRY (THEN (LIFT-IF) (PROP) (ASSERT)) (FAIL) (SKIP)) 

s t epl 

step21 

applies the proof command (THEN (LIFT-IF) (PROP) (ASSERT)). If that command discharges the current 

goal, then it does nothing else. Otherwise, it backtracks to the original proof state and attempts a new proof 

with the command step2. Since FAIL does not propagate out of atomic proof rules, Le., it evaluates to skip, 

the logical behavior of the above strategy expression is equivalent to that of the strategy expression (APPLY 

(THEN (LIFT-IF) (PROP) (ASSERT) (FAIL))) when step2 = (SKIP). 

The TRY command is not symmetric: failures signaled in its second argument is not handled in the same 

way as failures signaled in its third argument. This makes the analysis of failure propagation difficult and 

error prone. In particular, some PVS commands, such as THEN, ELSE, REPEAT, SPREAD, etc., are implemented 

with TRY, and their behavior with respect to failure propagation and backtracking is not easy to characterize. 

For instance, [(THEN step1 . . . step, (FAIL))I is 

- failure, if n = 0 or IstepiI = skip for 1 5 i 5 n. 

- backtracking, otherwise. 

In general, it is a good practice to wrap as atomic proof rules the strategy expressions that can generate 

failures. 

For the interested reader, the experimental package Practicals, available at http://research.nianet.org/fmat-nia/Practicals, provides a redesigned set of strategicals for catching and signaling failures, as well as 

additional control structures for programming PVS strategies. 

3.2 Controlling standard PVS steps. 

When one needs finer control in a strategy, one sometimes needs to use variants of the standard PVS steps 

that do either less or more than the default actions of these steps. For example, the PVS command 

(EXPAND name) 

does not simply expand the definition of name, but performs some simplifications as well. This can be 

inconvenient; e.g., since one of these simplifications can be a (LIFT-IF), it is possible for a quantified 

formula involving an IF-THEN-ELSE to become an IF-THEN-ELSE with two quantified formulae as branches, 
Developing User Strategies in PVS: A Tutorial 23 

complicating a strategy involving skolemization or instantiation. To obtain the effect of simply expanding 

the definition of name, one should instead use the PVS command 

(EXPAND name :ASSERT? NONE). 

Other example PVS steps that can be made to do less for finer control are SPLIT and FLATTEN. Using 

the optional : depth argument, SPLIT can be prevented from producing more subgoals than one desires. One 

application of this technique is in the definition of the simple strategy modus-ponens: 

(defstep modus-ponens (formnum) 

(spread (split formnum :depth 1) ((skip)(skip))) 

"Replaces antecedent formulae A and A => B by A and B uhen 

"Performing Modus Ponens") 

the formula A => B is labeled by formnum" 

Note that while the PVS rule ASSERT can sometimes be used to discharge the hypothesis of an implication, 

ASSERT may cause further changes, and it does not discharge a hypothesis that is not a simple expression. 

The rule modus-ponens permits one to discharge the hypothesis of an implication, without doing more (or 

less). 

Because controlling the number of subgoals in a strategy can be important, being able to apply fine 

control to SPLIT is useful. However, one can also apply fine control to FLATTEN as well. This is done by 

replacing it with FLATTEN-DISJUNCT with an appropriate :depth argument. 

One case in which the default action of a PVS step may be too limited is in a context where there 

is extensive use of CASES expressions. The default of ASSERT and SIMPLIFY is to not simplify inside these 

expressions. This choice often results in more efficient proofs, but experience has shown this may not be true 

when proofs involve large, complex, and possibly many-layered CASES expressions. In such a case, one may 

wish to use (ASSERT : CASES-REWRITE? T) and (SIMPLIFY : CASES-REWRITE? T) instead. 

3.3 Observing the proof state. 

The PVS proof state and related data structures are represented as classes in the Common Lisp Object 

System (CLOS). In particular, during the execution of any proof in PVS: 

- The current proof state is in the global variable *ps*. 

- The current proof goal is in the global variable *goal*. It can be also accessed as (current-goal *ps*). 

- The list of current sequent formulae, each one an instances of the CLOS class s-f ormula, can be accessed 

as (s-forms (current-goal *ps*)). 

A more comprehensive list of PVS global variables and data structures and the information they contain 

can be found in [lo, 111. 

The proof state (and in fact the value of any Lisp expression) can be observed during a proof using the 

proof command LISP. Thus, to observe the sequent formulae of the current goal at some point in the proof, 

one can issue 

(LISP (s-forms (current-goal *ps*)>) (5) 

at the top-level. When making extensive observations about the proof state, it can become inconvenient to 

have to embed all the Lisp expressions to be evaluated in a LISP command. Another inconvenience of this 

command is that it interleaves the desired information with repetitions of the current proof goal, making it 

difficult to make a coherent sequence of observations. (This applies only to PVS versions earlier than 3.1.) 

An alternative is to send Lisp into a break; this can be done by typing (LISP (BREAK)). 

Each s-f ormula in (s-f orms (current-goal *ps*) ) corresponds to one of the labeled formulae in the 

sequent of the current goal. An example of how a list of sequent formulae appears when displayed is: 

(NOT A B C NOT D E) (6) 
24 Myla Archer et al. 

where A, B, C, D, and E represent particular PVS formulae. The actual members of the list (6) print out as 

NOT A, B, C, NOT D, E. The list (6) represents the sequent: 

(or a variant in which some square brackets are replace by curly braces). In particular, the negative formulae, 

in order, correspond to the sequent formulae numbered -1, -2, and so on, while the positive formulae, in 

order, correspond to the sequent formulae numbered 1, 2, and so on. In general, the list of antecedent 

(negative) formulae and consequent (positive) formulae can be extracted from the proof state as (n-sf orms 

(current-goal *ps*) ) and (p-sf orms (current-goal *ps*)), respectively. 

Note that formulae in the antecedent, such as A and D in the sequent (7), appear negated in the representation of the PVS proof state. The following Lisp code retrieves a formula in positive form, i.e., as it appears 

to the user in the PVS theorem prover, from the formula n~mber:~ 

; Get formula from current goal (unnegated if antecedent formula) 

; Assumes that fnum is a formula number 

(defun get-fnum (fnum) 

(let ((index (- (abs fnum) I)> 

(goal (current-goal *ps*))) 

(formula (nth index (p-sforms goal))) 

(argument (formula (nth index (n-sf orms goal) ) ) ) ) ) ) 

(if (> fnum 0) 

To determine that one needs argument and formula to extract the desired part of an s-f ormula in (p-sf orms 

goal) and (n-sf orms goal), one can use technique 4 described in Section 3.4. 

The inverse of the operation get-fnum is to find the formula number or numbers corresponding to 

formulae with a given property. The PVS Lisp function (gather-fnums s-forms yes-fnwns no-fnwns 

pred), described in [lo, 111, returns the list of formula numbers (taken from yes-fnumslno-fnums) of sequent 

formulae in s-forms that satisfy pred. For example, given the property 

(defun is-fora11 (sform) (forall-expr? (formula sform))) 

the Lisp code: 

retrieves all the formula numbers in the current sequent that are universally quantified. 

(gather-fnums (s-form *goals*) '* nil #'is-forall) 

3.4 Using CLOS probes. 

Most values manipulated by PVS proof steps are CLOS objects. For instance, *ps* is a CLOS object which 

has a component current-goal; in turn, (current-goal *ps*) is a CLOS object which has a component 

(s-f orms (current-goal *ps*)). To probe the CLOS structure of an object and its components, one can 

use the Lisp functions describe or show. Given an object object, one can probe its CLOS representation in 

depth by repeatedly using describe to discover components to be probed further: 

(describe object) 

(describe (component object) 

(describe (component (component object) ) ) 

... 

More involved versions of this function that take care of special symbols, labels, and error handling are available in the Manip (http://shemesh.larc.nasa.gov/people/bld/manip.html) and Field 

(http://research.nimet.org/-munoz/Field) packages. 
Developing User Strategies in PVS: A Tutorial 25 

The function describe provides explicit names of the component slots in the representations of objects, 

and these names can then be used like function names to retrieve the elements in these slots, which are 

themselves objects. The description of object starts with a sentence of the form: 

object is an instance of #<STANDARD-CLASS object-class> 

This information generally tells you that object-class? is a recognizer for objects of class object-class. An 

element x of class object-class can also be recognized by the fact that (typep x object-class) will be true. 

When one needs a shortcut to a sequence of CLOS probes, or when one cannot be sure of the sequence 

or sequences needed, one can use the function mapobject. The function mapobject provides an analog for 

objects of mapcar for lists: it traverses (most of) the object structure, applying a given function to each 

component. Thus, to determine whether an s-formula sf orm contains a universal or existential quantifier, 

one can use the predicate has-quantif ier, defined as: 

(def un has-quant if ier (sf orm) 

(let ((has-quant nil)) 

(mapobject #'(lambda (x) (if has-quant t 

(when (or (forall-expr? x) 

(exists-expr? x)) 

(setq has-quant t) t))) 

sf orm) 

has-quant)) 

3.5 Defining helper functions. 

Helper functions from Lisp are useful for writing strategy expressions that involve Lisp code, i.e., those using 

either LET or IF. They generally involve CLOS probes into the current proof state; thus, we have already 

seen the following examples of potential helper functions in Sections 3.3 and 3.4: 

- get-fnum 

- is-forall 

- has-quant if ier 

The helper function get-fnum is used in a LET in the strategy add-eq in Figure 12 below in Section 4.1. 

Examples of definition and use of additional helper functions can be found below in Section 4.2. 

One can classify Lisp helper functions into general purpose and special purpose functions. General purpose helper functions include functions such as get-fnum and is-forall, which can be applied, respectively, to any valid formula number (or label) and to any valid s-formula. An example of a special purpose 

helper function is the function getsk-constructor-exprs from Figure 18 in Section 4.2. The function 

get-sk-constructor-exprs will cause a Lisp break if it is called incorrectly; it must be called only on sformulae of a very limited form. Special purpose helper functions generally use CLOS probes that are either 

unusual or grouped in a long series, making them hard to match. Thus, extra care must be taken when these 

functions are used: they should either be used in a context where they are known to be valid (as in the 

example in Section 4.2, or else a strategy should test the classes of a CLOS structure and its substructures 

before applying them. 

Alternatively, helper functions can take advantage of Common Lisp's exception handling features to deal 

with errors. While the language specification 1121 explains these features in full detail, the following idiom 

based on the handler-case macro is sufficient for most applications: 

(handler-case 

<expression> 

(error (condition) <alt value/action>)) 

If the evaluation of <expression> proceeds normally, its value is returned as the value of the handler-case 

construct. If the evaluation of <expression> raises any type of Lisp error, it will be caught and the <alt 

value/act ion> will be returned/performed. 
26 Myla Archer et al 

3.6 Using global variables. 

As in any type of programming, global variables must be used carefully in PVS. Clearly, two rules should 

be followed: 

1. Choose variable names not already in use; 

2. Never change a predefined PVS global variable, such as *ps* or *goal*. 

Towards satisfying rule 1, one can easily test whether a variable x is currently in use: either type the command 

(LISP x) when the prover is running, or else type x into the *pvs* buffer when the prover is not running. 

For run-time use, the Lisp functions boundp and fboundp are available to test whether a symbol is currently 

bound as a variable or a function. Note that if one violates rule 2 by changing *ps*, even if the new value 

of *ps* is a valid proof state object, one is creating a nonconservative extension of PVS, and losing PVS’s 

soundness guarantees. 

In general, global variables should be avoided. However, they can be useful as switches. In TAME, for 

example, the user can control whether saved proofs will be in verbose form (recording specific facts introduced 

in the proofs), or in bare-bones, nonverbose form, by invoking the rules (VERBOSE) and (NONVERBOSE) . These 

rules work simply by setting a specific global variable to t or nil. 

3.7 

When a strategy definition has parameters, it can happen that the proof step the strategy is to implement 

depends on some information that must be computed from the parameter values. 

A typical example is when the strategy definition has an &rest parameter. When the strategy (or corresponding defined rule) is applied, the &rest parameter is bound to a list of actual parameters. The strategy 

will typically need to extract the car and cdr of this list as it proceeds. Because proof rules cannot be 

applied directly to car or cdr expressions, commands involving the application of proof rules to the car or 

cdr of a list of actual parameters must be first computed and then called. Examples where this technique is 

used are in the definitions of the strategies apply-lemma, else*, and rewrite-one in Figures 7, 8, and 9, 

respectively, in Section 4.1. (Note that apply-lemma computes two commands, lemma-step and inst-step, 

though actually, only inst-step, which depends on the &rest parameter, needs to be computed.) 

Another example in Section 4.1 in which commands are computed is in the strategy add-eq in Figure 12. 

Here, two commands case-step and steplist are computed. Because case-step applies CASE to values 

computed from its formula-number arguments, it must be computed. Here again, one of the steps, steplist, 

need not be computed. However, note that “unnecessary” computation of a step often adds to the readability 

of a strategy definition, particularly when companion steps must be computed. 

3.8 

PVS provides a variety of steps for controlling the use of rewrites. An example of a strategy that takes 

advantage of PVS’s REWRITE rule is rewrite-one in Figure 9 on page 33. The strategy rewrite-one does 

rewriting once using its lemma arguments as the rewrite rules. 

For automatic or “large step” strategies, it is useful to do auto-rewriting. Auto-rewriting on a set of 

lemmas can be initiated by calling AUTO-REWRITE on a list of the lemmas. Similarly, auto-rewriting on a set 

of lemmas can be terminated by calling STOP-REWRITE on a list of the lemmas. Rather than explicitly listing 

lemmas, it can be convenient to collect a set of rewrites into a theory, and calling AUTO-REWRITE-THEORY 

(and STOP-REWRITE-THEORY) on that theory. Any lemmas installed as auto-rewrites will be used as rewrites 

whenever DO-REWRITE is called. Since ASSERT and SIMPLIFY call DO-REWRITE, these two PVS strategies 

also cause auto-rewrites to be performed. Auto-rewrites must clearly be used carefully, to avoid possible 

nontermination of rewriting. 

Rewrites in PVS can be conditional rewrites, where a rewrite rule is applied only if its condition simplifies 

to TRUE. Lemmas with conditions (i.e., hypotheses) can also be used for forward chaining, in which the 

(possibly parameterized) hypothesis is matched to some formula or formulae in the current sequent. Any 

match defines an instance of the conclusion, that is then added as an antecedent formula to the current 

sequent. The PVS rule FORWARD-CHAIN allows forward chaining on a lemma (or on a formula in the current 

sequent). Note that using REPEAT or REPEAT* in combination with FORWARD-CHAIN can lead to nontermination 

Computing the command to be invoked. 

Rewriting and forward chaining with lemmas. 
Developing User Strategies in PVS: A Tutorial 27 

if the conclusion of the lemma used for forward chaining matches its hypothesis; therefore, care must also 

be taken in using repeated forward chaining. There is currently no FORWARD-CHAIN-THEORY, although one is 

expected to be available in the near future [9]. 

There are many uses for rewriting and forward chaining; for example, TAME uses both auto-rewriting 

and forward chaining to automate certain reasoning about the relationships between constructor and accessor 

functions in DATATYPES that is not handled by ASSERT or GRIND. 

3.9 Using labels and comments. 

A simple use of comments and labels in a strategy has already been illustrated in Figure 1, which shows the 

definition of the strategy suppose. This strategy uses WITH-LABELS to introduce a set of labels simultaneously, 

and the command COMMENT is for introducing comments. There is also a command LABEL for introducing a 

single label. 

Labels are applied to formulae. Once a formula has a label, it can be referred to by that label. This fact 

has many uses in strategies. For example, a labeled formula can be hidden and revealed by calling HIDE 

and REVEAL on its label. One use of this device is to prevent expansion of definitions in the labeled formula 

except when such expansion is desired. Another example use for labels is to coordinate skolemization of one 

quantified formula with instantiation of another. It is possible to give a formula multiple labels by using 

the optional argument :push? T with either WITH-LABELS or LABEL. This allows all information in original 

labels to be retained, while adding new information, so that formulae can, if desired, be included in multiple 

categories for multiple purposes. The use of labels can also increase the stability of strategies. For simplicity, 

several example strategies in this tutorial use explicit references to formula numbers (see Sections 3.10 and 4). 

However, provided one knows the number, ordering, and nature of the new formulae that will be created by 

a command, by wrapping that command using WITH-LABELS and an appropriate list of labels, one can avoid 

explicit formula number references. On the assumption that the ordering in the set of newly created formula 

is less likely to change in new PVS versions than the explicit formula numbers that will be assigned to the 

new formulae, user strategies using WITH-LABELS and label references will be less fragile than those using 

explicit formula number references. An example of how labels appear in a sequent is shown in Figure 2, 

which shows a subgoal from a TAME proof for the invariant lemma lemma5 of TIP [4,3]. 

{-i,(pre-state-reachable)) 

{-2,(inductive-hypothesis)) 

{-3, (general-precondition) 1 

{-4,(specifi~-precondition)> 

I-5, (post-state-reachable)) 

reachable (prestate) 

length(mq(basic (prestate) 1 (e-theorem) 1 <= 1 

enabled-general(add-child(addE-action), prestate) 

enabled-spec if ic (add- child ( addE- ac t i on) , pre st at e) 

reachable (post st ate) 

{l,(inductive-conclusion)) 

I ------- 

IF NOT (mq(basic(prestate)) (ads-action) = null) 

THEN length(mq(basic(prestate)) WITH 

[(ads-action) := 

(e-theorem) 1 

cdr(mq(basic (prestate)) (ad&-action) 11 

ELSE length(mq(basic (prestate) (e-theorem) 

ENDIF 

<= 1 

Fig. 2. An example TAME sequent illustrating labels. 
28 Myla Archer et al. 

In contrast to labels, which attach to formulae, comments attach to subgoals. Note that subgoal in 

Figure 2 also contains a comment which identifies the case to which the subgoal corresponds. Comments also 

appear in saved proofs, immediately after the command that introduces them. When a command creates 

branches, it is possible to "label" the branches in the saved proof with comments by wrapping the command 

creating the branches in a SPREAD or BRANCH construct that then applies multiple calls to COMMENT to the 

branches, as illustrated in Figure 1 on page 19. An example saved proof showing how comments can be 

used to make saved proofs more understandable is shown in Figure 3, which shows the saved TAME proof 

of the the TIP property lemma-5. The subgoal in Figure 2 is the first subgoal of the first branch of the 

proof in Figure 3, so the comment in this subgoal "labels" the first branch of the proof. The saved proof in 

Figure 3 illustrates the effect of suppose, and also shows that comments can be used to capture ephemeral 

information from proof goals, such as facts being used in the reasoning. 

Inv-S(s:states) : boo1 = (FORALL (e:Edges): length(mq(e,s)) <= 1); 

... ,,,

(11 11 

Proof lema-5-like-hand for formula tip-invariants.lemma-5 

(AUTO-INDUCT) 

(("1" ; ;Case add-child(addE-action) 

( APPLY-SPECIFIC-PRECOND) 

;;Applying the precondition 

; ; init (target (addE-action) , prestate) 

;; & NOT (mq(addE-action. prestate)=null) 

(SUPPOSE "e-theorem = addE-action") 

( (til't ; ;Suppose e-theorem = addE-action 

(11211 ; ;Suppose not [e-theorem = addE-action] 

(TRY-SIMP)) 

(TRY-SIMP) 1) 1 

(11211 ; ; Case children-known (childV-action) 

(SUPPOSE "source (e-theorem) = childV-action") 

( (ftlgf ; ;Suppose source (e-theorem) = childV-action 

(APPLY -SPECIFIC-PRECOND) 

;;Applying the precondition 

;;init(childV-action, prestate) 

;; 8 

;; (FORALL (e: Edges): 

.. t, FORALL (f : tov(chi1dV-action) 1 : 

*, .. child(e, prestate) OR child(f, prestate) OR e = f) 

(APPLY-INV-LEMMA "2" "e-theorem") 

;;Applying the lemma 

; ; (FORALL (e: Edges) : init(source(e), prestate) 

;; => mq(e, prestate)=null) 

(TRY-SIMP)) 

(TRY-SIMP) 1) 1 

(1t291 ; ;Suppose not [source(e-theorem) = childV-action] 

("3" ; ;Case ack(ackE-action) 

(SUPPOSE "e-theorem = ackE-action") 

( (*tlft ; ;Suppose e-theorem = ackE-action 

(APPLY-SPECIFIC-PRECOND) 

;;Applying the precondition 

; ;NOT (init (target (ackE-action) , prestate)) 

;; & NOT (mq(ackE-action, prestate) = null) 

(TRY-SIMP)) 

(TRY-SIMP) 1) 1) 1 

(1t211 ; ;Suppose not [e-theorem = ackE-action] 

Fig. 3. A verbose TAME proof illustrating comments in a saved proof. 
Developing User Strategies in PVS: A Tutorial 29 

3.10 

As illustrated in Section 3, one can use PVS Lisp functions documented in [lo, 111 in writing Lisp code to 

be used in strategies.6 These documented functions can be a convenience in writing Lisp code, but one 

can generally achieve the same effects in one's Lisp code by combining standard Lisp constructs with CLOS 

probes. For example, the effect of the code in 8 on page 24, which solves the problem of listing all formula 

numbers in a goal corresponding to quantified formulae, can also be achieved by the code 

Using Lisp functions from PVS. 

(gather-fnums-property 'is-forall (current-goal *ps*)) (9) 

where gather-fnums-property is defined by: 

(defun gather-fnums-property (prop goal) 

(let ( (negf nums 

(let ((fnum 0)) 

(loop for x in (n-sforms goal) do (setq fnum (- fnum 1)) 

when (funcall prop x) collect fnum))) 

(posf nums 

(let ((fnum 0)) 

(loop for x in (p-sforms goal) do (setq fnum (+ fnum 1)) 

when (funcall prop x) collect fnum)))) 

(append negfnums posfnums))) 

However, there are PVS Lisp functions that are not formally documented that allow one to solve problems 

in ways not so easily duplicated. 

Consider the following problem. PVS expressions that are parameters to proof commands are input as 

strings. In general, these expressions are built from other expressions in the proof state, where they appear 

as CLOS structures, and converted to strings with the Lisp function format. In some special cases, we 

may want to perform the inverse operation, i.e., to get a CLOS structure from the string representation of 

a PVS expression. A simple way to achieve this operation is to bring the PVS expression to the proof state, 

for example using a harmless (CASE "expr = exprll), and then observing the CLOS structure of the proof 

state as explained in Sections 3.3 and 3.4. The following piece of code implements this technique 

(LET ((casestr (format nil "(-A) = ("A)" expr expr))) 

(THEN 

(CASE casestr) 

(LET ((closexpr (argsl (get-fnum -1)))) 

(THEN 

(DELETE -1) 

(. . . closexpr . . .)>)>) 

;; closexpr is the CLOS representation of expr 

The code above (which makes use of the documented PVS Lisp function argsl) has the side effect of 

temporarily modifying the proof state. In most cases, the modification has no logical consequences. However, 

if expr generates TCCs, these TCCs will appear in the new proof state. 

An alternative, cleaner way to get a CLOS structure of a PVS expression is by using the PVS parser and 

type-checker functions pc-parse and pc-typecheck directly. These functions are not properly documented 

and they must be used with care; otherwise, the PVS prover could get into an unstable state. The function (pc-parse expr gramtyp) returns a non-type-checked CLOS structure of the expression expcpr. The 

parameter gromtyp is a grammar nonterminal, in most cases with the same name as the CLOS type of the 

structure to be parsed. For instance, 

(pc-parse If(# x:=l, b:=true #)'I 'expr) 

An API document that covers all the Lisp calls needed for strategies and integration with other tools is being 

written at SRI [7]. 
30 Myla Archer et al. 

returns the CLOS structure corresponding to the PVS record (# x:=l, b:= true #I. On the other hand, 

(pc-parse 'I [# x : int , b : bool #I 'I ' type-expr) 

returns the CLOS structure corresponding to the PVS type record C# x: int , b : bool #I. CLOS structures 

should not be used in a proof state unless they are appropriately type-checked. The function (pc-typecheck 

closexpr) adds PVS type information to the CLOS structure closexpr. Usually, a call to pc-parse is 

followed by a call to pc-typecheck. 

An example where converting a string to a CLOS structure in this fashion is useful is in defining a 

strategy whose behavior depends on the type of one or more of its arguments. Provided the string x names 

a valid expression that is type correct in the current proof goal, the value of 

(type (pc-typecheck (pc-parse x 'expr))) (10) 

will be the (CLOS representation of the) type of that expression. (Note that type is a CLOS probe-i.e., 

the name of a slot or method-rather than a function from PVS.) The string 

(princ-to-string (type (pc-typecheck (pc-parse x 'expr)))) 

can then be compared to any specific type name represented as a string, or, more safely, the (not yet 

documented) PVS Lisp function tc-eq can be used to compare the type (10) with another (analogously 

computed) type. 

3.11 Applying wrappers. 

Wrappers are strategicals that prevent their strategy arguments from causing unintended effects. We have 

already seen one example use for wrapping: wrapping a command that may lead to failure in (APPLY . . . ) 

so that any failure caused will be local (undoing the proof only to the subgoal where the command was 

applied). 

Another instance in which one may wish to use a wrapper is when a strategy has potential side effects, 

for example through the use of auto-rewrites or global variables, and one wishes to be sure no permanent 

side effects result from execution of the strategy. Even a strategy that ultimately follows every auto-rewrite 

command with an appropriate corresponding stop-rewrite command can leave "dangling rewrites" active if 

it produces multiple branches and proves the last branch before it reaches a needed stop-rewrite command. 

In such a case one can wrap the strategy, together with a "cleanup step" that removes any potential side 

effects, in the strategical unwind-protect defined in Figure 4. To protect against auto-rewrites remaining 

(defstep unvind-protect (main-step cleanup-step) 

((then (delete -1) main-step) 

(spread (case "id(true)") 

(then cleanup-step (expand 'id" 1)))) 

"Invoke MAIN-STEP folloued by CLEANUP-STEP, vhich is performed 

"Invoking proof step with cleanup") 

even if MAIN-STEP leads to a proof of the current goal." 

Fig. 4. An example "safety wrapper" strategical. 

unintentionally active, the cleanup-step argument to unwind-protect can be a strategy that performs the 

needed sequence of stop-rewrite commands. 

3.12 Naming a subexpression. 

Field axioms, such as associativity, commutativity, distributivity, etc., are known to the PVS decisions 

procedures. For instance, the sequent 
Developing User Strategies in PVS: A Tutorial 31 

I - - - - - - - 

(1) x * x >= 0 

is automatically discharged by the proof command (GRIND). Surprisingly, the sequent 

1 ---- - -- 

(1) (x - 1) * (x - 1) >= 0 

is not discharged by (GRIND). In this case, GRIND yields the sequent: 

I - -- - -- - 

(1) 1-x+ (x*x-x) >=o 

which is not further simplified by the PVS decision procedures. 

The reason for this behavior is that the decision procedures always apply fields axioms, and in particular the distributive law, before other simplifications. Since PVS does not provide an explicit mechanism 

to customize these simplifications, they can be problematic for writing strategies where proof control is 

fundamental. 

One way to avoid certain implicit simplifications, such as the distributive law, is to wrap a subexpression 

in an application of the identity function, e.g., id(x - 1). This renders the expression ineligible for the 

distributive law. When this protection is no longer desired, the id function can be expanded to restore the 

original expression. For simple cases this technique is often adequate. 

For more advanced uses, undesired simplification can be avoided by naming the expression that should not 

be simplified. This can be achieved with the commands NAME and REPLACE, or the command NAME-REPLACE. 

The commands NAME introduce a new name definition to the current sequent. This name is then used by 

REPLACE to abbreviate the original expression. 

Figure 5 illustrates a strategy that blocks the first application of the distributive law in a formula by introducing a new name. The strategy NODISTR uses helper functions get-fnum, get-newname, get-distr-expr, 

and get-distr-plus. The function get-fnum (see Section 3.3) gets the formula in the formula number 

fnum. New names are created by the function get-newname, which increments the global variable newname 

each time a new name is required. Finally, the functions get-distr-expr and get-distr-plus descend the 

formula tree to find the first expression having the form (z + y) * z or z * (z + y). These functions use PVS 

functions inf ix-application? that checks if a formula is an infix application, name-expr? that checks if 

an operator is a name (as opposed to a lambda expression), and argsi and args2 that projects the first and 

second argument of an application, respectively. 

For instance, (NODISTR 1) applied to the sequent 

I - --- -- - 

(1) (x - 1) * (x - 1) >= 0 

(-1) 

(1) 

yields the sequent? 

(x - 1) = v7-- 

v7-- * v7-- >= 0 

I -- - --- - 

When strategies introduce new names automatically, there is the possibility of conflicts with user supplied names. To prevent such clashes, we recommend following a naming convention that yields distinctive 

identifiers. For example, the convention followed by the function get-newname is to create identifiers with 

two trailing underscore characters. 

The strategy NODISTR can be used to improve the automation provided by GRIND on the field of real 

numbers. For example, the simple strategy GRINOD in Figure 6 discharges, among others, the following 

sequent 

(1) 

’ The name of the new variable may be different. 

FORALL (x: real): (x - 1) * (x - 2) * (x - 1) * (x - 2) >= 0 
32 Myla Archer et al. 

;; Strategy definition 

(def strat NODISTR (f num) 

(LET ((form (get-fnum fnum)) 

(name (get-neuname) ) 

(expr (get-distr-expr form)) 

(str (when expr (format nil "-At' expr)))) 

(IF str (NAME-REPLACE name str :hide? nil) (SKIP))) 

"Introduces a new name in -A to block the distributive law") 

;; Generating new names 

(setq newname 0) 

(defun get-newname 0 

(progn (setq newname (+ 1 newname)) 

(format nil "v-A--" newname) ) ) 

;; Helper functions 

(defun get-distr-expr (form) 

(when (and (inf ix-application? form) 

(let ((op (id (operator form)))) 

(name-expr? (operator form) ) ) 

(cond ((member op ' (= <= >= < > + - /)) 

(or (get-distr-expr (argsl form)) 

(get-distr-expr (args2 form)))) 

((eq op '*) 

(or (get-distr-plus (argsl form)) 

(get-distr-plus (args2 form)))) 

(t nil))))) 

(defun get-distr-plus (form) 

(when (and (infix-application? form) 

(let ((op (id (operator form)))) 

(name-expr? (operator form))) 

(cond ((member op '(+ -1) form) 

((member op '(* /)) 

(or (get-distr-expr (argsl form)) 

(get-distr-expr (args2 form)))) 

(t nil))))) 

Fig. 5. Naming a subexpression to block the distributive law 

(defstrat CRINOD (fnum) 

(THEN (SKOSIMP fnum) 

(REPEAT (NODISTR fnum)) 

(GRIND :theories "real-props") 

"Blocks the distributive law in 'A before applying GRIND") 

Fig. 6. Combining NODISTR and GRIND 
Developing User Strategies in PVS: A Tutorial 33 

3.13 Using templates. 

The use of templates is an indirect technique that can be used in strategy development. For example, when 

one is reasoning in a special domain, one may wish to assume some degree of uniformity either in the objects 

about which one is reasoning or in the formulations of properties of these objects (or both). Templates allow 

one to enforce a standard naming scheme for objects and their types or a standard scheme for expressing 

properties. As a result, strategies based on templates can be based on a certain amount of definite information 

that allows them to make more reasoning automatic, and thus to achieve larger size proof steps. 

Templates for both specifications and lemmas are used to advantage by TAME. 

3.14 

For proof steps that do a significant amount of automatic reasoning, and which therefore can take a long 

time to execute, efficiency is an important design goal. Once one has designed a strategy that achieves an 

intended purpose, one can compare the strategy for efficiency against alternate versions by saving proofs 

that, use the different versions. The saved proofs include run time information that can be used for efficiency 

comparison. 

Comparisons for efficiency should be done over several examples, as there are often tradeoffs in the choice 

between two near-optimal versions of a strategy. Note that the PVS command TIME, which is similar to 

APPLY in that it turns a strategy into an atomic rule, has the additional effect of giving timing information 

for any branches created by the strategy on which the strategy does not terminate. Thus, TIME provides an 

additional resource in studies of efficiency: it can be used for strategy efficiency comparisons between the 

cases in the branches a strategy generates. 

Using PVS’s multiple proof feature. 

4 Examples of strategy design 

In this section, we provide several examples to further illustrate the kinds of reasoning steps that can be 

supported with PVS strategies, and to provide new PVS strategy developers with some useful ideas that 

they may wish to recycle in their own strategies. 

4.1 Some small-step strategy examples 

The example strategies in this section are geared towards carrying out tasks during interactive proving, and 

can be viewed as providing slightly more powerful versions of existing prover rules. Included are examples 

Of: 

- capturing a commonly used pattern of steps within a single step, 

- using TRY together with recursion to define a step that iterates a command over the list of arguments to 

- forking a “proof obligation” proof to simplify introducing a fact (as a conjecture) on the current proof 

- creating a new arithmetic reasoning step that is not supported by any standard PVS proof step. 

the step, 

branch, and 

Several of these examples also illustrate techniques from Section 3, including computing and then executing 

a command, use of CLOS probes into the proof state, use of Lisp helper functions, and use of PVS functions. 

Figure 7 shows a modest strategy apply-lemma that invokes a lemma after accepting a list of expressions 

for instantiating the variables. The strategy expands into a prover command of the form: 

(THEN (LEMMA name) (INST -1 expr-1 ... expr-n)) 

Note that the bindings of the LET construct in apply-lemma could have been written using Lisp’s backquote 

feature: 

(let ( (lemma-step ‘ (lemma ,lemma) 1 

(inst-step ‘(inst -1 ,@exprs))) 

(then lemma-step inst-step)) 
34 Myla Archer et al. 

(defstep apply-lemma (lemma &rest exprs) 

(let ((lemma-step (list 'lemma lemma)) 

(inst-step (cons 'inst (cons -1 exprs)))) 

(then lemma-step inst-step)) 

"Apply a lemma with explicit variable instantiations. 

Lemma variables appear in alphabetical order when introduced 

by the LEMMA rule. 

entering EXPRS . It 

That order needs to be observed when 

Il"%Invoking lemma -A on given expressions") 

Fig. 7. Applying a lemma and instantiating its variables. 

(defstep else* (&rest steps) 

(if (null steps) 

(skip) 

(let ((try-step ' (try , (car steps) 

(skip) 

(else*$ ,B(cdr steps) 1) 1 

try-step) 

"Try STEPS in sequence until the first one succeeds." 

""%Trying steps in sequence") 

Fig. 8. Generalization of the prover's ELSE strategical. 

In many cases this type of notation simplifies the coding effort and improves readability. We will make use 

of it in the remaining examples. 

Figure 8 illustrates a basic strategy pattern for trying a series of actions until one succeeds. When the 

first step is encountered that has an effect on the proof state, the strategy terminates without attempting any 

of the remaining steps. ELSE* can be thought of as a generalization of the prover's built-in ELSE strategical. 

It is likely to be useful as a building block for higher level strategies. 

The TRY strategical together with recursive invocation is employed to achieve the effect of conditional 

iteration. For each element of argument STEPS, if trying the step has no effect, ELSE* is invoked again on 

the remaining steps. TRY is applied to achieve the following general scheme: 

(TRY current-step (SKIP) recursive-invocation) 

Note the use of the strategy form (ELSE*$) rather than the rule form (ELSE*) in the recursive invocation. 

This is a convention often followed in PVS strategies. It ensures that when the top-level command is invoked 

as a nonatomic strategy, all subordinate strategies will be as well, resulting in a full expansion into predefined 

rules. 

(defstep rewrite-one (fnums &rest lemmas) 

(if (null lemmas) 

(skip) 

(let ((try-step 

'(try (rewrite ,(car lemmas) ,fnums) 

(skip) 

(rewrite-one$ ,fnums ,B(cdr lemmas))))) 

try-step)) 

"Try rewriting LEMMAS in sequence within FNUMS until the 

""%Trying lemma rewrites in sequence") 

first one succeeds. I' 

Fig. 9. Using the pattern for ELSE* in a more concrete setting. 
Developing User Strategies in PVS: A Tutorial 35 

, Figure 9 demonstrates how the pattern of ELSE* can be applied to a more concrete objective. Given a 

list of lemma names, REWRITE-ONE tries to rewrite with each lemma in turn until one is successful. It also 

the same recursive pattern presented in Figure 8. (See Section 3 for more on the use of term rewriting in 

, provides an argument FNUMS to control which part of the sequent should be subject to rewriting. It follows 

PVS.) 

(defstep claim-cond (cond) 

(steplist 

(let ((case-step (list 'case cond)) 

(list ' (skip) 

'(try (then (grind) (fail)) 

(skip) 

(skip-msg "Claim justification not proved" 

t))))) 

(spread case-step steplist)) 

"Try claiming a condition holds. 

step is attempted using (GRIND)." 

A proof of the justification 

""%Claiming the condition "A holds") 

I Fig. 10. Claiming a condition and trying to prove its justification. 

I 

I Figure 10 illustrates a different use for the TRY strategical. In CLAIM-COND, we wish to accept a PVS 

expression COND as a condition that holds in the current goal and introduce it as a new antecedent formula. 

We would also like to automatically prove that the condition holds. 

To carry out this task, we use CASE to introduce the supposition, then apply GRIND on the second branch 

generated by CASE to prove that COND holds. If GRIND fails to completely prove the justification, we undo 

the partial proof and leave it to the user to determine how to proceed. This behavior is obtained using the 

following scheme on the second branch generated by CASE: I 

(TRY (THEN (GRIND) (FAIL)) (SKIP) (SKIP-MSG message t)) 

Backtracking via FAIL is performed if the subgoal is not completely proved. In this case the SKIP-MSG rule 

is invoked to display a message to the user that the justification proof did not succeed. 

To direct the branching of the proof into subgoals, the SPREAD strategical is used. The first argument to 

SPREAD is a step that causes branching, which is CASE in this instance. The second argument is a list of steps 

for the follow-up actions to be performed for each subgoal. The second subgoal represents the justification 

proof for the claim, where the TRY construct is applied. 

i 

(defstep equate-terms (lhs rhs) 

(let ((case-eq (list 'case 

(format nil "(-A) = (-A)" lhs rhs))) 

( s tepl is t 

(list '(replace -1 :hide? t) 

'(try (then (grind) (fail)) 

(skip) 

(skip-msg "Equate justification not proved" 

t))))) 

(spread case-eq steplist)) 

"Try equating two expressions and replacing the LHS by the RHS. 

"-%Equating two expressions and replacing") 

A proof of the justification step is attempted using (GRIND)." 

Fig. 11. Claiming two terms are equal and carrying out replacement. 
36 Myla Archer et al. 

Figure 11 follows the same pat,tern as found in Figure 10. EQUATE-TERMS accepts two PVS expressions 

that are claimed to be equal, then substitutes one for the other. A new antecedent equality LHS = RHS will 

be added as a claim. REPLACE is applied to substitute RHS for LHS. Then a justification proof to establish the 

equality is carried out in the same manner as CLAIM-COND. 

Forming the CASE command requires some string manipulation, which is implemented using Lisp's FORMAT 

function. This is an example of a common operation in strategy writing. LET bindings are introduced to allow 

Lisp code to compute prover command invocations having whatever arguments are necessary. 

(defstep add-eq (fnuml fnum2) 

(let ((formula1 (get-fnum fnuml)) 

(formula2 (get-fnum fnum2)) 

(left-sum (format nil "-A + "A" 

(right-sum (format nil ""A + "A" 

(case-step '(case ,(format nil ""A = "AI' 

(steplist '((skip) (then (assert) (assert))))) 

(argsl formulal) (argsl formula2))) 

(args2 formulal) (args2 formula2))) 

lef t-sum right-sum) ) ) 

(spread case-step steplist)) 

"Given tuo antecedent equalities a = b and c = d, introduce 

""%Adding terms from "A and 'A to derive a new equality") 

a new formula relating their sums, a + c = b + d." 

Fig. 12. Adding two antecedent equalities to generate a third. 

Figure 12 illustrates the extraction of expressions from CLOS objects within the current proof state. 

ADD-Eq accepts two formula numbers for antecedent equalities involving numeric values. It then introduces 

a new antecedent equality that sums the two equations, i.e., given equations a = b and c = d, it forms 

a + c = b + d. The justification proof consists of two applications of ASSERT, which should be sufficient to 

prove the subgoal. 

To extract terms from the proof state, the formula objects are first retrieved using the Lisp function 

GET-FNUM described earlier. Assuming the formulae are equalities, their left hand and right hand sides can 

be accessed using the PVS functions ARGSl and ARGS2. When supplied as values to the FORMAT function, 

Lisp renders their textual representations as PVS expressions. This allows ordinary string manipulation to 

be used to construct new PVS expressions from fragments of the current sequent. 

Having formed the new antecedent equality as a text string, an application of the CASE rule is used 

to achieve the desired effect. In a more realistic strategy development effort, error checking code would 

be inserted at various places to check for invalid inputs. Strategy writers can decide how important such 

checking is for the intended purpose of their strategies. 

4.2 

Strategies geared to high level proof automation, either of full proofs or of proof steps at a high conceptual 

level, almost invariably require use of several of the techniques described in Section 3. To illustrate how some 

of the techniques described in Sections 2 and 3 can be applied to developing an automatic strategy for proving 

lemmas belonging to a particular class, we will show how the defined rule adt-uniquestrat from TAME 

was developed.' Although adt-uniquestrat was developed for TAME, it is useful in any context in which 

the DATATYPE construct is used: it allows the user to supply a one-step proof for any lemma that asserts that 

* A little history: development of TAME strategies began with an early version of PVS, in which the PVS step 

DECOMPOSE-EQUALITY was not a standard proof rule. With this rule, one can write a much simpler version of 

adt-unique-strat. The example in this section nevertheless serves to illustrate a general approach to creating a 

specialized high level strategy. 

Developing high level strategies: an example 
Developing User Strategies in PVS: A Tutorial 37 

if two elements of the same DATATYPE with the same constructor are equal, then the arguments to which the 

constructor is applied to obtain these elements must be pairwise equal. Figure 13 shows an example DATATYPE 

and its "uniqueness properties" taken from the TAME specification of the basic TESLA multicast stream 

authentication protocol [8,2]. Such a lemma is a corollary of the fact that the elements of any PVS DATATYPE 

form a free algebra, that is, a term algebra with no nontrivial equalities between terms. Unfortunately, the 

automatic PVS proof procedures such as ASSERT, SIMPLIFY, and GRIND do not automatically "know" this 

information. Moreover, as can be seen from the proof of Receive-unique in Figure 14, one does not really 

actions: DATATYPE 

BEGIN 

nu(timeof : (f intime?)) : nu? 

SSend (Si:nat, Sc,Skl,Sk2:Key, Sm:Message): SSend? 

ASend (Ai:nat, Ac:Comit, Akl,Ak2:Key. Am:Message): ASend? 

Receive (RSentPacket:SentPacket): Receive? 

END actions 

nu-unique: LEMMA FORALL (tl, t2: (fintime?)): 

Send-unique: LEMMA FORALL (il,i2:nat, cl,c2.kll.k12,k21,k22: Key, 

nu(t1) = nu(t2) => ti = t2; 

ml~n2:Message): 

SSend(i1 ,cl ,kll ,k21 ,ml) = SSend(i2, c2 ,k12 ,k22 ,m2) 

=> il=i2 & cl=c2 & kll=k12 & k21=k22 & ml=m2; 

ASend-unique: LEMMA FORALL(il,iZ:nat, cl,c2:Comit, 

kll,k12,k21,k22: Key, m1,nQ:Message): 

ASend(i1 ,cl , kll , k21 ,ml) = ASend(i2 ,c2 ,k12 ,k22 ,m2) 

=> il=i2 & cl=c2 & kll=k12 & k21=k22 & ml=m2; 

Receive-unique: LEMMA FORALL (spl, sp2: Sentpacket): 

Receive(sp1) = Receive(sp2) => spl = sp2; 

Fig. 13. Example of a PVS DATATYPE declaration, and its "uniqueness lemmas". 

want to make an excursion in a PVS proof to establish this property. 

The first step in developing adt-uniquestrat is to prove several uniqueness lemmas in PVS and look for 

patterns. Figure 14 shows the pattern to follow in establishing a uniqueness lemma for a constructor with one 

( " " 

(SKOLEM! ) 

(FLATTEN) 

(CASE "spl! 1 = RSentPacket(Receive(spl!l))") 

(("1" (CASE "sp2!1 = RSentPacket(Receive(sp2! 1))") 

(('1111 

(APPLY (THEN (REPLACE -1 +) (REPLACE -2 +) (HIDE -1 -2))) 

(REPLACE -1) 

(PROPAX) 1 

("2" (ASSERT) 1) 1 

("2" (ASSERT) 1) 

Fig. 14. Proof of a uniqueness lemma for a DATATYPE constructor with one parameter. 

parameter: One can see that, after skolemizing and flattening the formula in the lemma, one does two case 

splits, each based on an equality of an individual skolem constant to an application of the single datatype 

accessor function RSentPacket for Receive actions to an application of the Receive constructor to the same 
38 Myla Archer et al. 

(I, It 

(SKOLEM 1 

(FLATTEN) 

(SPLIT) 

( ("I" (CASE " i - 1 = Si ( SSend (i- 1 , c-I , kl- 1 , k2- 1 .m-l) ) " ) 

( ( " 1" (CASE "i-2 = Si ( SSend (i-2, c-2, kl -2, k2-2 ,m- 2) ) " ) 

(APPLY (THEN (REPLACE -1 +) (REPLACE -2 +) (HIDE -1 -2))) 

(REPLACE -1) 

(PROPAX) 

(Wi-lll "i-2" ,OC-l" I, c-2" "kl-I" "k1-2" "k2-1" "k2-2" "m-I" "m-2")) 

(("1" 

("2" (ASSERT)))) 

("2" (ASSERT) )) 1 

("2" (CASE "c-1 = Sc(SSend(i-1 ,c-1 ,kl-l ,k2-1 ,m-l)) ") 

(("1" (CASE "c-2 = Sc(SSend(i-2,~-2,kl-2,k2-2,m-2)) ") 

((''1" 

(APPLY (THEN (REPLACE -1 +) (REPLACE -2 +) (HIDE -1 -2))) 

(REPLACE -1) 

(PROPAX) ) 

("2" (ASSERT) )) 

("2" (ASSERT) 1)) 

("3" (CASE "kl-1 = Skl(SSend(i-1 ,c-1 ,kl-l ,k2-1 ,m-l))") 

( ("1" (CASE "kl-2 = Skl (SSend(i-2 ,c-2 ,k1-2 ,k2-2,m-2) )"I 

(("1" 

(APPLY (THEN (REPLACE -1 +) (REPLACE -2 +) (HIDE -1 -2))) 

(REPLACE -1) 

(PROPAX) 

("2" (ASSERT) 1) 1 

("2" (ASSERT) ))) 

("4" (CASE "k2-1 = Sk2(SSend(i_l,c_l.kl~l,k2~l,m~l))") 

( ("1" (CASE "k2-2 = Sk2(SSend(i-2, c-2,k1-2.k2-2 ,rn-2)) ") 

(("1" 

(APPLY (THEN (REPLACE -1 +) (REPLACE -2 +) (HIDE -1 -2))) 

(REPLACE -1) 

(PROPAX) 

("2" (ASSERT) 1) ) 

("2" (ASSERT)))) 

("5" (CASE "m-1 = Sm(SSend(i-1, c-l,kl-l,k2-l,m-l))") 

( ("1" (CASE "m-2 = Sm(SSend(i-2 ,c-2,k1-2 ,k2-2 ,rn-2) )"I 

(("1" 

(APPLY (THEN (REPLACE -1 +) (REPLACE -2 +) (HIDE -1 -2))) 

(REPLACE -1) 

(PROPAX) ) 

("2" (ASSERT) 1) 

("2" (ASSERT)))))) 

Fig. 15. Proof of a uniqueness lemma for a DATATYPE constructor with five parameters. 

skolem constant. The technique used in this proof can be adapted to handle the case of a constructor with 

more arguments. Figure 15 shows a proof of the uniqueness lemma for the constructor SSend: 

The proof of this lemma also begins with skolemization and flattening, but this is followed by a SPLIT 

command. By executing the proof, one can see that the SPLIT splits the proof into subcases, one for each 

accessor function of SSend, and therefore, calling (SPLIT) at the third step in the shorter proof would have 

no effect. In each subcase of the longer proof, the pattern in the shorter proof reappears. Moreover, this 

pattern is now more detailed: the two individual skolem constants correspond to the variables retrieved by 

the accessor function, and the constructor Send is applied not just to these skolem constants, but to the 

two sets of skolem constants corresponding to the variables in the Send expressions in the hypothesis of the 

lemma. 

We now have enough information to design a strategy. We can begin by defining a Lisp function that 

returns a command that follows the pattern of the subcases. Figure 16 shows the definition of such a function: 

mk-adt-unique-case, which takes as arguments the accessor function name, the two skolem constant names, 

and the two instantiated constructor expressions used in the pattern. We will expect to begin our strategy 

as the proof in Figure 15 begins: with a skolemization step, a (FLATTEN), and a (SPLIT). Following the 
Developing User Strategies in PVS: A Tutorial 39 

(defun mk-adt-unique-case (acc skconst-1 skconst-2 

sk-expr-1 sk-expr-2) 

(let ( (firstcase 

(format nil ""a"a"a"a"a"a" 

skconst-1 'I = I' acc "(" sk-expr-1 I')'I>) 

(secondcase 

(format nil ""a"a"a"a"a"a" 

skconst-2 'I = 'I acc "(" sk-expr-2 'I) ") 1) 

((spread (case ,secondcase) 

'(spread (case ,firstcase) 

((then (replace -1 +) 

(replace -2 +) 

(hide -1 -2) 

(replace -1)) 

(assert))) 

(assert) 1) ) 1 

Fig. 16. A Lisp function that computes a command to prove a uniqueness lemma case. 

(SPLIT) command, we then plan to use SPREAD to apply an appropriate subcase command to each of the 

su bgoals . 

To apply SPREAD, we we need a list of appropriate subcase commands, so we next define a Lisp function 

collectadt-unique-cases that returns such a list, as follows. Fkom the proof of the lemma SSend-unique 

in Figure 15, we see that there is a uniqueness case for every accessor function. Moreover, the two instantiated constructor expressions are the same for each uniqueness case, and the two skolem constants in each 

uniqueness case appear in these two expressions in the position corresponding to the accessor function. The 

function collectadt-unique-cases, whose definition is shown in Figure 17, expects as arguments 1) the 

list of accessors for a DATATYPE constructor, 2) a list of skolem constant names for the quantified variables 

in the uniqueness lemma for the constructor, which by convention are arranged in the lemma formulation 

so that the first two correspond to the first accessor, the second two correspond to the second accessor, and 

so on, and 3) and 4) two constructor expressions in which the skolem constants are correctly matched with 

their corresponding accessor positions. 

(defun collect-adt-unique-cases (acclist skconstlist 

sk-expr-1 sk-expr-2) 

(cond ((null acclist) nil) 

(t (cons 

(mk-adt -unique-case 

(car acclist) 

(car skconstlist) (cadr skconstlist) 

sk-expr-1 sk-expr-2) 

(cdr acclist) (cddr skconstlist) 

sk-expr-1 sk-expr-2) 1 1)) 

(collect-adt-unique-cases 

Fig. 17. A Lisp function that computes a list of uniqueness-case commands. 

Note that to work correctly when it is applied, collectadt-unique-cases must be given the appropriate 

arguments. Appropriate arguments can be computed from the formula in the lemma being proved. To 

compute the constructor expression instances corresponding the list of skolem constants, we need to know 

the names of the skolem constants. A convenient way to do this is to compute special skolem constant names 

from the list of bound variables in the lemma. Once the prover is invoked on the lemma, this can be done 

by using the Lisp function get-bindingnames (see Figure 18) to probe the proof state for the names of 
40 Myla Archer et al. 

(defun get-binding-names (sform) 

(defun mk-adt-unique-skolem-names (varlis) 

(mapcar 'id (bindings (formula sform)))) 

(mapcar #' (lambda (varname) 

(concatenate 'string (string varname) "-uniq")) 

varlis) 

(defun get-sk-constructor-exprs (sform) 

(expre (argument (car (exprs (argument (formula sf orm) 1) ) ) ) ) 

Fig. 18. Three auxiliary functions used in datatype-unique-strat. 

the bound variables, and then applying the Lisp function mk-adt -uniqueskolemnames to transform this 

list into a list of skolem names for the bound variables. The two constructor expressions are found by again 

probing the proof state, this time using the function get-sk-constructor-exprs. 

Finally, we can define the proof rule adt-uniquestrat, using the def step macro, as shown in Figure 19. 

Note that both adt-uniquestrat and its auxiliary rule adt-uniquestrat-continue begin with a probe of 

the proof state *ps* to retrieve a value sf om representing the current proof goal. The expected proof goal 

for adt-uniquestrat corresponds to a uniqueness lemma. The initial call to (ASSERT) in adt-uniquestrat 

assures that PVS has filled in all the fields in the CLOS structure for this goal, rather than lazily leaving 

them unbound. Both proof steps use the technique of first computing and then applying a command. 

(def step adt-unique-strat 0 

(then 

(assert) 

(let ((sform (car (s-forms (current-goal *ps*)))) 

(bind-names (get-binding-names sform)) 

(uniq-sk-names 

( cmd 

(mk-adt-unique-skolem-names bind-names)) 

' (then (skolem 1 ,uniq-sk-names) 

(adt-unique-strat-continue ,uniq-sk-names)))) 

cmd) 1 Ill1 llll) 

(def step adt-unique-strat-continue (sk-name-list) 

(let ((sf om (car (s-forms (current-goal *ps*)) 1) 

(sk-constr-exprs (get-sk-constructor-exprs sform)) 

(sk-constr-expr-1 (car sk-constr-exprs)) 

(sk-constr-expr-2 (cadr sk-constr-exprs)) 

(constr-name (id (operator sk-constr-expr-1))) 

(all-constrs 

(constructors 

(adt (adt-type (operator sk-constr-expr-1)))))) 

(let ( (constr-form (car 

(select #' (lambda (x) (eq (id x) constr-name)) 

(accessors (mapcar 'id (acc-decls constr-form))) 

(cases 

all-constrs) 1) 

(collect-adt-unique-cases accessors sk-name-list 

sk-constr-expr-1 

sk-constr-expr-2) 1 

(cmd ' (then (flatten) (spread (split) ,cases)))) 

cmd) 1 IIII It 11) 

Fig. 19. Defining a new proof rule adt-uniquestrat. 
Developing User Strategies in PVS: A Tutorial 41 

The effect of the part of adt-uniquestrat up to the point where it calls adt-uniquestrat-continue is 

to skolemize the formula in the lemma using the skolem constants computed by mk-adt-uniqueskolemnames. 

Thus, the value sf orm computed at the beginning of adt-uniquestrat-continue corresponds to the skolemized version of the uniqueness lemma. Moreover, adt-uniquestrat-continue is passed the list of skolem 

names as an argument so that it need not be recomputed. The step adt-uniquestrat-continue proceeds 

by first computing the arguments it needs to pass to the function collectadt-unique-cases, and uses the 

result of applying this function to the arguments in its computation of a proof command in the form of a 

strategy, which it then applies. 

5 Discussion 

Chapter 5 of the PVS Prover Guide [lo, 111 contains much information useful to users who wish to write 

their own strategies. This information includes a description of global variables used in the prover, the CLOS 

slots in a proof state, methods for retrieving formulae and recognizing the class of an expression, several 

useful PVS functions including argsl, args2, and gather-fnums, and the macros def step, defhelper, and 

def strat for defining new rules and strategies. 

Several things could provide additional help for writing user strategies in PVS. One is simply easily accessible documentation of additional useful PVS functions and macros. Documentation of the helper functions 

used in the standard PVS strategies would eliminate duplication of effort on the part of PVS users who write 

their own strategies. 

Currently, the CLOS structure must be probed to determine how to retrieve many details of the information on the proof state. Explicit documentation of this structure could allow this “probing” to be done 

off-line. 

Strategies that explicitly reference the CLOS structure used for the internal representation of the PVS 

whose names and effects would remain the same despite any changes in the internal representation of the 

proof state is one possibility for reducing the sensitivity of user strategies to any changes in the PVS 

implementation. 

Even without these extra aids, however, it is possible for users to develop sophisticated strategies to serve 

their special needs-and to share with others. 

I proof state must rely on the stability of this internal representation. An extra layer of “retrieval” functions 

Acknowledgement 

! Many thanks to N. Shankar for clarifying the semantics of TRY and providing several examples of its use. 

We also thank both N. Shankar and S. Owre for helpful comments. 

References 

1. Myla Archer. TAME: Using PVS strategies for special-purpose theorem proving. Annals of Mathematics and 

Artificial Intelligence, 29( 1-4):139-181, 2000. Published Feb., 2001. 

2. Myla Archer. Proving correctness of the basic TESLA multicast stream authentication protocol with TAME. In 

Informal Proceedings of the Workshop on Issues in the Theory of Security (WITS’O2), Portland, OR, Jan. 14-15 

2002. 

3. Myla Archer, Constance Heitmeyer, and Elvinia Riccobene. Proving invariants of 1/0 automata with TAME. 

Automated Software Engineering, 9(3):201-232, 2002. 

4. M. Devillers, D. Griffioen, J. Romijn, and F. Vaandrager. Verification of a leader election protocol-formal 

methods applied to ieee 1394. Formal Methods in System Design, 16(3):307-320, June 2000. 

5. B. Di Vito. A PVS prover strategy package for common manipulations. Technical Memorandum NASA/TM2002-211647, NASA Langley Research Center, Hampton, VA, April 2002. 

6. C. Muiioz and M. Mayero. Real automation in the field. Technical Report Interim ICASE Report No. 39, 

NASA/CR-2001-211271, ICASE, Mail Stop 132C, NASA Langley Research Center, Hampton, VA 23681-2199, 

USA. December 2001. 
42 Myla Archer et al. 

7. S. Owre and N. Shankar. PVS APZ Reference. SRI Computer Science Laboratory, Menlo Park, California, USA, 

September 2003. 

8. Adrian Perrig, Ran Canetti, J. D. Tygar, and Dawn Song. Efficient authentication and signing of multicast 

streams over lossy channels. In Proc. of IEEE Security and Privacy Symposium (SbP2000), pages 56-73, May 

2000. 

9. John Rushby. Personal communication. 2003. 

10. N. Shankar, S. Owre, J. M. Rushby, and D. W. J. Stringer-Calvert. The PVS prover guide. Technical report, 

11. N. Shankar, S. Owre, J. M. Rushby, and D. W. J. Stringer-Calvert. PVS Prover Guide, Version 2.4. Technical 

12. Guy L. Steele. COMMON LISP: the Language. Digital Press, Bedford, MA, 1990. Second edition. 

Computer Science Lab., SRI Intl., Menlo Park, CA, 1998. 

report, Computer Science Lab., SRI Intl., Menlo Park, CA, November 2001. 
Strategy-Enhanced Interactive Proving and Arithmetic 

Simplification for PVS 

Ben L. Di Vito 

NASA Langley Research Center, Hampton VA 23681, USA 

b.l.divito@larc.nasa.gov 

http://shemesh.larc.nasa.gov/lbld 

Abstract. We describe an approach to strategy-based proving for improved interactive deduction 

in specialized domains. An experimental package of strategies (tactics) and support functions called 

Manip has been developed for PVS to reduce the tedium of arithmetic manipulation. Included are 

strategies aimed at algebraic simplification of real-valued expressions. A general deduction architecture 

is described in which domain-specific strategies, such as those for algebraic manipulation, are supported 

by more generic features, such as term-access techniques applicable in arbitrary settings. An extended 

expression language provides access to subterms within a sequent. 

I 

I 1 Introduction 

Recent verification research at NASA Langley has emphasized extensive theorem proving over the domain of 

reals [4,5], with PVS [15] serving as the primary proof tool. Efforts in this area have met with some difficulties, 

prompting a search for improved techniques for interactive proving. Significant productivity gains will be 

needed to fully realize our formal methods goals. 

For arithmetic reasoning, PVS relies on decision procedures augmented by automatic rewriting. When a 

conjecture fails to yield to these tools, which often happens with nonlinear arithmetic, considerable interactive 

work may be required to complete the proof. Large productivity variances are the result. 

SRI continues to increase the degree of automation in PVS. In particular, decision procedures for real 

arithmetic are a planned future enhancement. We look forward to these improvements. Nevertheless, there 

will always be a point where the automation runs out. When that point is reached, tactic-basedl techniques 

can be applied to good effect. 

In this paper we describe an approach to strategy-based proving for improved interactive deduction in 

specialized domains. An experimental package of strategies (tactics) and support functions called Manip has 

been developed for PVS to reduce the tedium of arithmetic manipulation. Included are strategies aimed at 

algebraic simplification of real-valued expressions. A general deduction architecture is described in which 

domain-specific strategies, such as those for algebraic manipulation, are supported by more generic features, 

such as term-access techniques applicable in arbitrary settings. User-defined proof strategies can be seen as 

a type of “deductive middleware.” Our approach is general enough to serve other problem domains in the 

pursuit of such middleware. 

By way of motivation, consider the following lemma for reasoning about trigonometric approximations: 

~ 

~ 

I 

I 

where Ti(.) is the ith term in the power series expansion of the sine function: 

In PVS nomenclature, a rule is an atomic prover command while a strategy expands into one or more atomic 

steps. A defined rule is defined as a strategy but invoked as an atomic step. For our purposes, we regard the terms 

“txtic,” “strategy” and “defined rule” as roughly synonymous. 
44 Ben L. Di Vito 

Using only built-in rules, an early proof attempt for (1) required 68 steps. A common technique to carry 

out algebraic manipulation in such proofs is to use the case rule to force a case split on the (usually obvious) 

equality of two subexpressions, such as: 

(CASE "a!l * a!l * (b!l * b!l) = (b!l * a!l) * (b!l * a!l>") (2) 

Although not peculiar to PVS, this need to identify equivalent subexpressions and bring them to the prover's 

attention via cut-and-paste methods is rather awkward. It leads to a tedious style of proof that tries the 

patience of most users. 

In contrast, by using the Manip package we were able to prove the lemma more naturally in 18 steps, 

8 of which are strategies from our package, as shown in Fig. 1. Unlike the case-split technique, none of 

the steps contains excerpts from the sequent, such as those seen in (2). This proof represents one of the 

better examples of improvement from the use of our strategies. Although many proofs will experience a less 

dramatic reduction in complexity, the results have been encouraging thus far. 

( " " (SKOSIMP* 

(REWRITE " s in-t em-next 'I 

(RECIP-MULT! (! 1 R (-> 'labs") 1)) 

(APPLY (REPEAT (REWRITE 'labs-mult") 

(PERMUTE-MULT 1 R 3 R) 

(OP-IDENT I L I*) 

(CANCEL 1) 

(("1" (EXPAND "abs") 

(ASSERT) 

(PERMUTE-MULT 1 R 2 R) 

(CROSS-MULT 1) 

(MULT-INEQ -2 -2) 

(TYPEPRED "PI") 

(EXPAND "PI-ub") 

(MULT-INEQ -4 -4) 

(ASSERT) 1 

(GRIND NIL :REWRITES ("abs") )) 

("2" (USE "sin-term-nonzero") 

; strategy 

; strategy 

; strategy 

; strategy 

; strategy 

; strategy 

; strategy 

; strategy 

Fig. 1. Proof steps for lemma (1) using built-in rules plus manipulation strategies 

2 Architecture 

We have integrated several elements to arrive at a strategy-based deduction architecture for user enhancements to PVS. 

1. Domain-specific proof strategies. Common reasoning domains, such as nonlinear real arithmetic, provide 

natural targets for increasing automation. Extracting terms from sequents using suitable access facilities 

is vital for implementing strategies that do meaningful work. 

2. Extended expression language. Inputs to existing prover rules are primarily formula numbers and expressions in the PVS language. For greater effectiveness, we provide users with a language for specifying 

subexpressions by location reference and pattern matching. 

3. Higher-order strategies with substitution. Strategies that apply other proof rules offer the usual convenience of functional programming. Adding command-line substitutions derived from sequent expressions 

yields a more powerful way to construct and apply rules dynamically. 

4. Prelude extension libraries. The PVS prelude holds built-in core theories. Strategies use prelude lemmas but often need additional facts. PVS's prelude extension feature adds such theorems in a manner 

transparent to the user. 
Strategy-Enhanced Interactive Proving and Arithmetic Simplification for PVS 45 

5. User-interface utilities. To improve command line invocation of proof rules as well as offer various proof 

maintenance functions, a set of Emacs-based interface enhancements is included. 

Note that only elements 1 and 4 are domain specific; the others are quite generic. In this paper we will focus 

on elements 1-3. 

Several benefits accrue from the complementary elements of this architecture. 

- User interaction is more natural, less laborious and occurs at a higher level of abstraction. 

- Many manipulations apply lemmas from the prelude or its extensions. Strategies enable proving without 

- The brittleness of proofs (breakage caused by changes in definitions or lemmas) is reduced by avoiding 

- Proving becomes more approachable for those with mathematical sophistication but little experience 

explicit knowledge of these lemmas. 

the inclusion of expressions from the current sequent in stored proof steps. 

using mechanical provers. 

We envision some features as being more useful during later stages of proof development, especially when 

finalizing a proof to make the permanent version more robust. During the early stages, it is easier to work 

directly with actual expressions. Once the outline of a proof is firm, extended expression features can be 

introduced to abstract away excessive detail. 

3 Domain-Specific Strategies 

Systematic strategy development for various domains could improve user productivity considerably. This 

section proposes a general scheme for structuring and implementing strategies in PVS and briefly sketches a 

particular set of strategies for manipulating arithmetic expressions. 

3.1 Design Considerations 

Input to the PVS prover is via Lisp s-expressions. Internally the prover uses CLOS (Common Lisp Object 

System) classes to represent expressions and other data. PVS provides macros for creating user-defined proof 

rules, which may include fragments of Lisp code to compute new values for invoking other rules. 

1. 

2. 

3. 

4. 

5. 

We suggest the following guidelines for developing a strategy package. 

Introduce domain-relevant arguments. For arithmetic strategies, a user typically needs to specify values 

such as the side of a relation (L, R), the sign of a term (+, -), and term numbers. Variations on the 

conventions of existing prover input handle these cases nicely. 

Augment term access functions. Besides the access functions provided by the prover, additional ones may 

be needed to extract relevant values, e.g., the ith term of an additive expression. A modest set of access 

functions suffices for working with common language elements, such as arithmetic terms. 

Use text-based expression construction. A proper implementation style would be to use object constructors to create new expression values. This requires knowledge of a large interface. Instead, it is adequate 

for most uses to exploit the objects’ print methods and construct the desired expressions in textual form, 

which can then be supplied as arguments to other proof rules. 

Use Lisp-based symbolic construction. To build final proof rules for invocation, the standard Lisp techniques for s-expression construction, such as backquote expressions, work well. 

Incorporate prelude extensions as needed. When prelude lemmas are inadequate to support the desired 

deductions, a few judiciously crafted lemmas, custom designed for specific strategies, can be added 

invisibly. 

Applications of items 1-4 are demonstrated in the simple example of Fig. 2. Most strategies are rather more 

complicated than this example, often requiring the services of auxiliary Lisp functions and intermediate 

helper strategies. 

An example of a prelude extension lemma of the sort described in guideline (5) is the following: 

div-mult-pos-neg-ltl: LEMMA 

z/nOy < x IFF IF nOy > 0 THEN z < x * nOy ELSE x * nOy < z ENDIF 
46 Ben L. Di Vito 

(DEFSTEP has-sign (term &optional (sign +) (try-just nil) 

(LET ((term-expr (ee-obj-or-string (car (eval-ext-expr term)))) 

(relation (case sign 

((+I '>I ((-1 '4 ((0) '=I 

((O+) '>=I ((0-1 '<=I ((+-I '/=) (t '>I)) 

(case-step ' (CASE , (format nil "-A -A 0" term-expr relation))) 

(step-list 

(list '(SKIP) (try-justification 'has-sign try-just)))) 

(SPREAD case-step step-list)) 

"Try claiming that a TERM has the designated SIGN (relationship to 0). 

Symbols for SIGN are (+ - 0 O+ 0- +-I, which have meanings positive, 

negative, zero, nonnegative, nonpositive, and nonzero. Proof of the 

justification step can be tried or deferred. Use TRY-JUST to supply 

a step for the justification proof or T for the default rule (GRIND)." 

"-%Claiming the selected term has the designated sign") 

Fig. 2. Sample strategy built using PVS def step macro 

This lemma simply combines two existing lemmas in prelude theory real-props into a conditional form to 

allow rewriting for any nonzero divisor. In ordinary settings, rewriting to such a conditional expression is 

likely to be undesirable. In this case, however, the lemma accommodates rewriting plus follow-up steps such 

as case splitting. 

Following the design guidelines above will lead to strategies that are sound by construction. Prover objects 

are examined but not modified. Proof steps are obtained by expanding the strategies into rule applications for 

execution by the prover. New PVS expressions are submitted through the parser and typechecked. There are 

no mechanisms to enforce these good intentions, however. Coding errors could have unintended consequences, 

but with proper care there should be no side effects on the proof state. 

3.2 Algebraic Manipulation Strategies 

Users often want to manipulate expressions in the familiar style of conventional algebra, as one would do on 

paper. We now present a brief sampling of an arithmetic package to support this goal. Selected strategies 

are discussed that illustrate typical design choices. Appendix A lists the primary strategies in this family. 

Full details are available in a technical report [8] and user's manual [9]. 

- move-terms fnum side &optional (term-nums *) 

With move-terms a user can move a set of additive terms numbered term-nums in relational formula 

fnum from side (L or R) to the other side, adding or subtracting individual terms from both sides as 

needed. term-nums can be specified in a manner similar to the way formula numbers are presented to 

the prover. Either a list or a single number may be provided, as well as the symbol "*" to denote all 

terms on the chosen side. Example: invoking (move-terms 3 L (2 4)) moves terms 2 and 4 from the 

left to the right side of formula 3. 

- cross-mult &optional (fnums *) 

To eliminate divisions, cross-mult may be used to explicitly perform "cross multiplication" on one or 

more relational formulas. For example, a/b < c/d will be transformed to ad < cb. The strategy determines 

which lemmas to apply based on the relational operator and whether negative divisors are involved. Cross 

multiplication is applied recursively until all outermost division operators are gone. 

- cancel &optional (fnums *) (sign nil) 

When the top-level operator on both sides of a relation in hums is the same operator drawn from the 

set {+, -, *, /}, cancel tries to eliminate common terms using a small set of rewrite rules and possible 

case splitting. Cancellation applies when fnum has the form x o y R x o z or y o x R z o x. In the default 

case, when sign is NIL, x is assumed to be (non)positive or (non)negative as needed for the appropriate 
Strategy-Enhanced Interactive Proving and Arithmetic Simplification for PVS 47 

rewrite rules to apply. Otherwise, an explicit sign can be supplied to force a case split so the rules will 

apply. If sign is + or -, x is claimed to be strictly positive or negative. If sign is O+ or 0-, x is claimed 

to be nonnegative or nonpositive. If sign is *, x is assumed to be an arbitrary real and a three-way case 

split is used. Example: (cancel 3 O+) tries to cancel from both sides of formula 3 after first splitting 

on the assumption that the common term is nonnegative. 

- factor fnums &optional (side *) (term-nums *) (id? nil) 

factor! expr-loc &optional (term-nums *) (id? nil) 

If the expression on side of each formula in fnums has multiple additive terms, factor may be used to 

extract common multiplicative factors and rearrange the expression. The additive terms indicated by 

term-nums are regarded as bags of factors to be intersected for common factors. Terms not found in 

term-nums are excluded from this process. In the !-variant, the expr-loc argument supplies a location 

reference to identify the target expression so that it may be factored in place. As an example, suppose 

formula 4 has the form 

f(x) = 2 * a * b + c * d - 2 * b 

and the command “(factor 4 R (1 3))” is issued. Then the strategy will rearrange formula 4 to: 

We provide several strategies for manipulating products or generating new products. This supports an 

overall approach of first converting divisions into multiplications where necessary, then using a broad array 

of tools for reasoning about multiplication. Three examples follow. 

- permute-mult fnums &optional (side R) (term-nums 2) (end L) 

For end = L, the action of permute-mult is as follows. Let the expression on side of a formula in fnums be a 

product of terms, P = tl*. . .*t,. Identify a list of indices I (term-nums) drawn from { 1,. . . , n}. Construct 

the product ti, * . . . * ti, where ik E I. Construct the product tj, * . . . * tj, where jk E (1,. . . , n} - I. 

Then rewrite the original product P to the new product ti, * . . . * ti, * tj, * . . . * tj,. Thus the new 

product is a permutation of the original set of factors with the selected terms brought to the left. For 

end = R, the selected terms are placed on the right. Example: (permute-mult 3 L (4 2)) rearranges 

the product on the left side of formula 3 to be t4 * t2 * t1 * t3, with the default association rules 

making it internally represented as ((t4 * t2) * ti) * t3. 

- mult-eq rel-fnum eq-fnum &optional (sign +) 

Given a relational formula a R b and an antecedent equality x = y, mult-eq forms a new antecedent or 

consequent relating their products, a *x R b* y. If R is an inequality, the sign argument can be set to one 

of the symbols in {+, -, O+, 0-} to indicate the polarity of x and y. Example: (mult-eq -3 -2 -1 

multiplies the sides of formula -3 by the sides of equality -2, which are assumed to be negative. 

- mult-ineq fnuml fnum2 &optional (signs (+ +)) 

Given two relational formulas fnuml and fnum2 having the forms a R1 b and x R2 y, mult-ineq forms a 

new antecedent relating their products, a * x R3 b * y. If R2 is an inequality having the opposite direction 

as R1, mult-ineq proceeds as if it had been y Rh x instead, where Rh is the reverse of R2. The choice 

of R3 is inferred automatically based on R1, Rz, and the declared signs of the terms. R3 is chosen to be 

a strict inequality if either R1 or R2 is. If either formula appears as a consequent, its relation is negated 

before carrying out the multiplication. Not all combinations of term polarities can produce useful results 

with mult-ineq. Therefore, the terms of each formula are required to have the same sign, designated 

by the symbols + and - in argument signs. Example: (mult-ineq -3 -2 (- +)) multiplies the sides of 

inequality formula -3 by the sides of inequality -2, which are assumed to relate negative and positive 

values, respectively. 

Figure 3 illustrates these strategies by displaying several proof steps for lemma (1) (see Fig. 1). 
48 Ben L. Di Vito 

sin-terms-decr.1 : 

C-11 0 < a!l 

C-23 a!l <= PI / 2 

I ------- 

11) I > 2 * 

((1 / (4 * (n!l * n!i) 

* --I * a!l * a!l) 

+ 2 * n!l)) 

Multiplying both sides of selected 

formulas by LHS/RHS divisor (s) , 

this simplifies to: 

sin-terms-decr.1 : 

Rule? (PERMUTE-MULT 1 R 2 R) 

Rule? (MULT-INEQ -2 -2) 

Permuting factors in selected 

expressions, this simplifies to: 

sin-terms-decr. I : 

[-I3 0 < a!l 

C-23 a!l <= PI / 2 

I ------- 

{l) 1 > 2 * --I * a!l * a!l * 

(1 / (4 * (n!l * n!l) 

+ 2 * n!l)) 

Rule? (CROSS-MULT 1) 

Multiplying terms from formulas -2 

and -2 to derive a new inequality, 

this simplifies to: 

sin-terms-decr.1 : 

Fig. 3. Proof trace fragment for selected steps from Fig. 1 

4 Extended Expression Language 

Many prover rules accept PVS expressions as arguments, which take the form of literal strings such as 

“2 * PI * a! 1”. Strategies in our package may be supplied extended expressions as well as the familiar text 

string form. This works equally well at the command line and within strategy definitions. 

The main extensions provided are location references and textual pattern matching. Location references 

allow a user to indicate a precise subexpression within a formula by giving a path of indices to follow when 

descending through the formula’s expression tree. Pattern matching allows strings to be found and extracted 

using a specialized pattern language that is based on, but much less elaborate than, regular expressions. 

4.1 Location References 

In the location reference form ( ! <ext-expr> il . . . in), the starting point <ext-expr> must describe 

the location of a valid PVS expression within the current sequent. Usually this is a simple formula number 

or one of the formula-list symbols {+, -’ *}. The index values {ij} are used to descend the parse tree to 

arrive at a subexpression, which becomes the final value of the overall reference. Actually, the final value is a 

list of expressions, which allows for wild-card indices to traverse multiple paths through the tree. Moreover, 

the index values may include various other forms and indicators used to control path generation. 

Location references may be used as arguments for certain strategies where a mere text string is inadequate. 

For example, the factor! strategy can factor an expression in place using this feature even if the target 

terms appear in the argument to a function. Thus, location references are reminiscent of array or structure 

references in procedural programming languages. 

An example of a simple location reference is ( ! -3 2), which evaluates to the right-hand side (argument 

2) of formula -3. If this formula is “x! 1 = cos(a! l)”, then the string form of the location reference is 

“cos(a! 1)”. Adding index values reaches deeper into the formula, e.g., (! -3 2 1) evaluates to “a! 1”. 

Breadth can be achieved as well as depth; (! -3 *> evaluates to a list containing “x! 1” and “cos(a! 1)”. 

Index values and directives {ij} may assume one of the following forms: 
Strategy-Enhanced Interactive Proving and Arithmetic Simplification for PVS 49 

- An integer i in the range 1,. . . , k, where k is the arity of the function at the current point in the expression 

tree. Paths follow the ith branch or argument, returning the argument as value if i is the last index. The 

symbols L and R are synonyms for 1 and 2. 

an expression, as f(z) in f(z)(y), indices after the 0 will retrieve components of the expression. 

- The wild-card symbol *, which indicates that this path should be replicated for each argument expression, 

returning values from all n paths. 

- A list (j 1 . . . jm) of integers indicating which argument paths should be included for replication, i.e., 

a subset of the * case. 

- One of the deep wild-card symbols {-*, *-, **}, which indicates that this path should be replicated as 

many times as needed to visit all nodes in the current subtree. The values returned are the leaf objects 

(terminal nodes) for -*, the nonterminal nodes for *-, and all nodes (subexpressions) for **. - A text string serving as a guard to select desired paths from multiple candidates. If the current function 

symbol matches the string, path elaboration continues. Otherwise, the path is terminated, returning an 

empty list. 

- A list (si . . . sk) of strings that serves as a guard by matching each pattern s, in the manner of 

Section 4.2. 

- A form (-> gl . . . gk) that serves as a go-to operator to specify a systematic search down and across 

the subtree until the first path is found having intermediate points satisfying all the guards {g2} in 

sequence. The form (->* gl . . . gk) returns all eligible paths. 

, 

I - The index value 0, which returns the function symbol of the current expression. If the function is itself 

I 

Table 1 illustrates the formulation of location references using this notation. 

Note that indexing works for both infix and prefix function applications. For arithmetic expressions, special indexing rules result in some “flattening” of the parse tree during traversal. These conventions are more 

convenient for arithmetic terms and correspond more closely to our usual algebraic intuition for numbering 

terms. In particular, additive (multiplicative) terms are counted left to right irrespective of the associative 

groupings that may be in effect. They are treated as if they were all arguments of a single addition/subtraction 

(multiplication) operator of arbitrary arity. 

In practice, not all of the location reference features are likely to be equally useful. We provide a variety 

of traversal and search mechanisms to ensure some measure of thoroughness. Some users may choose to limit 

themselves to simple numeric indexing. 

I Table 1. Examples of location reference expressions applied to the formulas below 

LOC. reference Expr. strings I LOC. reference Expr. strings 

(! -2) 

(! -2 R) 

(! -2 R 1) 

(! -1 L 2 1) 

(! 1 R 1) 

(! -2 *) 

(! -1 L 2 *) 

(! -1 L * 1) 

r!l = 2 * x!l + 1 

2 * x!l + 1 

2 * x!l 

y! 1 

sq(x!l / 4) 

r!l, 2 * x!l + 1 

y! 1, r! 1 

x!l, y!l 

(! -1 L *) 

(! 1 R 1 **) 

x!l, r!l, y!l, r!l 

sq(x!l / 41, 

x!l / 4, x!l, 4 

r!l = 2 * x!l + 1 

2 * x!l + 1 

sq(x!l / 4) 

x!l / 4 

x!l * r!l,y!l * r!l 

{-13 

C-21 r!l = 2 * x!l + 1 

[I] sqrt(r!1) < sqrt(sq(x!l / 4)) 

x!l * r!l + y!l * r!l > r!l - 1 

I -______ 
50 Ben L. Di Vito 

4.2 Pattern Matching 

Each pattern pj in (? <ext-expr> pi . . . pn) is expressed as a text string using a specialized pattern 

language. Unlike location references, pattern matches usually produce only a text string and lack a corresponding CLOS object for a PVS expression. The patterns PI,. . . ,p, are applied in order to the textual 

representation of each member of the base expression list. In each case, matching stops after the first successful match among the {pj} is obtained. All resulting output strings are collected and concatenated into a 

single list of output strings. 

A pattern string may denote either a simple or a rich pattern. Simple patterns are easier to express and 

are expected to suffice for many everyday applications. When more precision is required, rich patterns offer 

more expressive power. 

Simple patterns allow matching against literal characters, whitespace fields, and arbitrary substrings. 

Pattern strings comprise a mixture of literal characters and meta-strings for designating text fields. Metastrings denote either whitespace or non-whitespace fields. A whitespace field is indicated by a space character 

in the pattern. A non-whitespace field is a meta-string consisting of the percent (X) character followed by a 

digit character (0-9), which matches zero or more arbitrary characters in the target string. 

Both capturing and non-capturing fields are provided. A capturing field causes the matching substring 

to be returned as an output. The meta-string %O denotes a noncapturing field, while those with nonzero 

digits are capturing fields. If a nonzero digit d is the first occurrence of d in the pattern, a new capturing 

field is thereby indicated. Otherwise, it is a reference to a previously captured field whose contents must be 

matched. Table 2 illustrates the formulation of simple patterns using this notation. 

Rich patterns follow the same basic approach as simple patterns, but add features for multiple matching 

types and multiple text-field types. The match types include full and partial string matching as well as 

top-down and bottom-up expression matching. 

Table 2. Examples of simple pattern matching applied to the formulas below 

Pattern Matching string(s) Captured fields 

1-11 

[-23 r!l = 2 * x!l + 1 

[I] sqrt(r!l) < sqrt(sq(x!1 / 4)) 

x!l * r!l + y!l * r!l > r!l - 1 

I _-_____ 

5 Higher-Order Strategies with Substitution 

Extended expressions allow us to capture subexpressions from the current sequent. Next we add a parameter 

substitution technique to formulate prover commands. To complete the suite, we add higher-order strategies 

that substitute strings and formula numbers into parameterized commands. These features are intended 

primarily for command line use. In LCF-family provers, ML scripting can achieve similar effects. 

5.1 Parameter Substitution 

A parameterized command is regarded as a template expression (actually, a Lisp form) in which embedded 

text strings and special symbols serve as substitutable parameters. The outcome of evaluating extended 
Strategy-Enhanced Interactive Proving and Arithmetic Simplification for PVS 51 

expressions is used to carry out textual and symbolic substitutions. Each descriptor computed during evaluation contains a text string and, optionally, a formula number and CLOS object. Descriptors are the source 

of substitution data while the parameterized command is its target. 

The top-level s-expression is traversed down to its leaves. Wherever a string or symbol is encountered, 

a substitution is attempted. The final command thus produced will be invoked as a prover command in 

the manner defined for the chosen higher-order strategy. (In Lisp programming terms, this process can 

be imagined as evaluating a backquote expression with specialized implicit unquoting. It also has some 

similarities to substitution in Unix shell languages as well as the scripting language Tcl.) 

Parametric variables for substitution are allowed as follows. Within literal text strings, the substrings 

%1, . . . , %9 serve as implicit text variables. The substring %I will be replaced by the string component of the 

first expression descriptor. The other %-variables will be replaced in order by the corresponding strings of 

the remaining descriptors. 

Certain reserved symbols beginning with the $ character serve as symbolic parameters. Such symbols 

are not embedded within strings as are the %-variables; they appear as stand-alone symbols within the list 

structure of the parameterized command. The symbols $1, $2, etc., represent the first, second, etc., expression 

descriptors from the list of available descriptors. 

Variants of these symbols exist to retrieve the text string, formula number, and CLOS object components 

of a descriptor. These are needed to supply arguments for built-in prover commands, which are not cognizant 

of extended expressions. The symbols $Is, $In and $1j serve this purpose. Aggregations may be obtained 

using the symbol $* and it variants. Table 3 summarizes the special symbols usable in substitutions. 

I Within this framework, we allow two classes of substitutable data: literal text strings and Lisp symbols. 

I 

I 

~ 

~ 

I 

Table 3. Special symbols for command substitution 

Symbol Value 

$1, $2, ... nth expression descriptor 

$* 

$Is, $2s, . . . nth expression string 

$*S 

$In, $2n, . . . Formula number for nth expression 

$+n 

$*n 

$lj , $2j, . . . CLOS object for nth expression 

$* j 

List of all expression descriptors 

List of all expression strings 

List of formula numbers (no duplicates) 

List of all formula numbers (includes duplicates) 

List of all CLOS objects 

I 5.2 Invocation Strategies 

I Next we describe a set of general-purpose, higher-order strategies. They are not specialized for arithmetic. 

Some offer generic capabilities useful in implementing other strategies for specific purposes. For each of these , 

I 

I 

I 

strategies, multiple expression specifications may be supplied as arguments. In such cases, each specification 

gives rise to an arbitrary number of descriptors. All descriptor lists are then concatenated to build a single 

list before substitutions are performed. Table 4 lists the strategies provided; several are discussed below. I 

invoke command &rest expr-specs 

This strategy is used to invoke command after applying substitutions extracted by evaluating the expression 

specifications expr-specs. ~ As an example, suppose formula 3 is 

I f(x!l + y!l) <= f(a!l * (z!i + 1)) , Then the command 
~ 52 Ben L. Di Vito 

Table 4. Summary of higher-order strategies 

Syntax Function 

(invoke command &rest expr-specs) Invoke command by instantiating 

(for-each command &rest expr-specs) Instantiate and invoke separately 

(f or-each-rev command &rest expr-specs) Invoke in reverse order 

(show-subst command &rest expr-specs) Show but don't invoke the 

(claim cond &opt (try-just nil) Claims condition on terms 

(name-extract name &rest expr-specs) 

from expressions and patterns 

for each expression 

instantiated command 

&rest expr-specs) 

Extract & name expr, then replace 

(invoke (case It%, <= %2") (? 3 "f(%l) <= f(%2)")) 

would apply pattern matching to formula 3 to create bindings %I= "x! 1 + y ! 1" and %2 = "a! 1 * (z! 1 + 1) It, 

which would result in the prover command 

(case "x!l + y!l <= a!l * (z!l + 1)") 

being invoked. An alternative way to achieve the same effect using location referencing is the following: 

(invoke (case "%1 <= 12") (! 3 * 1)) 

As another example, suppose we wish to hide most of the formulas in the current sequent, retaining only 

those that mention the sqrt function. We search for all formulas containing a reference to sqrt using a 

simple pattern, then collect all the formula numbers and use them to invoke the hide-all-but rule: 

(invoke (hide-all-but ($+dl (? * "sqrtll)) 

f or-each command &rest expr-specs 

This strategy is used to invoke command repeatedly, with a different substitution for each expression generated by expr-specs. The effect is equivalent to applying (invoke command e-i) n times. 

As an example, suppose we wish to expand every function in the consequent formulas having the string 

"cos" as part of its name. The following command carries this out, assuming there is only one instance per 

formula. 

(for-each (expand "%l") (! + *- ("cos") 0)) 

f or-each-rev command &rest expr-specs 

This strategy is identical to f or-each except that the expressions are taken in reverse order. 

go. This needs to be done in reverse order because formula numbers will change after each replacement. 

Imagine we wish to find all antecedent equalities and use them for replacement, hiding each one as we 

(for-each-rev (replace $In :hide? t) (! - ''='I>) 

claim cond &optional (try-just nil) &rest expr-specs 

The claim strategy is basically the same as the primitive rule case, except that the condition is derived 

using the parameterization technique. The condition presented in cond is instantiated by the terms found in 

expr-specs. Argument try-just allows the user to try proving the justification step (the second case resulting 

from the case split). 

For example, to claim that a numerical expression lies between two others, we could use something like 
Strategy-Enhanced Interactive Proving and Arithmetic Simplification for PVS 53 

I 

to generate a case split on the formula L‘a/b <= x+y & x+y <= c/d”. 

Invocation strategies are useful as building blocks for more specialized strategies that users might need 

for particular circumstances. Extended expressions can support an alternative to the more code-intensive 

strategy-writing style that requires accessing the data structures (CLOS objects) representing PVS expressions. This alternative can make lightweight strategy writing more accessible to users without a deep 

background in Lisp programming. 

6 Related Work 

Tactic-based proving was pioneered by Milner and advanced by many others, beginning with the work on 

Edinburgh LCF [ll]. The introduction of ML and its use for accessing subterms was also introduced in LCF. 

Constable and his students developed the Nuprl system [6], which included heavy reliance on tactic-based 

proof techniques. Tactic-based proving also has been used extensively in more recent interactive provers such 

as HOL [loll Isabelle [16] and Coq [12]. Although much of this has been devoted to low-level automation, 

there also have been higher level tactics developed. 

In the case of PVS, strategy development has not been as much a focus as tactic development has been 

for provers in the LCF family. Partly this is due to greater use of decision procedures in PVS as well as an 

increasing emphasis on rewrite rules. For example, Shankar [17] sketches an approach to the use of rewrite 

libraries for arithmetic simplification. While these methods are certainly helpful, we believe they need to be 

augmented by proof interaction of the sort we advocate. 

Several researchers have developed PVS strategy packages for specialized types of proving. Examples 

include a mechanization of the TRIO temporal logic [l], a proof assistant for the Duration Calculus [18], and 

the verification of simple properties for state-based requirements models [7]. A notable example is Archer’s 

account of the TAME effort [2], which has a good discussion on developing PVS strategies for timed automata 

models and using them to promote “human-style” theorem proving. 

In the area of arithmetic strategy packages for PVS, a semi-decision procedure for the field of real 

numbers [13], which had been developed originally for Coq, was recently ported to PVS. This package is called 

Field; it achieves simplification by eliminating divisions and rearranging multiplicative terms extensively. 

Field has been designed to use some Manip strategies for working with multiplication. C6sar Muiioz continues 

to enhance Field and maintains an active line of development. 

Our work on Manip emphasizes applied interactive proving, features for extracting terms from the working 

sequent, and flexible mechanisms for exploiting such terms. Many PVS strategy approaches stress control 

issues, giving less attention to the equally important data issues. Only by placing nontrivial term-access 

facilities at the user interface can the full potential of interactive strategies be realized. 

In a typical control-oriented approach, a strategy might have several plausible sets of rules to apply in 

speculative fashion. If a given try fails to produce results, bracktracking is performed and an alternative is 

attempted. By placing more emphasis on data or proof state, the strategy can determine which alternative 

to select based on attributes of the current state. Allowing users to indicate relevant terms from the sequent 

sharpens the focus even further during interactive proving. 

Currently under study are term access features that allow selection by mouse gestures. “Proof by pointing” 

techniques [3] are examples of applicable methods that can improve usability in this area. Once selected, a 

term can be matched with an extended expression for locating it. This can be done without burdening the 

user to derive the extended expression. 

7 Conclusion 

The Manip arithmetic package has been used experimentally at NASA Langley and made available to the 

PVS user community. Along with Field [13], it is now being used to prove new lemmas as they are introduced 

in Langley’s PVS libraries [14]. Proofs for the real analysis and vectors libraries, in particular, have made 

regular use of Manip strategies. As of May 2003, a total of 325 Manip strategy instances were counted in the 
54 Ben L. Di Vito 

proofs distributed as part of the Langley libraries. Further evaluation is needed to gauge effectiveness and 

suggest new strategies. 

Tactic-based theorem proving still holds substantial promise for automating domain-specific reasoning. 

In the case of PVS, much effort has gone into developing decision procedures and rewrite rule capabilities. 

While these are undoubtedly valuable, there is still ample room for other advances, particularly those that 

can leverage the accumulated knowledge of experienced users of deduction systems. Such users are well poised 

to introduce the wide variety of deductive middleware needed by the formal methods and computational 

logic communities. Our tools and techniques aim to further this goal. 

Future activities will focus on refining the techniques and introducing new strategy packages for additional 

domains. One domain of interest is reasoning about sets, especially finite sets. We expect that ideas from 

the arithmetic strategies can be readily adapted. 

Acknowledgments 

The need for this package and many initial ideas on its operation were inspired by Ricky Butler of NASA 

Langley. Additional ideas and useful suggestions have come from C&ar Muiioz of NIA, and John Rushby 

and Sam Owre of SRI. 

References 

1. A. Alborghetti, A. Gargantini, and A. Morzenti. Providing automated support to deductive analysis of time 

critical systems. In Proc. of the 6th European Software Engineering Conf. (ESEC/FSE’97), volume 1301 of 

LNCS, pages 221-226, 1997. 

2. Myla Archer. TAME: Using PVS strategies for special-purpose theorem proving. Annals of Mathematics and 

Artificial Intelligence, 29( 1-4):139-181, 2000. 

3. Y. Bertot, G. Kahn, and L. ThCry. Proof by pointing. In Proc. of Theoretical Aspects of Computer Software 

(TACS’94), volume 789 of LNCS, 1994. 

4. R.W. Butler, V. Carreiio, G. Dowek, and C. Muiioz. Formal verification of conflict detection algorithms. In 

Proceedings of the 1 lth Working Conference on Correct Hardware Design and Verification Methods CHARME 

2001, volume 2144 of LNCS, pages 403-417, Livingston, Scotland, UK, 2001. 

5. Victor Carreiio and CCsar Mufioz. Aircraft trajectory modeling and alerting algorithm verification. In Theorem 

Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000, pages 90-105, 2000. 

6. R. L. Constable and et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 

1986. 

7. Ben L. Di Vito. High-automation proofs for properties of requirements models. Software Tools for Technology 

Transfer, 3(1):20-31, September 2000. 

8. Ben L. Di Vito. A PVS prover strategy package for common manipulations. NASA Technical Memorandum 

NASA/TM-2002-211647, April 2002. 

9. Ben L. Di Vito. Manip User’s Manual, Version 1.1, February 2003. Complete package available through NASA 

Langley PVS library page [14]. 

10. M. J. C. Gordon and T. F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher-Order 

Logic. Cambridge University Press, 1993. 

11. M. J. C. Gordon, R. Milner, and C. P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation. Springer 

LNCS 78, 1979. 

12. INRIA. The Coq Proof Assistant Reference Manual, Version 7.1, October 2001. 

13. C. Muiioz and M. Mayero. Real automation in the field. NASA/CR-2001-211271 Interim ICASE Report No. 39, 

December 2001. 

14. NASA Langley PVS library collection. Theories and proofs available at 

http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS2-library/pvslib.html. 

15. Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von Henke. Formal verification for fault-tolerant 

architectures: Prolegomena to the design of PVS. IEEE Ransactions on Software Engineering, 21(2):107-125, 

February 1995. 

16. L. C. Paulson. Isabelle: A Generic Theorem Prover. Springer LNCS 828, 1994. 

17. N. Shankar. Arithmetic simplification in PVS. Final Report for SRI Project 6464, Task 15; NASA Langley 

contract number NAS1-20334., December 2000. 

18. J. Skakkebaek and N. Shankar. Towards a duration calculus proof assistant in PVS. In Third Intern. School and 

Symp. on Formal Techniques in Real Time and Fault Tolerant Systems, volume 863 of LNCS, 1994. 
Strategy-Enhanced Interactive Proving and Arithmetic Simplification for PVS 55 

A Algebraic Manipulation Strategies 

The following list summarizes the set of manipulation strategies. A few variants have been omitted in the 

interest of brevity. 

Syntax Function 

(swap lhs operator rhs &opt (infix? T)) x o y * yo x 

(group term1 operator term2 term3 

&opt (side L) (infix? TI) R: (x o y) o t z 0 (y 0 z) 

(swap-group term1 operator term2 term3 L: z o (y o z) & y o (x o t) 

&opt (side L) (infix? TI) R: (zoy)ot~(xoz)oy 

(swap-re1 &rest fnums) Swap sides and reverse relations 

(equate lhs rhs &opt (try-just nil)) . . . Zhs.. . & . . . rhs.. . 

(has-sign term &opt Claims term has sign indicated 

(sign +) (try-just nil)) 

(mult-by fnums term &opt (sign +)) Multiply both sides by term 

(div-by fnums term &opt (sign +)I Divide both sides by term 

(split-ineq fnum &opt (replace? nil)) Split 5 (2) into < (>) and = cases 

(flip-ineq fnums &opt (hide? TI) Negate and move inequalities 

(move-terms fnum side 

(isolate fnum side term-num) 

(isolate-replace fnum side term-num 

&opt (targets *)) 

(cancel &opt (fnums *) (sign nil)) Cancel terms from both sides 

(cancel-terms &opt (fnums *) (end L) 

(op-ident fnum &opt 

(cross-mult &opt (fnums *)) Multiply both sides by denom. 

(cross-add &opt (fnums *)) Add subtrahend to both sides 

(factor fnums &opt (side *) 

(transform-both fnum transform 

L: zo(yoz)*(xoy)ot 

Move additive terms to other side 

Move all but one term 

Isolate then replace with equation 

&opt (term-nums *I) 

Cancel speculatively & defer proof 

Apply operator identity to rewrite 

(sign nil) (try-just nil)) 

(side L) (operation *1)) expression 

Extract common multiplicative factors 

Apply transform to both 

(term-nums *) (id? nil)) from additive terms given 

&opt (swap nil) (try-just nil)) sides of formula 

(permute-mult fnums &opt (side R) 

(term-nums 2) (end L)) 

(name-mult name fnum side 

&opt (term-nums *)) 

(recip-mult fnums side) 

(isolate-mult fnum &opt (side L) 

(mult-eq rel-fnum eq-fnum 

&opt (sign +)) 

(mult-ineq fnuml fnum2 

&opt (signs (+ +)I) 

(mult-cases fnum 

&opt (abs? nil) (mult-op *1)) 

(mult-extract name fnum &opt 

(term-num 1) (sign +)I 

(side *) (term-nums *)) 

Rearrange factors in a product 

Select factors, assign name to 

x/d * z * (l/d) 

Select a factor and divide both 

both sides to isolate factor 

Multiply sides of relation by 

sides of equality 

Multiply sides of inequality by 

sides of another inequality 

Generate case analyses for products 

their product, then replace 

Extract selected terms, name 

replace them, then simplify 
First-Order Proof Tactics in Higher-Order Logic Theorem Provers 

Joe Hurd* 

Computer Laboratory 

University of Cambridge, 

joe.hurd0cl.cam.ac.uk 

Abstract. In this paper we evaluate the effectiveness of first-order proof procedures when used as 

tactics for proving subgoals in a higher-order logic interactive theorem prover. We first motivate why 

such first-order proof tactics are useful, and then describe the core integrating technology: an ‘LCFstyle’ logical kernel for clausal first-order logic. This allows the choice of different logical mappings 

between higher-order logic and first-order logic to be used depending on the subgoal, and also enables 

several different first-order proof procedures to cooperate on constructing the proof. This work was 

carried out using the HOL4 theorem prover; we comment on the ease of transferring the technology to 

other higher-order logic theorem provers. 

1 Introduction 

Performing interactive proof in the HOL theorem prover [12] involves reducing goals to simpler subgoals. It 

turns out that many of these subgoals can be efficiently ‘finished off’ by an automatic first-order prover. To 

fill this niche, Harrison implemented a version of the MESON procedure [13] with the ability to translate 

proofs to higher-order logic. The original MESON procedure, due to Loveland [17], is a sound and complete 

calculus for finding proofs in full first-order logic. This was integrated as a HOL tactic in 1996, and has 

since become a standard workhorse of interactive proof. Today, building all the theories in the most recent 

distribution of HOL4l relies on MESON to prove 1726 subgoals; the HOL formalization of probability theory, 

including an example verification of the Miller-Rabin primality test, contributes another 1953 subgoals to 

this total. 

The primary goal of this paper is to evaluate the effectiveness of different first-order proof calculi for 

use as HOL tactics supporting interactive proof. We compare the performance of several first-order calculi 

on three different problem sets: the TPTP first-order problem set; and two problem sets derived from HOL 

subgoals proved by MESON. The TPTP (Thousands of Problems for Theorem Provers) problem set is a 

collection of first-order problems designed to test the limits of current automatic first-order provers [24]. 

This experiment allows us to directly compare the performance of the first-order proof procedures in the 

different environments of fully automatic proof of deep theorems and supporting a user engaged in driving an 

interactive theorem prover. In this paper we show that performance in these two environments is correlated. 

Therefore, if a new first-order prover is developed that can prove more TPTP problems than the existing 

state of the art, we can expect the same prover to prove more HOL subgoals, thus improving the user 

experience. 

The most obvious difference between the fully-automatic and interactive environments is the real-time 

nature of interactive proof. Whether the cost of proof search is incurred each time the theory is loaded, 

compiled, or even just once when the theory is created, the user usually requires any HOL tactic to respond 

(almost) immediately. By contrast, fully automatic provers are generally judged on the number of theorems 

that they can prove within a much more relaxed time-limit. To simulate this environmental difference in 

our experiments, for the TPTP problem set we allow the provers 60 seconds per problem, and for the HOL 

problem sets we allow only 5 seconds per problem. 

A limit of 5 seconds per problem suggests that the performance of a prover may be rather sensitive to 

the characteristics of initial proof search. Following this reasoning, it seems plausible that a combination 

of different proof procedures may perform better than any individual, on the grounds that any problems 

* This work was supported by EPSRC project GR/R27105/01 

HOL4 is available at http: //hol. sf .net/. 
First-Order Proof Tactics in Higher-Order Logic Theorem Provers 57 

I that are ‘shallow’ for one of the procedures may be quickly solved within the time limit. We therefore 

implement a proof procedure that combines resolution, model elimination, and the Delta preprocessor. All 

three procedures may be run in parallel (using time slicing), and they cooperate by sharing unit clauses.2 It 

turns out that not only does this combination procedure significantly outperform each individual procedure 

The device that allows the provers to share unit clauses is a small ‘LCF-style’ kernel for clausal first-order 

logic. As well as providing a convenient mechanism for detecting unib clauses derived by model elimination, 

it also provides a convenient place to install the proof recording in the event that it is necessary to translate 

them to HOL. In particular, it is the only place that needs to worry about keeping track of proofs, and this 

enabled broader experimentation with the first-order provers. 

Since HOL4 is written in Standard ML, this is a convenient implementation language for our experiment, 

though in the past similar experiments have been performed by making calls to external C provers [14]. 

Therefore, this paper also provides a view of implementing first-order proof procedures in a functional 

programming language, and some interesting aspects of this are brought out in discussion. 

The secondary goal of this paper is to serve as a ‘HOW-TO guide’ for would-be implementors of first-order 

proof tactics in higher-order theorem provers. We will present all the steps necessary to prove higher-order 

subgoals using automatic first-order provers: the initial conversion from higher-order subgoal to first-order 

clauses; the first-order proof search; and the final translation of the first-order refutation to a higher-order 

logic theorem. 

I 

I on the HOL problem sets, but also on the TPTP problem set. 1 

I 

The main contributions of this paper are as follows: I 

- A relative performace comparison of different first-order proof calculi in the two environments of proving 

deep first-order theorems (the TPTP problem set) and aiding the user engaged in interactive proof (the 

two problem sets extracted from HOL subgoals). 

- A combination resolution and model elimination procedure that performs significantly better than either 

individually, in both the TPTP and the HOL environments. 

- A detailed description of how to implement tactics for proving higher-order logic subgoals using first-order 

proof procedures. 

The paper is structured as follows: in Section 2 we point out the interesting features of the mapping 

between higher-order and first-order logic; Section 3 examines the syntactic differences between the problem 

sets and presents our evaluation methodology; in Section 4 we describe the ML implementation of the 

first-order provers and their subsequent optimization; Section 5 presents the results of running different 

combinations of provers on the problem sets; Section 6 comments on how this technology might be ported 

to other higher-order logic theorem provers; and finally in Sections 7 and 8 we conclude and take a look at 

I 

1 related work. 

2 The HOL Interface to First-Order Logic 

1 This is the high-level view of how we prove the HOL goal g using a first-order prover: 

1. We first convert the negation of g to conjunctive normal form; this results in a HOL theorem of the form 

I where each ci is a HOL term having the form of a disjunction of literals, and may contain variables from 

the vectors a and wi. 

I 2. Next, we map each HOL term ci to first-order logic, producing the clause set 

c = {CI,. . . 

3. The first-order prover runs on C, and finds a refutation p. I 

Unit clauses are clauses with only one literal, and are used to simplify other clauses. 
58 Joe Hurd 

4. By proof translation, the refutation p is lifted to a HOL proof of the theorem 

5. Finally, some HOL primitive inferences use theorems (1) and (2) to derive 

In the following subsections we examine the translation of formulas and proofs between higher-order 

logic and first-order logic, which plays a role in steps 2 and 4 of the above process. Much of this information 

appears in a previously published system description [15]; it is reproduced here because it is an essential 

part of our framework for creating first-order proof tactics. 

Before getting into the details, we first give an extended example of the whole process with a typical 

HOL subgoal that we prove using a first-order proof tactic. Consider the subgoal 

Vx, y, z. divides 2 y j divides x (z * y) (4) 

where the predicate divides is defined as 

t Vx,y,z. divides x y @ 32. y = z *x (5) 

To prove the subgoal, we also need the following theorems about multiplication: 

t vx, y. x * y = y * x 

I- vz,y,z. (z *y) *z = z * (y * 2) 

The user invokes the first-order proof tactic on the subgoal (4), passing as arguments the definition (5) 

and theorems (6) and (7). Initially, the first-order proof tactic uses the arguments to set up the equivalent 

subgoal g: 

(5) A (6) A (7) * (4) 

The next step is to negate g and convert to conjunctive normal form. This conversion is completely standardnegation normal form followed by pushing out quantifiers and Skolemization-and we refer the interested 

reader to a textbook such as Chang and Lee [6] for more details. In our example, this results in the theorem 

t1g e 

3 a, b, c, d. 

(Vx,y.x*y=y*x) A 

(Vz,y,z. (z * y) * z = x * (y * z)) A 

(Vz, y, z. ~(y = z * z) V divides x y) A 

(Vx, y. ldivides x y V y = d 2 y * x) A 

divides a b A 

ldivides a (c * b) 

We map each line of this formula to a first-order clause. The existential variables a, b, c, d are mapped to 

first-order function symbols, and the universal variables x, y, z are mapped to first-order variables. The firstorder prover runs, finds a refutation, and this is translated to a HOL theorem from which the first-order 

tactic derives k g, thus proving the initial goal. 

2.1 

Seemingly the hardest problem with mapping HOL terms to first-order logic-dealing with A-abstractionscan be smoothly dealt with as part of the conversion to CNF. Any A-abstraction at or beneath the literal level 

Mapping HOL Terms to First-Order Logic 
First-Order Proof Tactics in Higher-Order Logic Theorem Provers 59 

is rewritten to combinatory form, using the set of combinators {S, K, I, C, 0). Using this set of combinators 

prevents the exponential blow-up that is encountered when only {S, K, I} are used [25].3 

The mapping that we use makes explicit function application, so that the HOL term m + n maps to the 

first-order term @(@(+, m), n). Since in HOL there is no distinction between terms and formulas, we model 

this in first-order logic by defining a special relation called B (short for Boolean) that converts a first-order 

term to a first-order formula. For example, the HOL boolean term m 5 n is mapped to the first-order 

formula B(@(@(<,m),n)). The only exception to this rule is equality: the HOL term 2 = y is mapped to 

the first-order logic formula =(z, y). 

As described thus far, this mapping is used to generate the uHOL first-order problem set from HOL 

subgoals sent to MESON. uHOL stands for untyped HOL, because no type information is included in this 

representation. However, we also experimented with including higher-order logic types in the first-order 

mapping of a HOL term. Using this idea, the HOL term m + n would map to the first-order term 

I @(@( + : N + N + N, m : N) : N + N, n) : N 

where ':' is a binary function symbol (written infix for readability), and higher-order logic types are encoded 

as first-order terms.4 This mapping is used to produce the HOL problem set from HOL subgoals. As might be 

expected, this produces much larger first-order clauses than omitting the types, and this results in first-order 

harmful: the extra information may pay for itself by cutting down the search space. This hypothesis is 

t 

I deduction steps taking longer to perform. However, we cannot conclude that including types is definitely 

I examined in Section 5. 

1 

i 2.2 Translating First-Order Refutations to HOL 

When the first-order prover has found a refutation of a set of clauses, the HOL tactic must translate the 

refutation to a HOL theorem, thus ensuring that no soundness bugs in the first-order prover are propagated 

into HOL. At first sight it may appear that the necessity of translating first-order refutations to higher-order 

logic proofs imposes a burden that hampers free experimentation with the first-order provers. However, 

by applying the logical kernel idea of the LCF project [ll], we can make the proof translation invisible 

to the developer of first-order proof procedures, leaving him free to experiment with new calculi. We have 

implemented this automatic proof translation for both the mapping with type information and the one 

without, and they have been successfully used to prove many HOL subgoals. 

~ 

AXIOM [Ai,. . . , A1 V...VAn 

I 

INST u Ai V...VAn 

AI[O] V...VAn[o] 

ASSUME L LVTL 

FACTOR AiV...VAn 

Ai, V ... V Ai, 

I Fig. 1. The Primitive Rules of Inference of Clausal First-Order Logic. 

I This is achieved by defining a logical kernel of ML functions that execute a primitive set of deduction 

rules on first-order clauses. For our purposes, we only need the five rules in Figure 1. 

The AXIOM rule is used to create a new axiom of the logical system; it takes as argument the list of 

literals in the axiom clause. The ASSUME rule takes a literal L and returns the theorem L V 1L.5 The INST 

In principle we could use more combinators to guarantee an even more compact translation, but HOL goals are 

normally small enough that this extra complication is not worth the effort. 

Encoding type variables as first-order logic variables allows polymorphic types to be dealt with in a straightforward 

manner. 

This rule is used to keep track of reductions in the model elimination procedure. 

, 

I 
60 Joe Hurd 

rule takes a substitution u and a theorem A, and applies the substitution to every literal in A.6 The FACTOR 

rule takes a theorem and removes duplicate literals in the clause: note that no variable instantiation takes 

place here, two literals must be identical for one to be removed. Finally, the RESOLVE rule takes a literal 

L and two theorems A, B, and creates a theorem containing every literal except L from A and every literal 

except 1L from B. Again, no variable instantiation takes place here: only literals identical to L in A (or 1L 

in B) are removed. 

These five primitive rules define a (refutation) complete proof system for clausal first-order logic. To see 

this, recall that a complete proof system results from FACTOR and RESOLVE rules that perform unification [6]. 

However, we can simulate these rules by first instantiating appropriately using the INST rule, and then 

applying our identical-match versions FACTOR and RESOLVE. 

signature Kernel 

sig 

type formula = 

type subst = 

(* An ABSTRACT 

eqtype thm 

(* Destruction 

Val dest-thm : 

Term. f ormula 

Term. subst 

type for theorems *) 

of theorems is fine *) 

thm -> formula list 

(* But creation is only allowed by these primitive rules *) 

Val AXIOM : formula list -> thm 

Val ASSUME : formula -> thm 

Val INST : subst -> thm -> thm 

Val FACTOR : thm -> thm 

Val RESOLVE : formula -> thm -> thm -> thm 

end 

Fig. 2. The ML Signature of a Logical Kernel Implementing Clausal First-Order Logic 

The ML type system can be used to ensure that these primitive rules of inference represent the only way 

to create elements of an abstract thm type.7 In Figure 2 we show the signature of an ML Kernel module 

that implements the logical kernel. We insist that the programmer of a first-order provers derive refutations 

by creating an empty clause of type thm. The only way to do this is to use the primitive rules of inference 

in the Kernel module: this is both easy and efficient for all the standard first-order proof procedures. 

At this point it is simple to translate first-order refutations to HOL proofs. We add proof logs into the 

representation of theorems in the Kernel, so that each theorem remembers the primitive rule and theorems 

that were used to create it. When we complete a refutation, we therefore have a chain of proof steps starting 

at the empty clause and leading back to axioms. In addition, for each primitive rule of inference in Kernel, 

we create a higher-order logic version that works on HOL terms, substitutions and theorems. The final 

ingredient needed to translate a proof is a HOL theorem corresponding to each of the first-order axioms. 

These theorems are the HOL clauses in the CNF representation of the original (negated) goal, which we 

mapped to first-order logic and axiomatized. 

To summarize: by requiring the programmer of a first-order proof procedure to derive refutations using 

a logical kernel, lifting these refutations to HOL proofs can be done completely automatically. 

In some presentations of logic, this uniform instantiation of variables in a theorem is called specialization. 

Indeed, the ability to define an abstract theorem type was the original reason that the ML type system was created. 
First-Order Proof Tactics in Higher-Order Logic Theorem Provers 61 

2.3 

Using the mapping in Section 2.1, we can use a first-order prover to prove some higher-order HOL goals, 

such as the classic derivation of an identity function from combinator theory: 

The Scope of a First-Order Prover for HOL 

k (VX,~. K x y = X) A (Vf,g,X. S fgz = (f Z) (92)) =+ If. VZ. f~ = x 

Similarly, the framework for translating refutations in Section 2.2 is general enough to translate any 

first-order theorem to HOL. Therefore, we can use a first-order prover to solve for HOL terms satisfying a 

set of HOL formulas, just as Prolog does for Horn formulas.* 

However, our method of embedding higher-order in first-order logic is not without danger. The whole 

reason for adding types to higher-order logic is to avoid the Russell paradox, and so if we choose to remove 

them in our translation we must beware of unsoundness. Defining a ‘Russell combinator’ R as 

R = (AX. T(Z x)) = S (K (1)) (S I I) 

we find that we can use the reduction rules for S and K to prove 

R R = ’(R R) 

and thus derive a contradiction. 

Of course, a first-order refutation that is unsound in this way cannot be successfully translated to a HOL 

proof. It is therefore trivial to discover any problems that occur due to the lack of type information in the 

first-order representation. When unsoundness is discovered, the subgoal is simply tried again with the type 

information included. Fortunately, this phenomenon occurs in less than 1% of all HOL subgoals. 

3 Problem Sets and Evaluation Methodology 

In the next section we describe the ML implementation of our combination of first-order provers. To evaluate 

and compare different procedures, we use the following three problem sets: 

TPTP This consists of all the problems classified as ‘unsatisfiable’ in version 2.4.1 of TPTP.’ 

uHOL This problem set consists of all subgoals proved by MESON when building: the standard theories 

included with version Kananaskis-0 of the HOL4 theorem prover; the HOL formalization of probability 

theory; and the example verification of the Miller-&bin primality test.” The HOL subgoals are mapped 

to first-order logic without type information (uHOL = untyped HOL). 

HOL The same problem 

information included. 

set as uHOL, but the HOL subgoals are mapped to first-order logic with type 

Table 1. Profiles of the Problem Sets. 

Set I N C L S L/C S/C S/L 

TPTP I 2752 31.0 65.0 229.0 2.07 8.17 4.00 

uHOL 3679 11.0 19.0 146.0 1.78 12.86 7.14 

HOL 3679 11.0 19.0 701.0 1.78 63.71 35.30 

Table 1 profiles the three problem sets. For each problem set, we show the number of problems (N), and 

the median of several statistics for each problem: number of clauses (C), number of literals (L), number 

The model elimination procedure has the capability to solve for terms in this way. 

The TPTP problem set is available at http: //m. cs .miami .edu/-tptp/. 

lo Available at http: //mu. cl. cam. ac.uk/~jeh1004/research/problems/. 
62 Joe Hurd 

of symbols" (S), mean literals per clause (L/C), mean symbols per clause (S/C), and mean symbols per 

literal (S/L). 

Comparing the TPTP and HOL problem sets, it can be seen that the average TPTP problem has more 

clauses, while the average HOL problem has more symbols per literal. However, by looking at the uHOL row, 

it is apparent that most of the symbols in the HOL problems come from type information. One similarity 

between all three problem sets is the average number of literals per clause: around two. 

As previously mentioned, we allow 60 seconds per TPTP problem and 5 seconds per HOL problem, to 

simulate the difference in requirements between fully automatic and interactive proof. All experiments were 

run on Athlon 1.4GHz processors with at least 512Mb of memory, using version 2.00 of Moscow ML12 on 

RedHat Linux 7.1. 

So that we can use statistical methods to compare the first-order provers, we randomly split each problem 

set into 10 equally sized sections. By counting the number of problems in each section that any two provers 

solve within the time limit, we can use the t-test to compute the statistical significance that one prover is 

better than the other [9]. Here is an example results table where we compare two hypothetical provers, foo 

and bar: 

foo bar 

Since we do not compare provers with themselves, the diagonal entries are marked with *. The 99.5% in 

the upper right entry means that foo is statistically better than bar with 99.5% confidence. The t95 above 

this means that, over the whole problem set, foo proved 95 problems that bar could not. The lower left 

entry in the table means that bar is not significantly better than foo, but it did prove 7 problems that foo 

could not. 

4 Implementing the First-Order Provers 

In Sections 2 and 3 we presented a mechanism for mapping HOL subgoals to first-order problems and a way to 

evaluate first-order provers. In this section we will describe an ML implementation of a collection of first-order 

proof procedures, using our evaluation method to select optimum parameters and justify optimizations. 

Since the literature contains such an abundance of strategies and techniques for first-order proof, it was 

necessary to select just a few for the purpose of our present experiment. In particular, we do not treat 

equality at all, and add equality axioms as part of our mapping to first-order logic. However, in the future 

there is nothing to stop us including more sophisticated methods for handling equality, say by adding a 

PARAMODULATION primitive inference rule. 

4.1 Model Elimination Procedure 

The first proof procedure that we implement is the model elimination procedure of Loveland [17]; our prover 

is essentially a ground-up reimplementation of Harrison's MESON [13], incorporating some optimizations of 

Astrachan, Loveland and Stickel [2,3]. 

Our strategy is to first produce a naive implemention, and then incrementally optimize it. The starting 

point is a version of model elimination called m-0 that treats every input clause as an initial clause. A 

clause must contain at least one negative literal for m-1 to treat it as initial, and initial clauses in m-n must 

contain all negative literals. 

Building upon m-n, we add ancestor pruning to get m-a, and then ancestor cutting to get m-x. Ancestor 

cutting means that if the negation of an ancestor exactly matches the current goal, we do a reduction on 

that ancestor and disallow backtracking. Incorporating Harrison's divide-and-conquer search strategy brings 

l1 By symbols we mean variables, functions, relations and logical connectives. 

l2 Moscow ML is available at http://ww.dina.dk/-sestoft/mosml.html. 
First-Order Proof Tactics in Higher-Order Logic Theorem Provers 63 

us to m-d, and trying to match the goal from the clause set before trying unification is called rn-s.l3 The 

optimization in m-c is slightly dubious, incorporating a limited form of caching to stop us attempting the 

same goal twice from a given point in the search. The overhead of this pays off on the TPTP problem set 

with a time limit of 60 seconds, but not on the HOL problem sets where the limit is 5 seconds. 

Finally, m-u incorporates unit lemmaizing, where the use of a unit lemma contributes size 1 to the proof. 

Since we use iterative deepening to search for proofs in order of size, the penalty of using a unit lemma is an 

important factor in the optimization. However, we cannot make the penalty depend on the proof size of the 

unit lemma, since later we will import unit lemmas from a resolution prover where proof sizes do not play 

any part. 

Table 2. Comparing Model Elimination Optimizations on the TPTP Problem Set. 

m-u 

m-c 

m- s 

m-d 

m-x 

m-a 

m-n 

m- 1 

m-0 

m-u m-c m-s m-d m-x m-a m-n m-1 m-0 +89 +91 +99 +180 +186 +198 +345 +371 

+13 +2 +14 +lo3 +lo9 +121 +269 +295 

+13 +O +13 +lo1 +lo7 +119 +267 +293 

+9 +o +1 +90 +96 +lo8 +255 +281 

+12 +11 +11 +12 +7 +25 +178 +204 

+12 +11 +11 +12 +1 4-19 +174 +ZOO 

+158 +184 

+29 

* 99.5% 99.5% 99.5% 99.5% 99.5% 99.5% 99.5% 99.5% 

- * 80.0% 97.5% 99.5% 99.5% 99.5% 99.5% 99.5% 

* 95.0% 99.5% 99.5% 99.5% 99.5% 99.5% 

* 99.5% 99.5% 99.5% 99.5% 99.5% 

* 95.0% 99.5% 99.5% 99.5% 

* 97.5% 99.5% 99.5% 

* 99.5% 99.5% 

* 99.5% 

-- 

--- 

---- 

----- 

+5 +4 +4 +5 +o +o 

+o +o +o +o +1 +3 +6 

+o +o +o +o +1 +3 +6 +3 

------ 

------- 

- - - - - - - - * 

Table 2 shows the result of a pairwise comparison between each step in the evolution of our model 

elimination prover, from the humble m-0 to the hi-tech m-u which proves 371 more TPTP problems. 

Similar results occur on the HOL problem sets. 

4.2 Resolution Procedure 

The second proof procedure that we implemented is the resolution procedure of Robinson 1211. Our version uses the given clause algorithm, and we implement term nets to improve the speed of unification and 

subsumption checking. Additionally, unit clauses are used whenever possible to simplify clauses. In contrast 

with the incremental sequence of optimizations that we used for model elimination, our resolution procedure 

has several independent parameters that control the search strategy. 

The first parameter controls how much subsumption checking is done. By default, as clauses are taken 

from the unused list they are checked to see if they are subsumed by a clause in the used list. If so, they are 

dropped and the next clause is chosen from the unused list. We also implement a higher level of subsumption, 

indicated by an extra s in the prover name. Here, when we lift a clause from the unused list, we immediately 

see if it is subsumed by another clause in the unused list. If so, we use that clause instead. 

The second parameter is a number n, and controls the order that we pick clauses from the unused list. 

For every clause picked from the unused list in FIFO order, we pick n clauses with the smallest symbol 

count.14 The number n is one of 1, 2, 3, 4 or 5, and is part of the prover name. This is called the ratio 

strategy, originally used in the Otter theorem prover [as]. 

l3 The fact that we are implementing this in ML might help to explain why this is such an effective optimization. If 

matching succeeds then there is no need to update the substitution context, and this results in less allocation and 

reduced garbage collection times. These reductions range between 20% and 80% on TPTP problems. 

l4 We efficiently implement this alternation in ML by storing unused clauses as both queues and (leftist) heaps. 

Okasaki [18] implements functional versions of these and many more data structures. 
64 Joe Hurd 

The final parameter is Robinson’s positive refinement [20], which we indicate with a final ‘+’ in the prover 

name. 

We found that the best prover for all three problem sets is r3+: the default level of subsumption; picking 

3 smallest clauses for every clause at the head of the queue; and using positive resolution. On the TPTP 

problem set, this parameter setting is better than any other with confidence at least 95%. 

4.3 Delta-style Procedure 

The third and final proof procedure that we implemented is based on the Delta preprocessor of Schumann [23]. 

Put simply, for every wary relation R present in the problem, we generate the ‘Delta goals’ R(X1, . . . , X,) 

and -d?(Yl ’...,Y,) (with fresh variables Xi and yi). We then use the model elimination procedure with 

iterative deepening to search for solutions to the Delta goals. Every unit clause that is derived during this 

process is shared with the other proof procedures. 

The Delta procedure takes the same optimization parameters as model elimination, and so it is not 

necessary to separately optimize this procedure. In any case, since it is not designed to directly solve the 

goal, but rather to help the other procedures by finding useful unit clauses, it only makes sense to use it 

when unit lemmaizing is switched on. 

5 Combining the First-Order Provers 

As already mentioned, when we run different proof procedures together they can cooperate by sharing unit 

clauses. Whenever a unit clause is derived, it is inserted into a global store that is available to every proof 

procedure. The way that the individual proof procedures make use of unit clauses was described in the 

previous sections. 

Each proof procedure runs for a time-slice,15 and a scheduler decides which proof procedure to run based 

on the cost of the execution time it has already consumed. For model elimination and resolution, the cost of 

execution time is simply the number of seconds, but for the Delta procedure it was empirically found to be 

better to use the square of the number of seconds. 

For example, if each proof procedure has consumed 1/3 second of CPU time, the model elimination and 

resolution cost is 1/3, while the Delta cost is (1/3)2 = 1/9. Therefore, Delta will be scheduled as the cheapest 

procedure. If each proof procedure has consumed 2 seconds, the model elimination and resolution cost is 2, 

while the Delta cost is 22 = 4, and so one of model elimination and resolution will be scheduled to run for a 

time-slice. 

Table 3. Comparing Combinations of Provers on the TPTP Problem Set. 

md m1 

mrd mr md m rd r 4-22 +160 +200 +291 +322 * 99.5% 99.5% 99.5% 99.5% 99.5% 

* 99.5% 99.5% 99.5% 99.5% 

* 99.5% 99.5% 99.5% 

* 99.5% 99.5% 

* 99.5% 

+161 +189 +283 +307 +9 

+22 +36 +56 +274 +298 

+13 +15 +7 +243 +264 

+25 +30 +146 +164 

+25 +23 +139 +154 +11 

- 

-- 

--- 

---- +42 

--__-- * 

Tables 3,4, and 5 show the result of running different proof procedure combinations on the TPTP, uHOL 

and HOL problem sets, respectively. 

l5 In our experiments we set each time slice to be 1/3 second long. 
First-Order Proof Tactics in Higher-Order Logic Theorem Provers 65 

mrd 

Table 4. Comparing Combinations of Provers on the uHOL Problem Set. 

mrd mr md m rd r +16 +111 +187 +164 +148 * 70.0% 99.5% 99.5% 99.5% 99.5% 

mr 

md 

m 

rd 

r 

+119 +182 +I56 +137 * 99.5% 99.5% 99.5% 99.5% 

* 99.5% 97.5% 90.0% 

+13 

+11 +22 +91 +152 +133 

- 

-- 

+14 +12 +18 +133 +113 --- * -- +21 +16 +lo9 +163 +33 --- 90.0% * - +22 +14 +lo7 +160 +50 --- 99.0% 90.0% * 

Table 5. Comparing Combinations of Provers on the HOL Problem Set. 

- 

mrd 

mr 

md 

m 

rd 

r 

mrd 

* 

+22 

95.0% 

+25 

+23 

- 

+14 

- +32 

mr md m rd +9 +171 +246 +174 

- 99.5% 99.5% 99.5% 

+184 +258 +184 

+lo2 +I68 

+22 +25 +146 *- 

* 99.5% 99.5% 99.5% 

- * 99.5% 75.0% +25 

-- 

4-11 4-154 +‘09 -- 99.5% * +23 +175 +233 +85 

- 99.5% 99.5% 99.5% 

r 

99.5% 

99.5% 

+127 

+131 

+124 

+lo5 

- 

- +20 

* 

I In every case, the combined model elimination and resolution procedure performed significantly better 

than either individually, with the highest level of confidence (99.5%). For the TPTP problem set, we can use 

some arithmetic to see that there must exist at least 166 problems that were proved by the combined procedure but were not proved by either acting alone. This is compelling evidence that the combined procedure 

does more than simply harvest the problems that are ‘shallow’ for one of model elimination and resolution. 

Rather, the sharing of unit clauses creates a whole new procedure that is better than either. 

Comparing the combinations of proof procedures across the three problem sets, as we move from TPTP 

through uHOL to HOL we find resolution becoming better relative to model elimination. Similarly, the Delta 

procedure helps the combined procedure less as we move from TPTP to HOL. This latter effect is probably 

due to the cost functions we chose, which favours Delta in the first 3 seconds of CPU time. When the total 

limit is 5 seconds, this represents a serious bias. 

Because the proof procedures share unit clauses, some rather counter-intuitive effects can arise from 

combining proof procedures. For example, there is a class of 7 TPTP problems that model elimination can 

prove, but model elimination and Delta together fail to prove within 60 seconds. One of these is GRP128-4-003, 

which model elimination acting alone proves in about 12 seconds! The only explanation is that Delta finds 

some ‘helpful’ unit clauses that lead model elimination into an unprofitable area of the search space. However, 

these kind of events are rare: the other 6 problems in this class take model elimination acting alone more 

than 45 seconds to prove. 

Finally, we can compare the performance of provers on the different versions of each problem in the 

uHOL and HOL problem sets. The best prover in this domain is the combination of model elimination and 

resolution, and there were 142 problems that it could prove in uHOL but not in HOL, and 13 problems that 

it could prove in HOL but not in uHOL. Therefore, this confirms our expectations that the much smaller 

versions of the problems in uHOL can be proved more efficiently, though there are a few examples where 

the types cut down the search space enough to make the difference between finding a proof within the time 

limit and not. 

I 

, 

I 

j 

I 
66 Joe Hurd 

6 Transferring the Technology to Other Higher-Order Logic Theorem Provers 

The results of the previous section show that we can create combination first-order proof tactics that are 

more powerful than individual proof procedures, and the LCF-style logical kernel allows us to easily translate 

first-order refutations to higher-order logic theorems. The existing implementation in HOL4 has been found 

to be a useful proof tool when used in proofs by the HOL developers. 

The general architecture is easily ported to other higher-order logic theorem provers such as PVS or 

Isabelle. Indeed, the first-order proof procedures complete with logical kernel are a standalone library in 

Standard ML, so could be imported without any change at a11.16 The only part that needs to be created 

afresh for each higher-order logic theorem prover is a rule of inference that translates first-order refutations 

to higher-order logic theorems. This will differ slightly according to the particular details of the higher-order 

logic. 

There is one difference between HOL and PVS that may be significant here. When translating a first-order 

refutation to higher-order logic, it is often necessary to translate a first-order term to higher-order logic. In 

HOL this is straightforward, but in PVS some auxiliary theorems may be necessary to establish the TCCs 

of the translated term. Additionally, there may be no type information in the first-order term, in which case 

we generate a HOL term and infer its principal type. In PVS this may not be possible in general, which 

may jeopardize the possibility of an untyped mapping to first-order logic. More investigation is necessary to 

establish whether the required information can be reconstructed in some way. 

Finally, for some interactive theorem proving applications, it may be appropriate to simply trust that 

the subgoal is valid if the first-order prover detects unsatisfiability of the corresponding clauses. There is 

already strong pressure on the implementors of first-order provers to make sure their system is sound; at the 

annual CADE automatic system competition, provers face disqualification if they fail any soundness test. 

Abandoning the idea of translating refutations gives an additional benefit: many first-order provers perform 

much better if they are not required to keep track of the refutation as they search. 

7 Conclusions 

In this paper we described a framework for implementing first-order proof tactics in higher-order logic 

theorem provers, which uses an LCF-style logical kernel to create a modular interface between the two 

logics. The architecture we presented is not specific to a particular higher-order theorem prover, and we 

have sketched out how it could be ported to a new theorem prover, notwithstanding the potential problem 

with type reconstruction in PVS. We have implemented a version in HOL4, with two working mappings: one 

that preserves type information from higher-order logic, and one that reconstructs it while translating the 

first-order refutation. 

We also implemented a combination of first-order proof procedures in Standard ML, and compared their 

performance on three different problem sets. Based on our experiments, we tentatively conclude that good 

performance from a first-order prover in one domain suggests that it will also perform well in other domains. 

Optimizations we made to improve performance on the TPTP problem set usually also improved performance 

on the HOL problem sets, though there was a significant shift from model elimination in the TPTP domain 

towards resolution in the HOL domain. This was extremely surprising, since the HOL problems are selfselected for the MESON prover in HOL. During interactive proof in HOL, if MESON cannot prove a subgoal 

within a reasonable time, then a user can perform a manual inference step and then try again. Further 

investigation is needed to establish why resolution seems to do better on HOL subgoals. 

We found the LCF-style kernel for clausal first-order logic to be more than just a convenient interface to 

a proof translator. Reducing the steps of proof procedures to primitive inferences clarified their behaviour, 

and also helped catch bugs early. Also, assuming the (52 line) ML Kernel module is correctly implemented 

and the programmer is careful about asserting axioms, loss of soundness arising from 'prover optimizations' 

can be completely avoided. 

Finally, on all three problem sets the combination of model elimination and resolution was found to 

perform significantly better than either individually. This supports the hypothesis that first-order search 

l6 Available at http: //vuv. cl. cam. ac .uk/'Jeh1004/research/metis/. 
First-Order Proof Tactics in Higher-Order Logic Theorem Provers 67 

spaces have a structure that rewards the use of a variety of search methods, despite the extra redundancy 

that is entailed; a view neatly summarized by Astrachan and Loveland [2]: 

“Unlike chess, theorems are a very diverse lot and different proof methods may excel in different 

areas.” 

8 Related Work 

In addition to MESON in HOL, there are many other examples of automatic first-order provers being used 

to prove problems in an interactive theorem prover: (in chronological order) FAUST in HOL [16]; SEDUCT 

in LAMBDA [5]; 3TAP in KIV [l]; Paulson’s blast in Isabelle [19]; Gandalf in HOL [14]; and Bliksem in 

Coq [4]. Various mappings are used from the theorem prover subgoals into problems of first-order logic, 

defining the scope of what can be automatically proved. Using the architecture presented in this paper for 

translating first-order refutations would allow different first-order provers to be ‘plugged-in’ to the theorem 

prover. Moreover, if first-order provers emitted proofs in a standardized ‘LCF-style’ logical kernel for clausal 

first-order logic, then this would further simplify their integration into interactive theorem provers. 

As part of the ILF Mathematical Library Project, Dahn and Wernhard [8] extracted 97 first-order problems from the article Boolean Properties of Sets in the MIZAR Mathematical Library. Later, Dahn [7] added 

the ability to represent MIZAR type information, and extracted 47 problems from the article Relations Defined on Sets. However, there has been no published study of the comparitive effectiveness of first-order 

provers on this problem set. 

Several projects have aimed to create combination first-order provers that are better than the individual 

components. For example, the TECHS system [lo] uses automatic referees to decide which clauses to exchange 

between provers, as opposed to our system that simply shares unit clauses. Further investigation is needed 

to decide the best way of combining proof procedures in our application. 

Finally, we note that Robinson [22] proposed a version of higher-order logic in terms of combinators 

(though it is typeless and therefore unsound due to the ‘Russell combinator’ we defined in Section 2.3).17 

However, the motivation behind combinators instead of the A-calculus is that proof automation can be 

simplified, and this also motivates our combinator mapping from HOL subgoals to first-order logic. 

Acknowledgements 

This project greatly benefitted from discussions with Mike Gordon, Michael Norrish and Konrad Slind. 

Also, the CAML code in John Harrison’s forthcoming book provided a useful starting point for my own ML 

implementation of first-order provers. Thanks are also due to Judita Preiss for technical support. 

References 

1. Wolfgang Ahrendt, Bernhard Beckert , Reiner Hahnle, Wolfram Menzel, Wolfgang Reif, Gerhard Schellhorn, and 

Peter H. Schmitt. Integration of automated and interactive theorem proving. In W. Bibel and P. Schmitt, editors, 

Automated Deduction: A Basis for Applications, volume 11, chapter 4, pages 97-116. Kluwer, 1998. 

2. 0. L. Astrachan and Donald W. Loveland. The use of lemmas in the model elimination procedure. Journal of 

Automated Reasoning, 19(1):117-141, August 1997. 

3. Owen L. Astrachan and Mark E. Stickel. Caching and lemmaizing in model elimination theorem provers. In 

Deepak Kapur, editor, Proceedings of the 1 lth International Conference on Automated Deduction (CADE-1 l), 

volume 607 of Lecture Notes in Artificial Intelligence, pages 224-238, Saratoga Springs, NY, USA, June 1992. 

Springer. 

4. Marc Bezem, Dimitri Hendriks, and Hans de Nivelle. Automated proof construction in type theory using resolution. In David A. McAllester, editor, Proceedings of the 17th International Conference on Automated Deduction 

(CADE-17), volume 1831 of Lecture Notes in Computer Science, pages 148-163, Pittsburgh, PA, USA, June 

2000. Springer. 

l7 Thanks to John Harrison for drawing my attention to this. 
68 Joe Hurd 

5. H. Busch. First-order automation for higher-order-logic theorem proving. In Tom Melham and Juanito Camilleri, 

editors, Higher Order Logic Theorem Proving and Its Applications, 7th International Workshop, volume 859 of 

Lecture Notes in Computer Science, Valletta, Malta, September 1994. Springer. 

6. Chin-Liang Chang and Richard Char-Tung Lee. Symbolic Logic and Mechanical Theorem Proving. Academic 

Press, New York, 1973. 

7. Ingo Dahn. Interpretation of a Mizar-like logic in first-order logic. In Ricardo Caferra and Gernot Salzer, editors, 

International Workshop on First-Order Theorem Proving (FTP '98), Technical Report E1852-GS-981, pages 

116-126, Vienna, Austria, November 1998. Technische Universitat Wien. 

8. Ingo Dahn and Christoph Wernhard. First order proof problems extracted from an article in the MIZAR mathematical library. In Maria Paola Bonacina and Ulrich Furbach, editors, International Workshop on First-Order 

Theorem Proving (FTP '97), number 97-50 in RISC-Linz Report Series, Schloss Hagenberg, Austria, October 

1997. Johannes Kepler Universitat Linz. 

9. Morris DeGroot. Probability and Statistics. Addison-Wesley, 2nd edition, 1989. 

10. Jorg Denzinger and Dirk Fuchs. Knowledge-based cooperation between theorem provers by TECHS. SEKI-Report 

SR-97-11, University of Kaiserslautern, 1997. 

11. M. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF, volume 78 of Lecture Notes in Computer Science. 

Springer, 1979. 

12. M. J. C. Gordon and T. F. Melham. Introduction to HOL (A theorem-proving environment for higher order 

logic). Cambridge University Press, 1993. 

13. John Harrison. Optimizing proof search in model elimination. In Michael A. McRobbie and John K. Slaney, 

editors, 13th International Conference on Automated Deduction (CADE-13), volume 1104 of Lecture Notes in 

Artificial Intelligence, pages 313-327, New Brunswick, NJ, USA, July 1996. Springer. 

14. Joe Hurd. Integrating Gandalf and HOL. In Yves Bertot, Gilles Dowek, AndrC Hirschowitz, Christine Paulin, 

and Laurent Thkry, editors, Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs 

'99, volume 1690 of Lecture Notes in Computer Science, pages 311-321, Nice, France, September 1999. Springer. 

15. Joe Hurd. An LCF-style interface between HOL and first-order logic. In Andrei Voronkov, editor, Proceedings 

of the 18th International Conference on Automated Deduction (CADE-18), volume 2392 of Lecture Notes in 

Artificial Intelligence, pages 134-138, Copenhagen, Denmark, July 2002. Springer. 

16. R. Kumar, T. Kropf, and K. Schneider. Integrating a first-order automatic prover in the HOL environment. In 

Myla Archer, Jeffrey J. Joyce, Karl N. Levitt, and Phillip J. Windley, editors, Proceedings ofthe 1991 International 

Workshop on the HOL Theorem Proving System and its Applications (HOL '91), August 1991, pages 170-176, 

Davis, CA, USA, 1992. IEEE Computer Society Press. 

17. Donald W. Loveland. Mechanical theorem proving by model elimination. Journal of the ACM, 15(2):236-251, 

April 1968. 

18. Chris Okasaki. Purely Functional Data Structures. Cambridge University Press, Cambridge, UK, 1998. 

19. L. C. Paulson. A generic tableau prover and its integration with Isabelle. Journal of Universal Computer Science, 

20. J. A. Robinson. Automatic deduction with hyper-resolution. International Journal of Computer Mathematics, 

21. J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23-49, 

22. J. A. Robinson. A note on mechanizing higher order logic. Machine Intelligence, 5:121-135, 1970. 

23. Johann Ph. Schumann. DELTA - A bottom-up processor for top-down theorem provers (system abstract). In 

Alan Bundy, editor, 12th International Conference on Automated Deduction (CA DE-12), volume 814 of Lecture 

Notes in Artificial Intelligence, Nancy, France, June 1994. Springer. 

24. Christian B. Suttner and Geoff Sutcliffe. The TPTP problem library - v2.1.0. Technical Report JCU-CS-97/8, 

Department of Computer Science, James Cook University, December 1997. 

25. D. A, Turner. A new implementation technique for applicative languages. Software - Practice and Experience, 

26. Larry Wos, Ross Overbeek, Ewing Lusk, and Jim Boyle. Automated Reasoning: Introduction and Applications. 

5(3), March 1999. 

1:227-234, 1965. 

January 1965. 

9(1):31-49, January 1979. 

McGraw-Hill, New York, 2nd edition, 1992. 
Coq Tacticals and PVS Strategies: 

I A Small Step Semantics * 

Florent Kirchner 

Ecole Normale SupCrieure de Cachan, France 

florent.kirchnerBinria.fr ; fkirchneBnianet.org 

Abstract. The need for a small step semantics and more generally for a thorough documentation and 

understanding of Coq’s tacticals and PVS’s strategies arise with their growing use and the progressive 

uncovering of their subtleties. The purpose of the following study is to provide a simple and clear formal 

framework to describe their detailed semantics, and highlight their differences and similarities. 

! 1 Introduction 

I Procedural proof languages are used to prove propositions with the assistance of a proof engine: the user 

wields the language to give the theorem prover instructions or tactics on the way to proceed throughout the 

proof. The instruction set roughly corresponds to the elementary steps of the formal logic inherent to the 

prover; a proof script is a collection of such instructions. The need for a way to express the proof scripts in 

a more sophisticated and factorized way emerges as soon as proofs get more complicated, resulting in very 

large proof scripts of elementary steps. This makes any proof reading or maintenance operation tedious if not 

impossible. Both Coq [l] and PVS [ll], derived from the LCF theorem prover, introduce proof combinators 

1 

l 

I in their proof language to powerfully compose elementary proof tactics: tactids in Coq, strategies in PVS’ . Though other provers such as Isabelle and NuPrl also implement tacticals, they have not been included in I 

this work but a similar reasonning could probably apply. The following sections expose the semantics of the 

~ tacticals of Coq and PVS, using a small steps semantics and some appropriate structures and notations. 

1 2 Conventions and Structures 

, Coq and PVS, as most procedural theorem provers, usually implement a goal oriented proof style. That is, 

given a proof goal and an elementary logical rule, the prover applies the logical rule backwards to the goal, 

yielding a set of potentially simpler subgoals. For example, given the proof goal r I- 0 5 X A X 5 1, the Coq 

instruction htro ((split) in PVS) generates the subgoals r t- 0 5 X and r I- X 5 1. This corresponds to 

the application of the logical rule: 

I 

-- I 

A-intro . At-B At-C 

At-BAC 

In turn, some new rules are applied to the new subgoals, and the process stops when all the subgoals are 

which is called here the proof context. Goals, i.e., sets of formulas of the form AI,. . . ,A, !- B1,. . . , B,, are 

commonly named sequents. 

, refined enough to be trivially proven true. This repetition creates an arborescent structure of subgoals, 1 

I 

I 

I 2.1 The Proof Context 

, The proof context is considered here as a collection of sequents organized in a tree of sequents, its leaves 

representing the sequents that are currently to be proven. A leaf, when modified by some command, becomes 

the parent of the sequents created by this command: the nodes of the tree of sequents are the “old” sequents. 

* This work was supported by INRIA FUTURS and the National Institute of Aerospace (under NASA Cooperative I 

, Agreement NCC-1-02043). 

Henceforth, when refering to the combinators in general, the name tactical will be used. 
70 Florent Kirchner 

Thus, the tree of sequents keeps track of the proof progression. Incidentally, one has to consider the number 

of features that are related to the proof context (state of the proof, proven branches, goal numbering, etc.). 

Hence the semantics is made much clearer by blending a simplified object-oriented structure with the tree 

representation. This way, the proof context, the sequents, and the formulas are considered as non mutable 

objects including attributes, which correspond to their features, and functions or methods that read or modify 

these attributes and eventually return a new object. For instance, one of the attributes of the proof context 

object is the tree of sequent objects. Furthermore, a sequent object has a set of formula objects as attribute. 

Let us now define some notations. A sequent is represented as r I- A, where F is the antecedent and A 

is the consequent, each being a list of formulas2. Latin letters A, B, etc. represent individual formulas. We 

write O.m(3) for the invocation of the method m of object 0 with the list of parameters 5. The objects 

here are non mutable, meaning that methods modifying an object return a new object. Thus, a method call 

0. m(3) is a synonym for the function call m(?,O), and the objects could also be seen as records. The letter 

T denotes a proof context object; we distinguish a few particular proof contexts: 

- T is a proof context that is completely proven. 

- 1, stands for a failed proof context. The integer n codes for an “error level”, i.e., an indicator of the 

propagation range of the error. Errors are raised by tacticals and tactics, when they are called in an 

inappropriate situation (i.e., when none of the reduction rules of our semantics apply3). 

- And 0 is the empty proof context, i.e., a proof context object hosting an empty tree. 

The equality test between a context and an empty, proven or failed context is the only equality test between 

contexts we authorize in our semantics. 

The description of the attributes and methods of T is as follows. 

- Attributes: 

0 T. seq-tree: the tree of sequents. 

0 T. active: pointer to the active subtree of sequents, i.e., the subtree on which the next command will 

take effect. In case it is a leaf, then T. active represents a sequent r k A, and we will write: T. r t- A 

to refer to such a proof context. 

0 T. progress: this is a flag raised when the tree of sequents has gone through changes. Basically, when 

a tactic successfully applies, it raises the progress flag ; it is reseted by a specific, “Break”, command. 

0 T. addLeaves(r1 t- AI,. . . , r, t- An): this method applies when the active attribute points to a leaf 

it adds n leaves to the tree. In the new tree, the new sequents G k Ai, i E (1,. . . , n}, will be leaves, 

and the former active leaf of the old tree will become their common parent node. 

0 ~.lowerPointer(i): moves the active pointer down (towards the root) in the tree, i 2 0 being the 

depth of the move. 

0 T. raisePointerToLeaf(): moves the pointer up to the first (i.e., innermost leftmost) unproven leaf of 

the tree. 

0 ~.pointNextSibling(): moves the pointer to the closest unproven leaf, sibling of the active sequent. 

If there is no such sibling, the pointer is set to a default empty value, which is represented by the 

method returning the empty proof context 0. 

0 T. setProgress(b): sets the corresponding flag to b. 

0 T. hasProgressed(): returns the value of the progress flag. 

0 T. setLeafProven0: the active leaves, that is, the leaves of the active subtree, are labeled as proven. 

0 ~.isActiveTFeeProven(): returns true if all the leaves in the active subtree are labeled as proven, 

- Methods: 

If there are no unproven sequents left, the proof is finished (i.e., T. setLeafProven() = T). 

false otherwise. 

The semantics presented in this paper does not distinguish between sequents with permuted formulas. This limitation is not problematic since we focus on tacticals, which do not require formula-level knowledge. But it should 

be addressed if a detailed semantics of the tactics, in addition to the semantics of tacticals, was to be considered. 

The error system is a bit more complicated than this, especially in Coq. But this simplification is a valid, understandable approximation of the provers’ behaviour. 
Coq Tactic 1s and PVS Strategies: A Small Step Sem ntics 71 

, The sequent and formula objects are illustrated in Fig. 1, which also provides some type information. The 

figure uses the UML formalism where a class notation is a rectangle divided into three parts: class name, 

attributes, and methods. The diamond end arrow represents an aggregation, that is, a relation “is part of”. 

The types presented here are basic and purely informative. 

Sequents Tree 

seqfree: tree of Sequent 

progress: bool 

active: tree of Sequent 

addLeaves(z1 , .. . , zn : Sequent ): Sequents Tree 

lowerPointer(i : int ): Sequents Tree 

raisePointerToLeaf0: Sequents Tree 

pointNextSibling(): Sequents Tree 

setProgress(boo1 ): Sequents Tree 

hasProgressed(): bool 

setLeafProven(): Sequents Tree 

isActiveTreeProven0: bool 

I 

Seauent 1 

r: set of Formula 

A: set of Formula 

proven: bool 

Formula 

Fig. 1. Proof context objects 

2.2 The Proof Script 

Given a set of tactics and of tacticals, a proof script is built by combining tactics with tacticals. For instance, 

in Coq, with the Intro and Assumption tactics, and the tactical “F, one can build the proof script Intro ; 

denote proof scripts. 

The distinction between tactics and tacticals within the proof language is somewhat fuzzy, as they both 

modify the proof context object. Here we consider that the tactics are the elements of the proof language 

that attempt to modify the tree of sequents, by adding leaves to it. For example, in PVS, the (split) tactic 

applied to the sequent A I- B A C behaves as the A-intro logical rule, adding two leaves A I- B and A I- C 

to the sequent tree. Thus the sequent tree 

AI-BAC 

I Assumption. Such a proof script applies to a proof context r. We use p,p‘ to designate tactics and e, e’ to 

is transformed into the sequent tree 

AI-B At-C 

AI-BAC 

The tacticals represent the proof language’s control structures. In our semantics, they do not modify 

the tree of sequents directly but rather reduce into simpler proof scripts, and possibly modify some other 

I 
72 Florent Kirchner 

attributes of the proof context. For instance in PVS, assuming a non-failed non-proven context r, the proof 

script (if nil (fail) (split)), formed of the tactical if and the two tactics (split) and (fail), evaluates in the (split) tactic: 

(if nil (fail) (split)) /r i (split) /T . 

The actual modification of the proof context is performed by (split). 

In these examples the difference between tactics and tacticals appears quite clear, but we also note that 

the definition of a tactical implies the manipulation of tactics. Because of this dependency, the presentation 

of the semantics of the tacticals needs to be parameterized by the computation rule for tactics. 

3 The Semantic Framework 

The notion of small step or reduction semantics was introduced by Plotkin [9] in 1981. It consists in a set of 

rewriting rules specifying the elementary steps of the computation, within a context. The idea behind the 

present formalism is to use the reduction semantics of the imperative part of Objective ML, popularized by 

Wright and Felleisen [12], as an inspiration to deal with the interactions between the proof language and the 

proof context. 

As exposed in the previous section, the reduction rules for the tacticals are dependent on the way tactics 

are applied to proof contexts. The semantics of the tacticals is parametrized by that of the tactics. Hence 

a formal definition of a tactic application is needed before any semantic rules are given. Since tactics, when 

evaluated, modify the tree of sequents, we consider them as expressions which modify the proof context. A 

tactic p applied to a proof context T returns another proof context r’: 

p%r=r’ . 

The exact instanciations of this functional definition are of course system specific, and will be exposed in 

sections 4 and 5. 

Tacticals are combinators, therefore their evaluation within a proof script should return either a simpler 

proof script or a tactic. We denote this returned expression by e‘. The reduction of tacticals can also modify 

the proof context r, thus a reduction rule in our semantics will look like: 

e/rie’/r’, 

where denotes a head reduction (i.e., reduction of the head redex). These rules are conditionnal rewriting 

rules, with the tactics’ computation function as a possible parameter. For example, the Coq tactical ‘‘? 

applies its first argument to the current goal and then its second argument to all the subgoals generated. 

If the first argument proves the current goal or fails, applying another proof script to that failed or proven 

proof context does not make any sense, and the second argument is neglected : 

111 ; e2 / r i e2 / (~1%07) if Vn (v%r) # I, 

and -(w,%r). isActiveTreeProven() , 

111 ; e2 / r i 01 / r if 3n (vl%r) = I, 

or (vI%r). isActiveTreeProven() . 

The context rule 

allows processing a proof script on which no head reduction applies. The definitions of the detailed reduction 

rules as well as that of the grammar of the context E depend highly on the language, and will be presented 

in the later prover-specific sections. 

Finally, the values of our semantics consist, for each language, in the set of its components we do not 

wish to reduce. Thus they will be defined as the subset of each languages that are tactics, augmented, in the 

case of Coq, by the recursively defined functional and recursive operations (see section 4.2). 
Coq Tacticals and PVS Strategies: A Small Step Semantics 73 

Note that this definition of the reduction semantics of the tacticals produces, when all tacticals have 

been reduced, something like 0 / T as a final result. This is unsatisfying since we would like to see this final 

tactic v applied to T (as in 0%~). Hence the use, for each langage, of a “Break” command that does this 

final evaluation. 

4 coq 

In Coq the tactical commands are defined as an independent language, called Ctac4. Delahaye [4] gives the 

definition of this language and an informal big step semantics5. 

4.1 Syntax 

Let us define the syntax of a Coq proof script: 

e ::= 

And 

expr ::= 

I 

I 

I 

I 

I 

I 

I 

I 

I 

I 

I 

I 

I 

I 

I 

I 

I 

I 

I 

I 

I 

I 

expr. all expressions must end with “.” . 

X identifiers 

P tactic 

k integer (Cta,-specific) 

t Coq term 

Fun x -D e 

Rec 21 22 -D e 

(el e2) 

Let x1 = el And . . .And x, = e, In e 

Match t With ([ti] -D ei)?==, 

Match Context With ([hpi k pi] -D ei)?!=, 

el Orelse e2 

Do k e 

Repeat e 

Progress e 

First [el I . . . le,] 

Solve [el I . . . le,] 

Tactic Definition x e 

Meta Definition x e 

Recursive Tactic Definition 5 e 

Recursive Meta Definition z e 

e 

el ; e2 

eo ; [ell.. . le,] . 

4.2 Semantics 

The values of the semantics are defined as: 

2, ::= p 

I Fun x --(re 

I Rec XI 22 +. e . 

Ctac also includes some commands that correspond to our definition of tactics, which we will see later; and some 

miscellaneous features that will not be presented in this paper. 

Whereas a small step semantics is defined by a set of reduction rules that apply within a reduction context, a big 

step semantics directly links an expression with its normal form. 
74 Florent Kirchner 

The reduction rules for the tacticals follow. 

Applications These simply correspond to the @-reduction rules of the A-calculus. 

(Fun z 4 e)(w) / T -% e[z tl w] / T . 

(Rec f z 4 e)(w) / T 4 e[z w v][f H (Rec f z 4 e)] / T . 

Local variable binding The xi are bound to the values vi in the expression e. The bindings are not 

mutually dependent. 

Let 21 = v1 And . . .And z, = w, In e / T e[zl tlv1,. . . ,x, H v,] / T . 

Term matching This tactical matches a Coq term with a series of patterns, and return the appropriate 

expression, properly instanciated. 

Let @ be the binary operator defined as: 

ale1 @ 02e2 / T + 2rl / T 

-+ v2 1 T 

+ Idtac / T otherwise. 

if the substitution 01 is defined 

and ulel / T evaluates in vl; 

else, if 02 is defined 

and 02e2 / T evaluates in v2; 

For all i E {l, . . . , n), (T~,++~ is the substitution resulting from the matching of t by pi (undefined if pi 

does not match t ; matching by - always succeds and yields the empty substitution). 

The reduction rule then is: 

Match t With ([pi] 4 ei)r=l / T ffpi++t ei / . 

Context matching This tactical matches the current goal with a series of patterns, and returns the appropriate expression, properly instanciated. The order of the patterns is not significant ; since Coq uses 

constructive logic, the consequent A is limited to a single formula B. 

The original Coq rule allows for multiple antecedent patterns, which is a simple nesting of the presented 

form: 

Match Context With ([hpi I- pi] --(r ei)y==l / T. (. . . Aj . . . I- B) & 

ffhpitiAjff;,+.,~ ez / 7 . 

If this does not succeed then the context progression rule is used instead: 

Match Context With ([hpi I- pi] 4 ei)Y==, / T. (. . . Aj . . . I- B) & 

Match Context With ([hpi I- pi] 4 ei)r=l / T. (. . . A,-1 . . . I- B) . 

Break The break command ‘.’ triggers the evaluation of the tactics and then resets some parameters in the 

proof context before the application of the next proof script: 

v. / T 4 (v%T). raisePointerToLeaf0. setProgress(fa1se) . 

Sequence The sequential application of two tactics: v2 is applied to all the subgoals generated by vl. This 

is the basic example of the use of conditional rules in conjunction with the % relation. 

vl ; e2 / T 4 e2 / (w~%T) iftln 2 o (01%~) # I, 

and ~(v1 %T). isActiveTreeProven() , 

v1 ; e2 / T i v1 / T if 3n 2 o (wl%T) = I, 

or (w1 %T). isActiveTreeProven() . 
Coq Tacticals and PVS Strategies: A Small Step Semantics 75 

N-ary sequence First applies vo and then each of the vi to one of the subgoals generated. The definition 

of this command uses an additional operator, 7, to allow potential backtracking. 

00; [el 1 . . . le,] / T Fel,. . . , e, / (00%~). raisePointerToLeaf0 

if Vn 2 0 (00%~) # I, 

and ~(vo%T). isActiveTreeProven() 

00; [ell.. . le,] / T i 00 / T 

if 3n 2 0 (00%~) = I, 

or (00%~). isActiveTreeProven() , 

and 

- 

;Tu1, e2 . . . , e, / T, 

;TW, e2 . . . , e, / 7’ 

7e2,. . . , e, / (01 %T’). pointNextSibling0 

(Fail 0) / T 

70, / 7’ i (Fail 0) / T 

70, / 7’ i Idtac / (w,%T’). lowerPointer(1) 

if Vn 2 0 (01%~’) # I, , 

if 3n 2 0 ( wl %T’) = I, , 

if T’= 0 

- 

or (v,%T’). pointNextSibling() # 0 , 

and (v,%T’). pointNextSibling() = 0 . 

if 7’2 0 

Branching This tactical tests whether the application of 01 fails or does not progress, in which case it 

applies 02. 

01 Orelse e2 / T i e2 / T 

01 Orelse e2 / T i 01 / T 

if (01%~) = I, 

or ~(01%~). hasProgressed() , 

if (01%~) =# I, 

and (01 %T). hasProgressed() . 

Progression The progression test. Fails if its argument does not make any change to the current proof 

context. 

Progress v / T i 

Progress 0 / T 

/ T if (0%~). hasProgressed() , 

(Fail 0) / T if ~(II%T). hasProgressed() . 

Iteration Here k is a primitive integer, only used in This tactical repeats v, lc times, along all the 

branches of the sequent subtree. Here again we introduce an additional operator E. 

Doke/Ta(Kke)/T , 

with 

- 

Do 0 e / T 

(Do, k v) / T 

Idtac / T 

(E (k - 1) e) / (0%~) 

if Vn 2 0 (0%~) # I, 

and ~(o%T). isActiveTreeProven0 

if3n 2 0 (0%~) = I, 

or (0%~). isActiveTreeProven() . 

(Do, k 0) /T i w /T 
76 Florent Kirchner 

Indefinite iteration This is the indefinite version of the previous iteration. It stops when all the applications of v fail. As for the previous finite iteration, notice the additional operator R.epeat,. 

Repeat e / r Repeat, e / r , 

with 

Repeat, v / r 

Repeat, v / r 4 v / r 

Repeat, v / 7 4 Repeat, e / (v%r) 

Idtac / r if 3n 2 0 (v%r) = I, 

if (21%~). isActiveTreeProven() 

if Vn 2 0 (v%r) # I, 

and i(v%r). isActiveTreeProven() , 

Catch The Try tactical catches errors of level 0, and decreases the level of other errors by 1. 

Try v / r & Idtac / r 

Try v / r & [Fail (n - l)] / r 

Try v / r 

if (v%r) = LO 

if 3n > 0 (v%r) = lo 

v / r if Vn 2 0 (v%r) # lo . 

First tactic to succeed Applies the first tactic that does not fail. It fails if all of its arguments fail. 

First [ ] / T 4 (Fail 0) / r 

First [vlleal.. . IVn] / 7 i w1 / T 

First [wllezl.. . le,] / T 4 First [e21 . . . le,] / T 

if Vn 2 0 (211%~) # I, 

if 3n 2 0 (v,%r) = I, . 

First tactic to solve Applies the first tactic that solves the current goal. It fails if none of its arguments 

qualify. 

Solve [I /r 4 Fail 0 /T 

Solve [vllezl . . . le,] / r 

Solve [v1 le21 . . . Iv,] / r i Solve [e21 . . . le,] / r 

v1 / r if (vl%r). isActiveTreeProven() 

if ~(v1 %r). isActiveTreeProven() . 

4.3 Toplevel Definitions 

The semantics of the user-defined tactics and tacticals requires an extension of the meta-notation. Let M be 

a memory state object with its two trivial methods newTactical(name, description) and getTactical(name). 

M. newTactical(z, e) -+ M{z tl e} , 

if z e Dom(M). 

M. getTactical(z) + M(z) . 

The declaration of new commands simply writes: 

(Recursive) Tactic Definition z := v / r 4 M. newTactical(z, v) / r , 

(Recursive) Meta Definition z := t / r M. newTactical(z, t) / r , 

where the “Recursive” tag is optional. 

will be tried: 

Thus when evaluating an expression on which none of the previous reduction rules apply, the following 

/ r --% M. getTactical(z) / r . 
Coq Tacticals and PVS Strategies: A Small Step Semantics 77 

4.4 Context 

The evaluation context is defined as: 

E ::= [] 

I E. 

EelvE 

Let z = E In e 

E Orelse e I v Orelse E 

E;e I v;E 

FE I ;7E,e2,. . . ,en 

Do, n E 

I Repeat, E 

I Progress E 

I Match E With (pi --+ ei)y==l 

1 First[Ele21.. . le,] 

1 Solve[Ele21.. . le,] 

1 Tactic Definition z := E I Meta Definition z := E 

I Recursive Tactic Definition z := E 

I Recursive Meta Definition z := E . 

- 

I Try E 

4.5 Tactics 

The goal of this section is not to give the semantics for all the tactics but rather to demonstrate on a few 

specific examples how the application of simple tactics to a proof context can be expressed. 

In general tactics apply to a sequent tree, but will be exposed here only the case where T. active designates 

a leaf. When the pointer designates a subtree, the tactic is simultaneously applied to all the unproven leaves 

of this subtree. 

The following equations define partial functions, they are extended to complete functions by taking the failed 

proof context IO as a return value for any undefined point. 

Intro%T. r I- (x : A)B = T. addLeafs (r, (5 : A) I- B). setProgess(true) . 

Clear 2%~. T, (z : A) I- B = T. addLeafs (T I- B). setProgess(true) , 

with V(xi : Ai) E r .z Ai. 

Assumption%T. r, (z : A) I- A' = T. setLeafF'roven(). setProgess(true) , 

with A and A' unifiable. 

Cut A%T. r I- B = T. addLeafs (r I- (z : A) . B, r I- A). setProgess(true) . 

The identity was introduced in [4] as a tactical, but it behaves as a tactic: 

Idtac%.r = 7 , 

The same holds for the error command: 

(Fail n)%~ = I, . 
78 Florent Kirchner 

5 PVS 

PVS tactics and strategies are thoroughly described in [8] and [6], but as far as we know, there is no published 

small-step semantics of the strategy language. 

5.1 Syntax 

Here is the syntax of the subset of PVS’s tactics that will be considered: not all of PVS’s strategies are 

exposed here; those that appear are believed to be the most significant ones, the others being either special 

cases or slight variants of the aforementionned. 

Contrary to Coq, there is no symbol in PVS to mark the end of the proof command. This problem is 

dealt with by using a special symbol (8): 

e ::= expr I all expressions must end with “7” 

And 

expr::= x identifier 

IP tactic 

It Lisp term 

I (if t el ez> 

I (let ((21 tl). . . (2, t,)) e) 

I (try el e2 e31 

I (repeat e> 

I (repeat* e> 

I (spread eo (el. . .e,)> 

I (branch eo (el. . .e,>> 

I (try-branch eo (el.. .e,> e,+l) 

5.2 Semantics 

There are no abstraction strategies in PVS therefore the values are defined as the tactics: 

v ::= p . 

The reduction rules for the tacticals follow. 

Break triggers the evaluation of the tactics and does the final proof context parameter reset: 

8 / T (‘u%T). raisePointerToLeaf(). setProgress(fa1se) . 

Lisp conditional A lisp argument t is evaluated to determine whether the first or the second tactic argument is applied. 

(if t el ez) /~4e2 /T 

(if t el ez> /~4el /T 

ift=nil 

ift#nil . 

Lisp variable binding The local variable binding strategy. The symbols xi are bound to the lisp expressions ti in the latter bindings and in e. 
Coq Tacticals and PVS Strategies: A Small Step Semantics 79 

Backtracking This strategy combines a branching facility triggered by the progress condition, with an error 

catching functionnality. It applies v1 to the current goal, it this shows a progress then it applies v2, else 

it applies v3. Moreover, if 02 fails then this strategy returns (skip). This final backtracking feature calls 

for the use of an additional operator try,. 

Remark that the sequencial tactical then is simply defined as (then v1 v2) = (try v1 w2 v2). 

(try v1 e2 e3) / T (try, e2) / (w1%?-) if (VI%?-). hasProgressed() 

and Vn 2 0 (VI%?-) # I, 

and l(v1 %?-). isActiveTreeProven() 

if 3n 2 0 (211%~) = I, 

if ~(v1 %?-). hasProgressed() 

(try v1 e2 e3) / ?- i (fail) / T 

(try 01 e2 e3) / ?- 

(try 211 e2 e3) / ?- 

e3 / ?- 

/ ?- if (VI %T) . isActiveTreeProven(), 

with 

I (try, W) / 7’ --% ‘U / 7’ 

(try, v) / ?-’ i (skip) / ?- 

if Vn 2 0 (‘u%?-’) # I, 

if 3n 2 o (v%?-’) = I, 

I Indefinite iteration The tactic argument is applied to the current goal, if it generates any subgoals then 

it is recursively applied to the first of these subgoals. The repetition stops when an application of the 

tactic has no effect. 

(repeat e) / T i repeat, e / T , 

with 

repeat, w / ?- 

repeat, v / ?- i v / ?- 

repeat, w / ?- A repeat, e / (&I-). raisePointerToLeaf0 

Idtac / ?- if 3n 2 0 (21%~) = I, 

if (21%~). isActiveTreeProven() 

if Vn 2 0 (v%?-) # I, 

and l(v%?-). isActiveTreeProven() , 

Like repeat, repeat* repeats v, but on all the previously generated subgoals. 

~ 

(repeat* e) / T i repeat*, e / ?- , 

with 

repeat*, w / ?- 

repeat*, v / ?- i v / T 

repeat*, v / ?- i repeat*, e / (u%?-) 

(skip) / ?- if 3n 2 0 (v%T) = I, 

if (w%?-). isActiveTreeProven() 

if Vn 2 0 (w%?-) # I, 

and l(w%?-). isActiveTreeProven() , 

I 

I N-ary sequence The N-ary sequence in PVS is similar to that of Coq, but here the number of generated 

I subgoals need not be exactly n. 

(spread wo (el.. .e,)) / ?- 4 

spready,e~ ,...,en el,. . . ,e, / (210%~). raisePointerToLeaf() , 

and, with 1 representing the list vo, el,. . . ,e,: 

1 spread,vl, e2 . . . , e, 1 T’ i 

spreadTe2,. 1 . . ,e, / (v~%T’). pointNextSibling() 

if Vn 2 0 (VI%?-’) # I, , 
80 Florent Kirchner 

and 

and 

spread,vl, 1 e2.. . ,e, / 7’ (fail) / T if 3n 2 0 (VI%,’) = I, , 

and 

spreadkv, / 7’ -% (skip) / (Y,%T’). lowerPointer(1) 

if T’# 0 

and (v,,%~’). pointNextSibling() = 0 , 

and 

,el ,...,en v, / 7’ i 

spread~3e~,...,en, ( 8 k’P)v~, 2 el,. . . ,e,, (skip) / T 

if (w,%T’). pointNextSibling() # 0 , 

The (branch . . . ) method behaves likewise, but repeats the last element of the list on all the remaining 

siblings when necessary: 

(branch vo (el.. .e,)) / T --% 

branchy ,el ,...,en el, . . . , e, / (wo%T). raisePointerToLeaf0 . 

The reduction rules are the same for branch?Ie’ as for spread?’e’’“‘’en , but for the last rule: 

branchy ,el ,...,en Y, / r’ i 

branch? ,el ,...,en ,en v~,el,. . . ,e,, e, / 7 

if (v,%~’). pointNextSibling() # 0 , 

N-ary backtracking A combination of the try and the branch strategies, try-branch applies v1 to the 

current goal, and in case it generated subgoals it applies each of the v: to one of the subgoals. Else it 

applies 212. As for try, this strategy catches any failure that would arise from the application of any of 

the v:. 

(try-branch vo (el . . .e,) e’) / T 4 

(try-branch?7e’ el . . .e,) / (VO%T) 

if (vo%T). hasProgressed() 

and Vn 2 0 (VO%T) # I, . 

(try-branch wo (el . . .e,) e’) / T 

(try-branch vo (el . . .e,) e’) / T --% e’ / T 

(fail) / T if 3n _> 0 (WO%T) = I, 

if i(v0%07). hasProgressed0, 

with 

1 (try-branch, v1e2 . . . e,) / 7’ 

(try-branch: e2 . . . e,) / (w~%T’). pointNextSibling() 

if Vn _> 0 (vl%07’) # I, , 
~~ ~ 

Coq Tacticals and PVS Strategies: A Small Step Semantics 81 

and 

(try-branch, 1 w1e2.. .en) / 7’ (skip) / T 

if 3n 2 0 (v1%07’) = 1, , 

and 

if I-’= 0 

or (vn%.r’). pointNextSibling() # 0 , 

and 

try-branchkv, / 7’ --% (skip) / (v,%r’). lowerPointer(1) 

if r’# 0 

and (v,%T’). pointNextSibling() = 0 , 

and 

5.3 User-defined strategies 

As for Coq, the meta-notation needs to be enriched to cope with the user definitions. Let M be a memory state 

object storing the new strategies, and its methods setStrategy(name, description) and getStrategy(name). 

Unlike Coq though, PVS uses a specific file, pvs-strategies, to load user definitions, and does not allow 

for toplevel declarations. Moreover, these definitions split into two categories, rules i.e. atomic commands or 

blackbox, and strategies i.e. non-atomic commands or glassbox. 

PVS calls the setstrategy at launch to initialize the memory state, and only allows readings during runtime: 

M. getStrategy(x) + M(x) , 

where M(x) = (Box e), Box is one of the two tags Glass or Black, and e is a proof script. The tags are not 

part of the real PVS syntax: they are introduced here to describe a phenomenon that is actually hidden in 

the implementation. 

When evaluating a tactic on which none of the previous reduction rules apply, the following will be tried: 

x / T M. getStrategy(x) / T 

Finally this calls for a definition of the semantics of the Glass and Black commands: 

(Black u) / T 

(Black v) / T 4 

(skip) / T if 3n 2 0 (v%T) = I, 

/ 7- if Vn 2 0 (21%~) # I, , 

(Glass v) /T+~/T. 
82 Florent Kirchner 

5.4 Context 

5.5 Tactics 

The same conventions will be used as for Coq's tactics. Note that PVS does not use the error level: lo is the 

only error possible. 

(flatten)%T. I' I- A 3 B = T. addLeaves (I', A I- B). setProgess(true) . 

(flatten)%T. r I- A V B = T. addLeaves (I' I- A, B). setProgess(true) . 

(f latten)%T. I', A A B I- C = 

T. addLeaves (I', A, B I- C). setProgess(true) . 

(propax)%-. I', A I- B = T. leaproven(). setProgess(true) 

if A and B are syntaxically 

equal. 

(beta)%'o.r. I' t (Xz : t)(u) = T. addLeaves (I' t[z tc u]). setProgess(true) . 

(skip)%T=r . 

(skolem * (' 'a' '))%IT. I', (32 : A) I- B = 

T. addLeaves (I', A[z +I u] I- B). setProgess(true) . 

(skolem * ("a" ))%T. I'I-(Vz:A) = 

T. addLeaves (I' t A[. +I u]). setProgess(true) . 
Coq Tacticals and PVS Strategies: A Small Step Semantics 83 

6 Conclusion and Future Work 

We have presented a small step semantics for the core of both Coq and PVS’s tacticals, as well as for some 

simple tactics. This semantics seems correct with respect to the formal definition of both languages, provided 

for Coq by Delahaye’s definition of Ltac [4], and for PVS by the Prover Guide [ll]. A proof of correctness of 

our semantics in regard with these definitions is currently under way. Future work will also try to incorporate 

more advanced tactics to the system, although this will certainly prove more difficult, entailing the use of 

global proof environments and variables, a-equivalence classes, and most likely the integration of PVS-like 

automatic conversion methods. It might also be interesting to express tacticals from other languages (such 

as Isabelle or NuPrl) in this framework, and the idea of a correlation between proof tacticals and rewriting 

strategies might be worth studying. Nevertheless the formal basis of the semantics is easily and conservably 

extendable, and should allow for an efficient and - hopefully - not too complicated continuation. 

Finally, beyond its informative features, this work sets the very basis for an unified representation of PVS’s 

strategies and Coq’s tacticals, which would allow for proof portability, double-checking, prover-relevancy 

modularization, i.e., an overall improved flexibility and interoperability. 

References 

I [l] B. Barras, S. Boutin, C. Cornes, J. Courant, J.C. Filliatre, E. GimCnez, H. Herbelin, G. Huet, C. Muiioz, 

C. Murthy, C. Parent, C. Paulin, A. Saibi, and B. Werner. The Coq Proof Assistant Reference Manual - Version 

7.4. http://coq.inria.fr/doc/main.html, 2003. 

[2] David Carlisle, Scott Pakin, and Alexander Holt. The Great, Bzg Lzst of Bw Symbols, February 2001. 

[3] H. Cirstea, C. Kirchner, and L. Liquori. Rewrite Strategies in the Rewriting Calculus. In WRLA ’02, volume 71 

[4] David Delahaye. Conceptzon de langages pour de‘crare les preuves et les automatasatzons dans les outrls d’azde a 

[5] Catherine Dubois. Proving ML Type Soundness Within Coq. In Mark Aagaard and John Harrison, editors, 

[6] CCsar Muiioz. Strategies in PVS. Lecture notes, 2002. National Institute of Aerospace. 

[7] Tobias Oetiker. The Not So Short Introduction to BT&Y2e, January 1999. 

[8] Sam Owre and Natarajan Shankar. The formal semantics of PVS. Technical Report CR-1999-209321, Computer 

of Electronzc Notes an Theoretzcal Computer Science. Elsevier Science B.V., 2003. 

la preuve. Thhse de doctorat, UniversitC Paris 6, 2001. 

TPHOLs, volume 1869 of Lecture Notes an Computer Scaence, pages 126-144. Springer, 2000. 

Science Laboratory, SRI International, Menlo Park, CA, May 1999. 

University, 1981. 

I [9] Gordon D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Aarhus 

[lo] Franqois Pottier. Typage et Programmation. Lecture notes, 2002. DEA PSPL. 

[ll] N. Shankar, S. Owre, J. M. Rushby, and D. W. J. Stringer-Calvert. PVS Prover Guide. Computer Science 

Laboratory, SRI International, Menlo Park, CA, September 1999. 

[12] Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Informatzon and CompuI 

I tatzon, 115(1):38-94, 15 November 1994. 
Rippling in PVS 

A. A. Adamsl and L. A. Dennis' 

The University of Reading 

A.A.Adams@Rdg.ac.uk 

http://wu.rdg.ac.uk/"sisOOaaa/ 

lad@cs.nott.ac.uk 

http://cs.nott .ac.uk/'lad/ 

The University of Nottingham 

Abstract. Rippling is a method of controlling rewriting of the terms in an induction step of an inductive proof, to ensure that a position is reached whereby the induction hypothesis can be applied. 

Rippling was developed primarily by the Mathematical Reasoning Group at the University of Edinburgh. The primary implementations are in the two proof planning systems Clam and XClam. An 

implementation is also available in HOL. In this paper we explain how we plan to implement rippling 

as a tactic for automatic generation of proofs requiring induction in PVS. Rippling has mostly been 

used as part of a larger project for developing high-level proof strategies, but has rarely been applied 

to "real-world" examples. Once we have this implementation we intend to assess the utility of this as 

a tactic by running rippling on the large number of inductive proofs developed by Gottliebsen as part 

of the PVS Real Analysis library [8]. By comparing the performance of the automation offered by rippling on these proofs with the original proof, which were proved by a combination of hand-generation 

of proofs and by existing PVS strategies, we hope to assess the utility of rippling as a technique for 

real-world applications. 

1 Introduction 

When faced with a lemma (or sub-goal) requiring an inductive proof, the experience PVS user will invoke 

one of the PVS strategies such as induct-and-rewrite or induct-and-simplify. While in many cases 

these may work, there are also often cases where more user-control is necessary, requiring a user to control 

the rewriting stages of the inductive parts of the proof manually. The Real Analysis library developed by 

Gottliebsen [8] contains numerous such inductive proofs (mostly convergence arguments for power series) 

which do not fall to the existing automation of PVS. 

There has been a great deal of work on automating inductive proof in different provers, but the approach 

we concentrate on is rippling. This approach is detailed below, but it is primarily a method for controlling 

the use of rewrite rules to ensure that they are used in the correct order, and in the correct orientation, to 

allow cross-fertilisation, i.e. the use of the induction hypothesis. In addition to control of the rewriting steps 

necessary to prove the induction step, it is possible to choose the wrong induction scheme to apply in the 

first place. We propose to implement rippling and induction scheme choice in PVS to produce tactics that 

will complement the existing induction tactics in PVS. We plan to test our hypothesis that induction choice 

and rippling can prove goals on which existing tactics fail, by applying the resulting system to the PVS Real 

Analysis library's induction proofs. 

2 Rippling 

Rippling is a rewriting technique which relies upon a difference reduction heuristic rather than an ordering 

on terms for termination. This makes it attractive in an induction setting where it has been used extensively 

(see [6] for a full discussion) in which the object is to reduce the differences between the induction conclusion 

and the induction hypothesis although it has also been used in other settings such as equational rewriting [ll]. 

Rippling was first introduced in [5]. We intend to use the theory as presented by Smaill & Green [13] 

who proposed a version that naturally copes with higher-order features. Rippling steps apply rewrite rules 

to a target term (called the erasure) which is associated with a skeleton and an embedding that relates 
Rippling in PVS 85 

the skeleton to the erasure (e.g. rippling rewrites an induction conclusion which has an induction hypothesis 

embedded in it so the induction hypothesis is the skeleton and the conclusion is the erasure). After rewriting, 

a new embedding of the skeleton into the rewritten term is calculated. There is a measure on embeddings 

and any rewriting step must reduce this embedding measure (written as <@). 

Rippling is terminating. Rippling either moves differences outwards in the term structure so that they 

can be cancelled away or inwards so that the differences surround a universally quantified variable (or sink). 

If it is possible to move differences inwards in this way the embedding is said to be sinkable. The measure 

on embeddings allows differences that are being moved outwards to be moved inwards but not vice versa. 

There is not space here to give full details of the embedding measure - details of the first-order measure can 

be found in [l] and details of the measure for embeddings can be found in [713. 

Embeddings treat the syntax of terms as a variant of Higher-Order Abstract Syntax or A-tree syntax [12] 

in which abstraction and application are explicitly represented as nodes in the term tree. 

The position of a node in a term tree is determined by a list of integers indicating the path from the root 

of the tree to that node (for implementation reasons this list is usually read from right to left). The operator 

of an application term is labelled as the 1st branch and then each member of the ensuing tuple from 2 to n 

in order4. A-abstraction nodes are ignored when calculating term positions. So the position of g in the term 

g(Az.f(a,z,b)) is [l], the position of z is [3,2] and the position off is [1,2]. 

Embeddings are also described by a tree data structure. Embedding trees describe how the skeleton term 

tree embeds in the erasure term tree. The nodes in an embedding tree can be viewed as labels on the nodes in 

the term tree of the skeleton (excluding A-abstraction nodes). These labels contain addresses. The addresses 

are the addresses of nodes in the term tree of the erasure into which the skeleton is to be embedded. A 

node in an embedding tree will appear at a function application node in the skeleton term tree and indicates 

that this node is matched to the function application term in the erasure term tree at the indicated address. 

Similarly the leaves of an embedding tree are attached to the leaves of the skeleton term tree. 

Example 1 Consider embedding the term Az. f(x) into the term Ay. Ax. (f(y) + z). We do this as in 

figure 1. The two terms are shown as trees with branches represented by solid lanes. The address of each node 

is given (A-abstraction nodes do not carry addresses). The embedding appears between them as an embedding 

tree with dashed lines - the address label of the nodes is also shown. The dotted arrows illustrate how the 

embedding tree links the two terms. 

application [I 

/ 

I Fig. 1. An Embedding 

Draft version available from second author. 

This assumes an uncurried syntax is being used - it is easy to restrict rippling to curried syntax if desired. 
86 A. A. Adams and L. A. Dennis 

In proofs by induction, using a constructor formulation, the measure is used as follows. Given an induction 

hypothesis @(x) and goal @(s(x)), there is an embedding, e, between @(x) and @(s(x)). Recursion equations 

and lemmas are available as rewrite rules to be used on the goal. Typically, these rewrite rules are not 

confluent, and include potentially looping rules, such as associativity. The following heuristic can be used: 

use rewrites which give a new goal G' such that there is an embedding, e', between @(x) and G', and such 

that e' <M e, i.e. the embedding is smaller in the measure. 

The rippling heuristic imposes three conditions on such rewriting: 

1. soundness - the rewriting should correspond to logically valid inference; 

2. skeleton invariance - the appropriate skeleton embeds in the goal, before and after rewriting; 

3. measure decreasing - the embedding in the rewritten formula is smaller in the order. 

First order rippling calculi use goals decorated with annotations in the form of boxes, underlines and 

arrows. We intend to use these conventions within this paper in order to indicate to the reader how the 

current embedding relates the skeleton to the erasure but do not intend to include such decorations in our 

implementation. If one expression can be embedded into another then this is indicated in the notation by 

placing boxes (or wave fronts) round the additional parts of the larger expression. The embedded expression 

can be identified as those parts of the expression that are outside the boxes or those parts within boxes which 

are underlined (called wave holes). As an example the result of difference matching5 s(x)~ and s(x+y) would 

be s(lc+1(I ). Here the first expression, s(x), appears outside the wave fronts or in the wave holes of the 

annotated expression. If the annotations of s(P1 ) are stripped away then the second expression, s(z+y), 

is left. s(z) is the skeleton and s(z + y) is the erasure. 

The main advantages of rippling are that it allows an equation to be treated as a rewrite in both directions 

without loss of termination and provides useful information for automatically patching failed proof attempts. 

Example 2 Consider the associativity of disjunction: 

Av(BvC)=(AvB)vC, 

which can be used as a rewrite in either direction, depending upon the skeleton to be preserved, and the 

direction in which the wave-front is to be moved. For example, the term A V ml can be rewritten to 

I (A v B) V C I using the equation as a rewrite rule from left to right while it is also possible (perhaps later ~ 

in the same proof) to rewrite the term V C to -1 using the rule from right to left. 

In the first case the skeleton is A V B (which embeds into the goal both before and after rewriting), and 

in the second it is B V C. Thus one is able to use rewrites in both directions during rippling so long as they 

are in contexts where the skeletons differ. 

During rippling the direction in which a difference is moving is indicated using an arrow on the wave 

fronts. If a difference is moving outward in the term structure the arrow is upwards and if the difference is 

moving inward then the arrow is downwards. We indicate variables which are universally quantified in the 

skeleton (i.e. sinks) with the symbol u. So if for instance the induction hypothesis were Vy.n + y = y + n 

then the conclusion might be annotated as ]so) + LyJ = LyJ + mf '. An additional heuristic often 

used with rippling is to insist that all rewrites involving inward moving differences are sinkable (i.e. there is 

a sink in any subterm involving an inward wave front). 

The process by which annotations or embeddings are generated. 

The semantics of the symbols here is unimportant to the description but s can be viewed as the successor function 

on natural numbers and + as addition on natural numbers. This is consistent with the use of these symbols 

elsewhere in this paper. 

Note that in the conclusion the universal quantifier has been removed by skolemisation. 
Rippling in PVS 87 

2.1 Coloured Rippling 

In [10,14] notions of “colo~ring~~ annotated terms are used for situations in which a number of different 

skeletons are in play and so differences are manipulated with respect to more than one term. Colouring 

can be used to indicate to which skeleton a wave hole relates, or whether it relates to both. To achieve 

this embeddings based versions of rippling extend their annotations so that one erasure is related to several 

skeleton/embedding pairs. 

I 

I 

2.2 An Example of Rippling 

Consider the theorem 

VZ, m : list(7). rev(Z) <> m = qrev(l, m) 

I The step case goal is annotated by difference matching as 

I 

I The following equations are available for use as rewrite rules: 

rev(X :: Y) 5 rev(Y) <> X :: nil 

(u <> V) <> w E u <> (V <> W) 

I qrev(H :: T, M) G qrev(T, H :: M) 

I Using these the conclusion can be rippled as follows: 

I I I I 

h :: nil <> LM‘J can be simplified to h :: LM’J making the conclusion 

I 

I I 

LM’J is a sink and the goal can be proved by appeal to the induction hypothesis. 

the annotated terms. At this point rippling is said to be blocked, that is no further rippling can occur, but 

fertilisation isn’t possible. There are a number of normalisation techniques which can perform the necessary 

simplification to unblock rippling. In PVS it will be possible to use existing tactics to complete this last step. 

I The last simplification step is not a rippling step since h :: nil and h are both unannotated subterms of 

I 

i 

2.3 Implementing Rippling in PVS 

In order to implement rippling in PVS we will need to extend the goal representation to allow annotation with 

embeddings. Once this is done we intend to provide three basic tactics SET-UPRIPPLE which will perform 

difference matching to annotate a goal with respect to one or more of its hypotheses, RIPPLE(ru1e) which 

will attempt to rewrite the goal using rule - we hope to be able to use existing rewriting tactics within 

PVS for this and simply add additional checks for the rippling conditions on top of this and lastly a tactic 

POSTRIPPLE which will remove annotations. 

Using these basic tactics it will be possible to create more sophisticated tactics which (for instance) 

choose a rule from PVS’ rewrite rule set rather than relying on one provided by the user and which can in 
88 A. A. Adams and L. A. Dennis 

one step annotate a goal, ripple as much as possible and then remove annotations thus automating the full 

rewriting process in the step case of an induction. 

We anticipate that taken together these tactics will give the power of fully automated rippling as well as 

the flexibility of an interactive setting so that a user can intervene and guide the process more carefully if 

desired. 

Extending the PVS goal syntax to allow rippling annotations might prove problematic. However, an 

alternative approach is to extract a copy of the current goal and annotate it. This annotated goal is then 

passed as an extra argument to help control the rippling tactics. The annotated goal term can then be 

recalculated at each step and as a “reality-check” the annotations can be stripped and compared with the 

actual goal produced by applying a rewrite rule. 

induction scheme 

3 Ripple Analysis 

In addition to controlling the rewriting during the step case rippling has a second major application in proof 

by induction which is in automating the choice of the induction scheme and variable to use. This automation 

process is called ripple analysis [6] and is based on a rational reconstruction of the recursion analysis of 

Boyer and Moore [3]. 

In essence ripple analysis exploits any recursive definitions (or possibly lemmas) for the functions involved 

in the current goal to create candidate choices for induction schemes. Implementations of ripple analysis 

examine candidate induction schemes and variable choices and try to see whether a ripple step can be 

applied to any new structure introduced by the scheme. 

Example 3 Consider the proof of the theorem 

VU, b, C. a + (b + C) = (a + b) + c (10) 

There are three choices of induction variables here a, b or c. Assume the following equivalence is available 

as a rewrite rule 

s(X) + Y s(X + Y) (11) 

Consider the annotated conclusion of the the step case if a is chosen as induction variable and the 

is used: 

In this case both occurrences of new structure (the two wave fronts) can be moved by a ripple step using 

(11). However if b were chosen as the induction variable then the annotated step case conclusion would be 

Va,c. 1. + (m’ + Lcl> = (1.J +ut 0) ) + LcJ (14) 

In this case while the wave front on the LHS of the equality can be moved by a ripple step that on the 

right can not. The wave front on the right is said to be flawed. 

Traditionally ripple analysis works with a database of possible schemes and applies them to all candidate 

induction variables and combinations of induction variables (this allows induction to be applied simultaneously to both a and b (for instance) should there be a rewrite rule which requires a successor constructor 

in both places - obviously additional base cases need to be generated in such cases). Each candidate 

scheme/variable choice pair is scored according to how many flawed wave fronts it contains, in general this 

heuristic score also takes into account the “complexity” of the suggestions (i.e. preferring schemes introducing minimal structure on one variable to schemes introducing more complex new structure or using more 
Rippling in PVS 89 

than one induction variable) and the suggestion with the highest score is chosen as the candidate for the 

induction. 

Recently Gow [9] has investigated the dynamic generation of induction schemes as an alternative to the 

use of a fixed database. This was the method used in the original Boyer-Moore system [2], but with rather 

I unsatisfactory results, leading to the removal of this aspect from their later implementations [4] 

I 3.1 Implementing Ripple Analysis in PVS 

We intend to implement a new induction tactic in PVS which will automatically chose an induction scheme 

and induction variable. This tactic will use the rippling machinery we will already have implemented to provide the RIPPLE tactic and will use choose the most appropriate scheme from a defined (but user extensible) 

I set of schemes. There are a number of schemes included in the PVS prelude, such as subrange induction: 

k, m: VAR subrange(i, j) 

p: VAR pred[subrange(i, j)] 

I subrange-induction: LEMMA 

(p(i) AND (FORALL k: k < j AND p(k) IMPLIES p(k + I))) I 

IMPLIES (FORALL k: p(k)) 

Various libraries also implement new induction schemes for new types when introduced. 

I This tactic can then be combined with our rippling tactics and application of (induction) hypotheses to 

I provide a tactic which completely automates the step case of induction proofs and generates base case goals 

for the attention of the user. 

4 Conclusion 

I This paper has presented the basics of rippling, which has been shown theoretically (and in practice with 

other theorem proving systems) to be a useful way of controlling induction proofs. The authors believe it will 

prove useful as an addition to the strategies currently available in PVS. It is our intention to implement the 

these experiments show that rippling is useful we will work with the PVS developers to release a the code 

for general use. 

I system as described in this paper and to test our hypothesis of utility on the Real Analysis library. Should 

I References 

1. David Basin and Toby Walsh. A calculus for and termination of rippling. Journal of Automated Reasoning, 

2. R. S. Boyer and J. S. Moore. A Computational Logic. Academic Press, 1979. 

3. R. S. Boyer and J S. Moore. A Computational Logic. ACM monograph series. Academic Press, New York, 1979. 

4. R. S. Boyer and J. S. Moore. A Computational Logic Handbook. Academic Press, 1988. 

5. A. Bundy, A. Stevens, F. van Harmelen, A. Ireland, and A. Smaill. Rippling: A heuristic for guiding inductive 

proofs. Artificial Intelligence, 62:185-253, 1993. Also available from Edinburgh as DAI Research Paper No. 567. 

6. Alan Bundy. The automation of proof by mathematical induction. In A. Robinson and A. Voronkov, editors, 

Handbook of Automated Reasoning, Volume 1. Elsevier, 2001. 

7. L. A Dennis, I. Green, and A. Smaill. Embeddings as a higher-order representation of annotations for rippling. 

In prep. 

8. H. Gottliebsen. Transcendental Functions and Continuity Checking in PVS. pages 198-215. Springer-Verlag 

LNAI 1869, 2000. 

9. J. Gow. The Dynamic Creation of Induction Rules using Proof Planning. PhD thesis, Division of informatics. 

16(1-2):147-180, 1996. 

10. D. Hutter. Guiding inductive proofs. In M. E. Stickel, editor, 10th International Conference on Automated 

Deduction, volume 449 of Lecture Notes in Artificial Intelligence, pages 147-161. Springer-Verlag, 1990. 

11. D. Hutter. Using rippling for equational reasoning. In S. Holldoblrt, editor, Proceedings 20th German Annual 

Conference on Artificial Intelligence KI-96, number 1137 in Lecture Notes in Artificial Intelligence. SpringerVerlag, 1996. 
90 A. A. Adams and L. A. Dennis 

12. D. Miller. Abstract syntax for variable binders: An overview. In et. al. J. Lloyd, editor, Computation Logic 

(CL '2000), volume 1861 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 2000. 

13. Alan Smaill and Ian Green. Higher-order annotated terms for proof search. In Joakim von Wright, Jim Grundy, 

and John Harrison, editors, Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs '96, 

volume 1275 of Lecture Notes in Computer Science, pages 399--414, Turku, Finland, 1996. Springer-Verlag. Also 

available as DAI Research Paper 799. 

14. Tetsuya Yoshida, Alan Bundy, Ian Green, Toby Walsh, and David Basin. Coloured rippling: An extension of a 

theorem proving heuristic. In A. G. Cohn, editor, Proceedings of ECAZ-94, pages 85-89. John Wiley, 1994. 
Generating Proof-Specific Strategies for PVS* 

t Pertti Kellomaki 

Tampere University of Technology 

pertti.kellomakiQtut.fi 

http://wvv.cs.tut.fi/"pk 

Abstract. We describe how generated PVS proof strategies were used to partially automate invariant 

proofs of joint action specifications. A user writes specifications using the Disco specification language, 

and a compiler maps the specifications to PVS theories accompanied with custom strategies for verifying 

invariance theorems in the theories. 

j 1 Introduction 

This paper describes work that was done in 1995-1997 using PVS [lo] versions up to 2.1. Some of the work 

has likely been rendered redundant by advances in PVS, especially by improvements in the grind strategy, 

but some of it still remains relevant. 

In [7,6] we present verification of invariant properties of systems specified using the joint action formalism. 

A joint action is an atomic change of state involving multiple participating objects. An action specifies 

assignments to the participants, and the rest of the world implicitly remains unchanged. 

When mapped to the logic of PVS, joint actions give rise to conjunctions of quantified subformulas. The 

earlier versions of PVS we were working with did not handle quantifications very well automatically, but 

fortunately it turns out that the proofs have a regular high-level structure which depends on the structure 

of the specification for which invariants are being verified. 

Our solution was to generate a custom PVS strategy for each invariant-action pair in a specification at 

the same time as mapping the specification to PVS logic. The user then used the generated strategies to 

As the concrete vehicle for expressing specifications we used the Disco [l, 4,8] specification language. 

compiler and an animation facility to validate the specification. Invariant properties can be expressed in the 

language, and the user is notified if the purported invariants are violated during animation. 

If formal proofs of invariants are desired, the compiler can be instructed to generate a PVS theory 

corresponding to the Disco specification. The theory is accompanied with a set of custom strategies to make 

verification easier. Verification is carried out in the usual manner by interacting with PVS, and the custom 

strategies can be used to automate the routine parts of invariant proofs. 

The rest of the paper is organized as follows. Section 2 introduces the joint action approach to specificaI 

I 

i 

i 

, drive the proof to a point where some form of human judgment was needed to proceed. 

Figure 1 depicts the big picture. A user writes specifications using the Disco language, and uses the Disco I 

I 

I 

tion. Sections 3 and 4 describe mapping Disco specifications and automation of invariant proofs, respectively. 

Section 5 discusses the work, and Section 6 concludes the paper. I 

2 Joint Action Specifications 

A joint action [2] specification consists of a set of state variables, a predicate characterizing the initial state, 

and a set of state transitions called joint actions. State variables reside in objects, which are instances of 

classes. Joint actions are intended to be used to specify synchronizations of objects in distributed systems. 

An action is enabled, if a combination of objects exists to participate in the roles of the action, such 

that the guard of the action is true. The selection of the action to be executed next and the selection of 

participants is nondeterministic. Concurrency is modeled via interleaving. 

* This research was suported by the Academy of Finland, grant number 102536. Pertti Kellomtiki is funded as a 

Research Fellow by the Academy of Finland. 
92 Pertti Kellomaki 

compiler Is; PVS specification PVS 

PVS strategies I 

Fig. 1. The Disco specification environment 

The Disco specification language has a programming language like notation for joint actions. Figure 2 

illustrates a Disco specification. The action balance models simple load balancing, and it is enabled for any 

pair of node objects a and b for which the guard a.w < b.w is true. The action changes the values of a.w and 

b.w to be closer to one another, while the rest of the world remains unchanged. 

system loadBalance is 

class C is 

end; 

assert pos-w is V cc : C :: cc.w _> 0; 

action newJob by cl : C is 

when c1.w < 10 do 

end; 

action balance by a, b : node is 

when a.w < b.w do 

w : integer; -- models the work load of a node 

-- implicitly also an initial condition 

-- an arbitrary upper limit 

c1.w := c1.w + 1; 

a.w := a.w + 1; 

b.w := b.w - 1; 

end; 

end: 

Fig. 2. Disco specification 1oadBalance 

The semantics of joint action specifications can conveniently be given in Lamport’s Temporal Logic of 

Actions [9] (TLA). Each joint action corresponds to a TLA action wrapped in existential quantifications 

corresponding to the roles of the action. 

Conceptually the biggest difference between TLA and Disco is the treatment of state variables. TLA has 

named state variable while in Disco state variables are fields contained in anonymous objects. The only way 

to refer to objects is via quantification, either by referencing explicitly quantified variables or by referencing 

the implicitly quantified action roles. This indirection is also the main source of additional complexity in 

proofs. 

The TLA meaning of a Disco action depends on the context in which it is interpreted, because in logic 

one needs to make explicit which variables are not changed. In a specification which contains a single class 

node with a single attribute w, the TLA meaning of action balance is 
Generating Proof-Specific Strategies for PVS 93 

3(a, b : node) : 

a # b A a.w < b.w 

A a.w' = a.w + 1 

AV(c: node) : c # a Ac # b + c.w' = c.w 

where a.w and a.w' refer to the value of field w of participating object 

respectively. The conjunct a # b arises from the semantics of Disco actions, 

only participate in one role of an action. 

A b.w' = b.w - 1 

a before and after the action, 

which states that an object can 

In a specification where class node additionally has an attribute y, the meaning is 

](a, b : node) : 

a # b A a.w < b.w 

A a.w' = a.w + 1 

A V(c : node) : c # a A c # b =+ c.w' = c.w 

Ab.W' = b.w - 1 

A V(c : node) : c.y' = c.y 

Each additional state variable adds a new quantified expression as a conjunct. Every class in the specification must be taken into account, even those that are not mentioned in the action at all. While straightforward 

in principle, a large number of universally quantified subexpressions makes mechanical reasoning about actions rather tedious in practice. 

3 Mapping Disco to PVS 

The mapping from Disco to PVS closely follows the TLA formulation above. We represent classes as PVS 

record types, where each field is a function from state to the appropriate PVS type, i.e. a state variable. 

State is an uninterpreted type, and a behavior is a sequence of states. Figure 3 shows the PVS formulation 

of the fragment of temporal logic we use. 

Figure 4 shows the PVS theories corresponding to the specification in Figure 2. Two theories are generated 

for a Disco specification, one containing the definitions corresponding to Disco classes and actions, and 

another one containing the theorems to be proved. In order to modularize proofs, a separate lemma is 

generated for each invariant-action pair. 

With hindsight, a different mapping of Disco to PVS would have been more amenable to mechanical 

verification. In particular, we could have used the PVS function override mechanism to express assignments 

to state variables. In the formulation we used, we had to instantiate a quantified formula for each unchanged 

state variable whose value in the next state we needed to compute. Some proof automation would still have 

been desirable, because the layered style of developing specification advocated by the Disco method easily 

leads to specifications with many classes with many fields. 

4 Generating PVS Strategies 

The only way to refer to objects in Disco is via quantification, so all the formulas in the initial sequent of a 

Disco invariant proof are quantified. In order to get to the interesting parts of a proof, one has to do a series 

of skolemizations and instantiations. When an action guard contains quantifications, it is useful to apply the 

skolemization-instantiation process to it as well. 

The skolemizations produce two sets of names in the proof state, one corresponding to the participants 

of the action and another corresponding to the objects denoted by the quantified variables of the invariant. 

Since there is a potentially large number of ways in which the two sets can overlap, the top level of an 

invariant proof is a possibly large case analysis. 

Fortunately invariance proofs follow a ked pattern, so constructing the top level of a proof can be taken 

care of automatically. A simple heuristic is often sufficient for dealing with quantifiers, and the necessary 

case analysis can be derived from the skolemizations performed. 
94 Pertti Kellomdci 

disco: THEORY 

BEGIN 

state: TYPE 

behavior: TYPE = [nat -> state] 

temporal-formula: TYPE = [behavior -> bool] 

state-predicate: TYPE = [state -> booll 

action: TYPE = [state, state -> booll 

stutter(A : action) : action = 

LAMBDA (unprimed, primed : state) : 

A(unprimed, primed) or primed = unprimed 

bool = FORALL (n: nat): F(suffix(b, n)) 

temporal-formula = LAMBDA (b: behavior): P(b(0)) 

[I ((F: temporal-formula) , (b: behavior)) : 

statepred2temporal((P: state-predicate)): 

CONVERSION statepred2temporal 

action2temporal((A: action)): temporal-formula = 

CONVERSION actionltemporal 

invariant((P: state-predicate). (assumptions: bool). 

LAMBDA (b: behavior) : A(b(O), b(1)) 

(I: state-predicate) , (A: action)) : 

bool = FORALL (b: behavior): 

assumptions AND I(b(0)) 

AND [I (stutter(A1 ,b) => [I (P,b) 

NOT 

( 

=> 

objid: TYPE 

WD disco 

preserves((sing1e-action: action), (P: state-predicate), 

(assumptions: bool) , (I: state-predicate) , 

(A: action)) : 

FORALL (b: behavior) : 

bool = 

assumptions AND I(b(0)) AND [I (stutter(A1 ,b) 

=> FORALL (n: nat): 

P(b(n)) AND single-action(b(n) , b(n+l)) => P(b(n+l)) 

invariant-rule: THEOREM 

FORALL (P: state-predicate, assumptions: bool, 

I: state-predicate, A: action): 

(I(b(0)) AND [] (stutter(A1 ,b)) 

OR 

assumptions AND I(b(0)) => P(b(0))) 

(FORALL (b: behavior): 

AND FORALL (n: nat): 

assumptions AND P(b(n)) AND A(b(n). b(n + 1)) 

=> P(b(n + 1)))) 

invariant (P, assumptions, I, A) 

Fig. 3. Formalization of temporal logic in PVS 
~~ 

Generating Proof-Specific Strategies for PVS 95 

LoadBalance: THEORY BEGIN 

discolib: LIBRARY = "/home/korppi-a/pk/vaikkari/pdp/pvs/" 

IMPORTING discolibQdisco 

c: TYPE FROM [# u: [state -> int], ref: objid #] 

neuJob-guard((c1: c) ,(other: state)) : bool = u(cl) (other) < 10 

neuJob((unprimed, primed: state)): bool = 

(neuJob-guard(c1, unprimed)) AND 

(EXISTS (cl: c) : 

((u(c1) (primed) = (u(c1) (unprimed) + 1)) AND 

( (FORALL (other: c) : 

((other) /= (cl)) IMPLIES 

(w(other)(primed) = (u(other)(unprimed))))))) 

(action balance omitted) 

END 1oadBalance 

.oadBalance-assertions: THEORY BEGIN 

IMPORTING example 

c-unique-reference: bool = 

FORALL (objl. obj2: c): ref (objl) = ref (obj2) 

IMPLIES objl = obj2 

pos-u-body((cc: c) , (other: state)) : bool = ~(cc) (other) >= 0 

pos-u((other: state)): bool = 

(FORALL (cc: c): pos-u-body(cc, other)) 

ASSUMPTIONS: bool = c-unique-reference 

INIT((other: state)): bool = pos-w(other) 

ACTIONS((s, sp: state)): bool = 

neuJob(s. sp) OR balance(s, sp) 

neuJob-preserves-pos-v: 

LEMMA preserves(newJob, pos-u, ASSUMPTIONS, INIT, ACTIONS) 

balance-preserves-pos-w: 

LEMMA preserves(ba1ance. pos-u, ASSUMPTIONS, INIT. ACTIONS) 

pos-u-is-invariant: 

THEOREM invariant(pos-u, ASSUMPTIONS, INIT, ACTIONS) 

END 1oadBalance-assertions 

Fig. 4. Mapping of specification 1oadBalance to PVS 
96 Pertti Kellornaki 

In a programmable LCF-style theorem prover such as HOL [3], we could write a program in the prover 

metalanguage to construct the high level proof. PVS is not programmable in this sense, and it is not possible 

to write a general strategy that would handle all invariance proofs. Instead, we use an auxiliary program to 

generate offline a specific instance of the general strategy for each specification. Since a specification and the 

generated strategies are very closely tied together, it is convenient to merge the tools for translating from 

Disco to PVS and for generating proof strategies. Proof strategies for a specification are normally generated 

at the same time as the specification is translated to PVS. 

We have not attempted to write decision procedures in the sense that the generated strategies would 

try automatically to prove some subgoals. Rather, the strategies simplify the proof up to a point where the 

subgoals are ready for the user to take control. The user can of course use the PVS strategy language to 

advice PVS to apply some strategy to each of the subgoals before resorting to interactive proof. For example, 

when verifying an invariant involving large amounts of propositional logic, one could start the proof with 

the command 

(then* ( generated strategy) (bddsimp)) 

which would first construct the top level of the proof using the generated strategy, and try to resolve each 

of the resulting subgoals using the bddsimp strategy of PVS. Any subgoals not discharged by bddsimp would 

then be presented to the user for interactive proof. 

4.1 Example 

Consider verifying the assertion pos-w in Disco specification ZoadBalance. In order to verify that pos-w is 

an invariant, we need to establish that it holds in the initial state, and that the actions of the specification 

preserve it. 

Figure 5 shows the generated top level strategy. The strategy first introduces the invariant rule to the 

sequent and instantiates it suitably (lines 2 and 3). The proof is then split into two parts: the initial condition 

(lines 7 and 8) and the preservation of pos-w (line 9 onward). The former is trivially taken care of by expanding 

the definition of INIT (the Disco semantics includes all assertions as conjuncts in the initial condition), and 

the latter by introducing lemmas and instantiating them suitably. 

Figure 6 shows the strategy generated for establishing that pos-w is preserved by action newJob. Lines 

2 to 14 set the stage for the actual proof by expanding definitions and tidying up the sequent. When the 

strategy is applied to lemma newJob-preserves-pos-w and control has reached line 14 of the strategy, the 

current sequent is 

[-11 ASSUMPTIONS 

[-21 INIT(b! l(0) 

[-SI [I action2temporal (stutter (ACTIONS) ) 

[-41 (FORALL (cc : c) : pos-v-body (cc , nov) ) 

(-5) (EXISTS (~1: c): 

(neuJob-guard(c1, nov)) 

AND 

((w(c1) (next) = 1 + w(c1) (now)) 

AND 

((FORALL (other: c): 

((other) /= (cl)) IMPLIES 

(v(other) (next) = (v(other) (nov)))))) 1 

I - -- - - - - 

[l] (FORALL (cc: c): pos-u-body(cc, next)) 

The existential quantification in formula -5 and the universal quantification in formula 1 are then skolemized by the steps in lines 18 and 22. 

When the work was being carried out, the only way to refer to formulas in PVS was by their number 

in the current sequent. Since we did not want to try to predict this number, we include the formulas as 

strings in the generated strategies. Each string is parsed and type checked when the strategy is run, and 

the resulting formula is compared for equality with each formula in the sequent. This is done by escaping to 

Common Lisp from the PVS strategy language. 
Generating Proof-Specific Strategies for PVS 97 

1: (defstep pos-w-is-invariant 0 

2: (then* (lemma "invariant-rule") 

3: (repeat (inst?)) 

4: (split 

5: (skosimp*) 

6: (branch (split) 

7: ((then* (expand l'INIT1f) 

8: (ground) 1 

9: (then* (skosimp*) 

10: (lemma "newJob-preserves-pos-w") 

11: (expand "preserves") 

12: (inst -1 "b!l") 

13: (split -1) 

14: (inst -1 "n!l") 

15: (lemma "balance-preserves-pos-wq') 

16: (expand "preserves") 

17: (inst -1 tub!ll') 

18: (split -1) 

19: (inst -1 "n!l") 

20: (expand "ACTIONS") 

21: (bddsimp) 

22: (ground) 1) 1) 

23: "Top level strategy. " 

24: "Top level strategy. ") 

Fig. 5. Top level strategy for pos-w 

Next, the proof is split into two cases depending on whether the two skolem constants just introduced 

denote the same value or not. In Disco terms, we are investigating separately the object that participates in 

the action, and those that do not participate. This is done by the steps in lines 26 and 27. Figures 7 and 8 

show the details suppressed in lines 28 and 29. 

Figure 7 shows the strategy fragment taking care of participating objects. First, formula -4 is instantiated 

by line 1 in the strategy. Line 2 expands the definition of pos-w-body. At line 4, the equality w(cl)(next) = 1 

+ w(cl)(now) is used as a rewrite rule, line 5 removes the now redundant universally quantified antecedent, 

and finally the guard of the action is expanded at line 6. 

c-11 CC = cl 

After this part of the strategy has been run, the current sequent is 

[-21 ASSUMPTIONS 

[-31 INIT(b! l(0) 1 

C-41 [I action2temporal (stutter (ACTIONS) 

C-51 w(cl)(now) >= 0 

(-6) w(cl)(now) < 10 

[I] 1 + w(cl)(now) >= 0 

which the decision procedures of PVS recognize as valid. 

The strategy fragment for nonparticipating objects (Figure 8) is similar. In this branch of the proof, the 

equality to be used as a rewrite rule is contained within a universal quantification, so it must be suitably 

instantiated before use. 

I - --- -- - 

This part of the strategy produces the sequent 

[-I] (~(cc) (next) = (~(cc) (now))) 

[-21 ASSUMPTIONS 

[-31 INIT(b! l(0)) 

[ -41 [] act ion2t emporal (stutter (ACTIONS) ) 
98 Pertti Kellomaki 

1: (then* (pdp-instantiate-not "c1" nil 

2: (expand "pos-w-body") 

3: (flatten) 

4: (object-replace "c1" "w" t) 

5: (hide-quantifications) 

I 6: (expand "neuJob-guard") 

'I (FORALL (cc: c) :pos-w-body(cc ,now)) 'I) 

1: (defstep newJob-preserves-pos-u (1 

2: 

3: 

4: 

5: 

6: 

7: 

8: 

9: 

10: 

11: 

12: 

13: 

15: 

16: 

17: 

18: 

19: 

20: 

21: 

22: 

23: 

25: 

26: 

28: 

29: 

14: 

24 : 

27: 

(then* (expand "preserves") 

(skosimp* 

;; introduce names now and next for the unprimed 

;; and primed states 

(name "now" "b!l(n!l)") (replace -1 *) (hide -1) 

(name "next" "b!l(n!l+l)") (replace -1 *) (hide -1) 

;; expand the definitions of the assertion 

;; and the action 

(expand "pos-w") (expand "neuJob") (flatten) 

(then* 

;; introduce skolem constant cl for the 

;; participant cl 

(skolemize-action ("cl")) (flatten) 

;; introduce skolem constant cc for the 

;; quantified variable in primed pos-u 

(skolemize "cc" nil "(FORALL(cc:c) : 

pos-w-body(cc,next))") 

;; consider separately the cases for an object that 

;; participates or does not participate in the action 

(spread 

(case-replace "cc = ~1~~) 

( handle participating objects 

handle all other objects) ))) 

30: "Automatically generated strategy for proving: 

31: "Try to prove: pos-u and newJob => pos-Y'") 

pos-w and newJob => pos-u"' 

Fig. 6. Strategy to establish that newJob preserves pos-w 
Generating Proof-Specific Strategies for PVS 99 

1: (then* (pdp-instantiate-not 

2: llccll nil 

3: 

4: 

5: 

6: (FORALL(other: c) : ((other)/=(cl)) 

7: (spread (split) 

8: ((then* (expand "pos-w-body") 

9: (flatten) 

10: (object-replace "cc" "w" t) 

11: (hide-quantifications) 

12: (expand "neuJob-guard") ) 

13: (ground) 1) 1 

I' (FORALL(cc: c) :pas-w-body(cc,now)) ") 

lIcc" 

(pdp-instantiate-not 

nil 

IMPLIES(w(other) (next)= (w(other) (now) )))") 

Fig. 8. Strategy fragment for nonparticipating objects 

(-53 

(-6) 

C-71 

C-81 

I C-91 

(FORALL (cc: c) : w(cc) (now) >= 0) 

w(cc)(now) >= 0 

(newJob-guard (cl , now) ) 

(w(cl)(next) = 1 + w(cl)(now)) 

((FORALL (other: c) : 

((other) /= cl) IMPLIES 

(w(other) (next) = (w(other) (now))))) 

cc = cl 

w(cc) (now) >= 0 

I which is immediately recognized as valid by the decision procedures (this sequent is not even shown to the 

user). 

I 4.2 Removing Quantifications 

The strategy generator uses a simple approach to produce ground formulas from the quantified formulas in 

a sequent. Let 

Q 101 : e202 : . . . Q ,on : P(01,. . . ,on) (3) 

be a Disco assertion where each Q i denotes either universal or existential quantification and each oi denotes 

a formal name. A Disco action maps to an existentially quantified formula of the form 1 

Consider the proof obligation 

[-11 Q 101 : Q202 : . . . Q,O, : P(o1,. . . ,on) 

[-21 $a,. . . ,Pm : Ah,. . . ,Pm) 

[l] &lo1 : Q202 : ... QnOn : P'(01, ...) 0,) 

I 

I 

t. (5) 

where P' stands for the value of P in the next state. Our ultimate goal is to use the equations within A to 

rewrite P' in terms of unprimed variables. We can, however, only do this for ground formulas. The problem 

then is to perform a series of skolemizations and instantiations to produce suitable ground formulas in the 

sequent. 
100 Pertti Kellomaki 

Skolemizing the action in (5) leaves us with 

[l] Q 101 : e202 : . . . Q ,on : P‘(o1,. . . ,on) 

where we have used the names pl, . . . ,pn of the quantified variables as names of the skolem variables. 

We can now skolemize either formula [-11 or formula [l], depending on whether the outermost quantification is existential or universal. For the sake of illustration, let us assume that 01 is existentially quantified. 

After skolemization we get the following sequent: 

[-I] Q2oz : . . . Q,o, : P(01,. . . ,on) 

[-21 d(pl,...,pm) 

[l] 301 : Q 202 : . . . Q no, : P’(01,. . . ,on). 

Iwhere 01 is a new skolem constant. 

Having introduced 01, we can now instantiate formula [l] with it. This gives us 

[-11 e202 : . . . Q,On : P(o1,. . . ,on) 

[-2] A(p1,. . . ,~m) 

[l] 301 : Qzoz : . . . QnOn : P’(01,. . . ,on) 

[2] &2@ : . . . Qnon : P‘(o1,. . . ,on) 

I- 

(7) 

Ignoring formula [l] for the moment, we have now effectively removed the outermost quantification from 

the original formulas. Repeating this process finally results in ground instances of P and P’. The ground 

instances of P‘ can then be rewritten using the equations in the action. 

If further skolemizations introduce skolem constants with the same type as 01, formula [l] can be instantiated with them, possibly facilitating new skolemizations. The skolem constants pl, . . . , p, introduced when 

skolemizing the action can also be used for instantiating formulas. 

This skolemization-instantiation process either continues forever, or it terminates with all possible combinations of skolem constants for P and P’. It is easy to construct an example where our algorithm loops 

forever: any assertion containing both a universal and an existential quantification over the same type results 

in a loop. 

This kind of looping is easily detected when generating strategies. When a skolem constant is being 

introduced, the strategy generator tries to use the name of the quantified variable. If a skolem constant with 

the same name already exists, the generator prompts the user for a fresh name. A loop thus manifests itself as 

constant prompting for fresh names. Such a failure of the strategy generator suggests that a straightforward 

proof attempt using the same ideas will also fail. 

5 Discussion 

The main reason we chose to use PVS was the high degree of low level automation, as our proofs mostly 

consist of propositional logic and simple arithmetic reasoning. We were not willing to give up the low level 

automation for a more expressive strategy language. 

We compensate for the limited expressiveness of the PVS strategy language by performing the required 

computations beforehand. The effects of the computation are carried out when the generated strategy is 

executed. The approach is not very elegant, but it demonstrates that in some cases it is possible to use 

offline computation to overcome the constraints of a restricted strategy language. 

The largest case study done with the system is a distributed communication protocol [5,11]. The protocol 

implements a token ring over a shared bus, and it recovers from station failures by removing failed stations 

from the ring. We verified an invariant stating that all the active stations agree on which stations are still in 
Generating Proof-Specific Strategies for PVS 101 

the ring, with the exception of those stations that have not yet received a broadcast message updating the 

list of active stations. 

Verifying the invariant took approximately one and a half hours run time on a Sparc Server 670 MP 

with 114MB memory. Four subgoals were left for the user to handle, all of them requiring instantiation of an 

existentially quantified variable. Completing these subgoals took about twenty minutes, bringing the elapsed 

time to around two hours. This does not include the time spent in finding the proof for the four subgoals. 

The major problem with our approach is the size of the generated strategies. The size of the specification 

for the case study is little over 500 lines of Disco, which maps to about 7kB of unformatted, uncommented 

PVS. The specification consists of nineteen actions. The strategies generated for this specification are approximately l0OkB in size. The size could be decreased significantly by using the formula labeling feature 

present in later versions of PVS, but still the size of strategies would be problematic for larger specifications. 

A much better approach would be to generate strategies on the fly, by escaping to Common Lisp to 

construct strategies to be executed by PVS as strategy language forms. However, in constructing the strategies 

one might require information not readily available in the current sequent (e.g. the set of skolem constants 

denoting participants of the action). This information would need to be passed down into subgoals. 

Unfortunately the strategy generator is obsolete, as it depends on a now abandoned version of the Disco 

compiler. It would not be technically difficult to write a new back end for the current Disco compiler to 

produce PVS, more difficult would be to obtain academic funding for the work. 

6 Conclusions 

We have described how invariant proofs of Disco specifications were partly automated by generating PVS 

strategies. Each generated strategy contains the proof commands needed to carry out the top levels of a 

proof that a specific action preserves a specific invariant. 

A user can instruct PVS first to run a generated strategy, and then to apply e.g. ground or grind to each 

of the subgoals produced by the strategy. Only the subgoals not resolved by PVS are then presented to the 

user for interactive proving. 

The work demonstrates that strategy generation can be of practical help in verification. However, the 

size of the generated strategies suggests that strategy generation should occur on the fly rather than offline. 

References 

1. 

2. 

3. 

4. 

5. 

6. 

7. 

8. 

9. 

The Disco project WWW page. At http://disco.cs.tut.fi on the World Wide Web, 2003. 

R. J. R. Back and R. Kurki-Suonio. Distributed cooperation with action systems. ACM Zkansactions on Programming Languages and Systems, 10(4):513-554, October 1988. 

Michael J. C. Gordon. HOL: A proof generating system for higher-order logic. In Graham Birtwistle and P. A. 

Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 73-128. Boston Kluwer Academic 

Publishers, 1988. 

H.-M. Jiirvinen, R. Kurki-Suonio, M. Sakkinen, and K. Systa. Object-oriented specification of reactive systems. In 

Proceedings of the 12th International Conference on Software Engineering, pages 63-71. IEEE Computer Society 

Press, 1990. 

Pertti Kellomdci. Analysis of a stabilizing protocol. Licentiate of Technology thesis, Tampere University of 

Technology, 1994. http://www.cs.tut.fi/"pk/papers.html. 

Pertti Kellomdci. Mechanical Verification of Invariant Properties of Disco Specifications. PhD thesis, Tampere 

University of Technology, 1997. 

Pertti Kellomaki. Verification of reactive systems using Disco and PVS. In John Fitzgerald, Cliff B. Jones, and 

Peter Lucas, editors, FME'97: Industrial Applications and Strengthened Foundations of Formal Methods, number 

1313 in Lecture Notes in Computer Science, pages 589-604. Springer-Verlag, 1997. 

Reino Kurki-Suonio. Fundamentals of object-oriented specification and modeling of collective behaviors. In 

H. Kilov and W. Harvey, editors, Object-Oriented Behavioral Specifications, pages 101-120. Kluwer Academic 

Publishers, 1996. 

Leslie Lamport. The temporal logic of actions. ACM Tkansactions on Programming Languages and Systems, 

16(3):872-923, May 1994. 
102 Pertti Kellomaki 

10. Sam Owe, John Rushby, Natrajan Shankar, and Riedrich von Henke. Formal verification of fault-tolerant 

architecures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107-125, 

February 1995. 

11. Leo Sintonen. Event driven bus architecture for bounded area networks. In Proceedings of the 16th Annual 

Conference of IEEE Industrial Electronics Society, pages 539--541, Pacific Grove, California, November 27-30 

1990. 
Developing Strategies for Specialized Theorem Proving about 

Untimed, Timed, and Hybrid 1/0 Automata * 

Sayan Mitral and Myla Archer2 

MIT Laboratory for Computer Science, 

200 Technology Square, Cambridge, MA 02139 

mitrasBtheory.lcs.mit.edu, 

Washington, DC 20375 

archerBitd.nrl.navy.mil 

Code 5546, Naval Research Laboratory, 

Abstract. In this paper we discuss how we intend to develop a specialized theorem proving environment for the Hybrid 1/0 Automata (HIOA) framework [7] over the PVS [ll] theorem prover, and some 

of the issues involved. In particular, we describe approaches to using PVS that allow and encourage the 

development of useful proof strategies, and note some desired PVS features that would further help us 

to do so for our HIOA environment. 

1 Introduction 

Interest in specialized theorem proving environments has emerged from various application domains [3,4,6, 

11. A major motivation for developing such environments is to relieve the developers and verification engineers 

environments also help expert users of theorem provers by replacing repetitive proof patterns with strategies, 

and by making it possible to generate human readable proofs. 

We plan to develop a specialized theorem proving environment to be used with the Hybrid 1/0 Automata 

(HIOA) framework. HIOA is a very general framework for modeling systems with both discrete and continuous behavior, and subsumes both the timed and untimed 1/0 automata models. Therefore, any strategies 

and metatheories for HIOA would be applicable to timed and untimed 1/0 automata as well. A theory 

template for specifying HIOAs has been presented in [9]. This formalization of HIOA in PVS is similar to 

the formalization of Lynch-Vaandrager (LV) timed automaton [8] in the Timed Automaton Modeling Environment (TAME) [l]. However, important differences arise in the two formalizations because LV-timed 

automata communicate via shared actions alone, whereas HIOAs also communicate via shared variables. 

Therefore, the evolution of continuous variables is modeled in TAME using time passage actions to capture 

cumulative changes over an interval, while in the HIOA model, the evolution of the continuous state variables 

over time is modeled using trajectories. Our HIOA environment must allow for these differences. 

The rest of this paper is organized as follows: In Section 2 we discuss the main types of proofs which will 

be supported by our HIOA environment and the design issues involved in developing proof strategies for each 

type. In Section 3 we suggest certain new features of PVS which would aid the development of strategies for 

PVS. Finally, we summarize and conclude in Section 4. 

I from mastering the specification language and the proof commands of a general theorem prover. Specialized 

l 

I 

I 

j 

i 2 Supported Proof Types 

Apart from simplifying direct proofs of properties, the HIOA proving environment will provide special strategies for mechanizing inductive invariant proofs and abstraction (e.g., simulation) proofs for timed, hybrid 

and untimed 1/0 automata. Apart from TAME, another theorem proving environment has been developed, 

based on Isabelle, which mechanizes invariant proofs for 1/0 automata [lo]. In [2], the authors present a 

simulation proof of a leader election protocol in PVS. However, we have not come across any work which 

addresses the development of strategies for mechanizing simulation proofs. 

* Funding for this research has been provided by ONR 
104 Sayan Mitra and Myla Archer 

2.1 Inductive Proofs 

The approach we intend to take for supporting inductive invariant proofs is derived from the Timed Automaton Modeling Environment (TAME) [l]. As in TAME, we will develop a parameterized theory machine 

which defines the reachable states of an automaton in terms of its states, initial states, actions and (in case of 

hybrid 1/0 automata) activities [9]. This theory will also establish the theorem that allows proving invariants 

inductively. We will also develop a general theory template which can be instantiated with particular state 

variables and actions (optionally, activities) to obtain an automatonNume-decls theory describing the automaton. The automatonName-decls theory will import an instance of the theory machine with the declared 

states and actions as parameters. Instantiation of the theory machine defines reachability and the induction 

theorem for the particular automaton. All the invariants and the associated lemmas of an automaton will 

be collected and proved in a theory named automatonName-inv. 

The advantages of this (TAME) approach are as follows: (1) It is possible to write generic strategies 

which work for all automata specified using the template. The strategies for induction are tailored for the 

defined automaton template, and are defined in the file pvs-strategies. Therefore, (2) the user can use 

the specialized environment from within the PVS system. Finally, (3) it is easy to generate human readable 

proofs using the generic strategies, provided that the strategies implement proof steps meaningful to humans. 

A slightly different approach has been taken by the developers of Disco [6,5], where the PVS specification 

of the automaton is processed by a “generator” to produce the proof scripts. One advantage of this approach, 

due to the clearly defined interface between the theorem prover (PVS) and the specialized environment 

(Disco), is that the generated proof scripts are relatively insensitive to the modifications of the internals of 

theorem prover commands and data structures. 

However, we would like our strategies to be directly applicable to all automata specified with our template 

theory. The success of our approach does depend on access to the data-structures in the proof state maintained 

by PVS, and the consistency of the behavior of PVS proof commands. We discuss the PVS support necessary 

to achieve this in Section 3. 

2.2 Abstraction Proofs 

Given automata A and C, it is often useful for the purposes of verification to show that there exists an 

abstraction relation between them. Several kinds of abstraction relation, e.g., homomorphism, refinement, 

forward and backward simulation, etc., are described in the literature, and there may also be other such 

relations of interest. 

Abstraction proofs can be performed directly by specifying both automata A and C, and the abstraction 

relation between them, within the same PVS theory. However, this approach makes it difficult to construct 

generic strategies for automating the proofs, and to use invariants which have been proved separately for the 

individual automata. 

Instead, we intend to make use of PVS support for theory parameters, as follows. Two parameters A 

and C of the type automaton theory (Figure 1) can be passed as parameters to the theory abstraction 

(Figure 2), which also takes the abstraction relation absrel and the action map actmap as parameters. 

The theory abstraction, which somewhat resembles the theory grouphomomorphism in [12] for setting up 

proofs of homomorphism between groups, defines the abstraction relations between the two interpretations 

of the automaton theory. To pass actual theory parameters to grouphomomorphism, the various elements 

of the group theories must be named: the members of the groups, identities and composition operators, etc. 

But, when individual automata follow the same naming conventions as in the theory automaton, a shortcut 

is in principle possible in passing actual theory parameters to abstract ion: because the various elements of 

the actual parameters can be matched to the formal parameters syntactically, only the actual theory names 

need to be provided. A modification to PVS that will allow this shortcut is under construction at SRI. 

The actmap relation in the theory abstraction maps an action of the concrete automaton C to an 

action of the abstract automaton A. The axioms vis-ax and invisax that indicate that the visible actions 

in C map to visible actions in A and invisible (i.e., internal) actions in C map to the stutter step in A, 

become proof obligations when abstraction is instantiated. At the same time, the axioms stutter-transax 

and stutter-enabledax from the theory automaton will become proof obligations with respect to both 

automaton theory instances. 
Developing Strategies for Specialized Theorem Proving 105 

automaton: THEORY 

BEGIN 

actions : TYPE+; 

stutter: actions; 

visible (a:actions) : bool; 

states : TYPE+; 

start (s:states) : bool; 

enabled (a:actions, s:states) : bool; 

trans (a:actions, s:states) : states; 

stutter-trans-ax: AXIOM (FORALL (s:states): (trans(stutter,s) = SI); 

stutter-enabled-ax: AXIOM (FORALL (s:states): (enabled(stutter,s))); 

reachable (s:states) : bool; 

equivalent (sl, s2: states) : bool; 

END automaton 

Fig. 1. The automaton abstract theory 

abstraction [ A, C: automaton, 

actmap: [C.actions -> A.actions1, 

absrel: [C.states, A.states -> boo11 1 : THEORY 

BEGIN 

a-C : VAR C.actions; 

a-A : VAR A.actions; 

s-C, sl-C, s2-C: VAR C.states; 

s-A : VAR A.states; 

vis-ax: AXOIM 

(FORALL a-C: C.visible(a-C) => A.visible(actmap(a-C))); 

invis-ax: AXIOM 

(FORALL a-C: NOT(C.visible(a-C)) => (actmap(a-C) = A.stutter)) ; 

weak-refinement-base : bool = 

(FORALL s-C. s-A: 

C.start(s-C) & absrel(s-C, s-A) 

=> A. start (s-A) 1 ; 

weak-refinement-step : bool = 

C.reachable(s-C) & 

C.equivalent(s-C, sl-C) & C.visible(a-C) & C.enabled(a-C, sl-C) & 

A. reachable (s-A) & 

absrel (sl-C, s-A) 

(FORALL s-C, sl-C. a-C, s-A: 

=> A.enabled(actmap(a-C), s-A) & 

(EXISTS (s2-C: C.states): 

C.equivalent(C.trans(a-C, sl-c), s2-C) & 

absrel (s2-C, A. trans (actmap(a-C) , s-A) 1) 1 ; 

weak-refinement : bool = weak-refinement-base &.weak-refinement-step; 

END abstraction 

Fig. 2. The abstraction theory 
106 Sayan Mitra and Myla Archer 

For abstraction proofs the theory abstraction assumes a role analogous to that of the theory machine 

in the case of induction proofs, in that it will define the abstraction relations and also establish the theorems (e.g., concerning trace inclusion) that are the consequences of the existence of such relations between 

pairs of automata. In Figure 2, only one sort of refinement relation has been defined; in practice, the theory abstraction will define all possible useful abstraction relations between the two automata. The theory 

abstraction will thus provide us with a starting point for developing generic strategies for proving abstraction relations. 

3 PVS Support 

In this section we suggest some PVS features which would be helpful for writing strategies, particularly for 

the above types of proofs. 

1. 

2. 

3. 

4. 

4 

Naming in theory interpretations. The abstraction proofs involve many related theories, for example 

different instances of uutomatonName-decl, automatonNume-inv, machine, etc. It is difficult to write 

general strategies that involve formulas or definitions in multiple theories: the user often has to identify 

the particular theory instances explicitly. It would be useful for strategy writers if PVS provided well 

documented naming conventions and functions for determining theory instances associated with names, 

and supported the automatic context-based selection by user strategies of appropriate theory instances 

for names. 

Functions to access information in specification and in proof states. A strategy often depends 

on the nature of the automaton specification. It can also make choices based on the current proof state. 

The CLOS structure used by PVS provides functions to access various slots of the current proof state 

object. However, these are not guaranteed to be fixed, and indeed can sometimes change dynamically. 

For writing strategies it would be helpful if functions to access the definitions in a particular theory-for 

example the invariance lemmas or the action definitions-and functions for accessing parts of a sequent, 

formulae, etc., were provided as a part of a PVS strategy language. 

Documentation of implementation details in PVS proof commands. The LISP/CLOS functions used in writing the internal PVS strategies (e.g., induct) are not well documented. Many of these 

functions, for example typep, tc-eq, can be useful for writing new strategies. Therefore, proper documentation of these functions would save effort and help new strategy writers learn the art. 

Improved support for maintaining compatibility with PVS. The effects of some basic PVS 

commands (e.g. SKOLEM, EXPAND) have altered over PVS versions owing largely to changes in PVS’s 

decision procedures and their use in conjunction with such basic steps. As a result, strategies developed 

for older versions of PVS do not always work in the newer PVS versions. Therefore, it is highly desirable 

to provide a feature in future versions of PVS that would allow strategies to invoke prover commands 

and get the same result as in some specified previous version. Because most changes in effects appear to 

involve the decision procedures and their hidden uses, there should at the very least be optional versions 

of proof steps that decouple them from any use of these procedures. 

Conclusions 

Domain specific theorem proving is a practical means for harnessing the power of mechanical theorem provers 

for system design and analysis. In this paper we have outlined design principles for the development of proof 

strategies of a specialized theorem proving environment for hybrid 1/0 automata based on PVS. Our aim 

is to make the more complex component of the environment-the proof strategies-generic, based on a 

specific HIOA template, leaving the simpler component-the specification-to be written by instantiating 

the template. We have outlined the support we believe would help us develop effective generic strategies. 

Acknowledgements 

We wish to thank John Rushby and Natarajan Shankar of SRI for helpful discussions about our plans for a 

framework supporting generic strategies for abstraction relations between automata. We thank Sam Owre 
Developing Strategies for Specialized Theorem Proving 107 

and Natarajan Shankax for undertaking enhancements to PVS that will support our plans. We also thank 

Nancy Lynch of MIT for helpful discussions and her comments about the design of the specification language 

for HIOA. 

References 

1. Myla Archer. TAME: PVS Strategies for special purpose theorem proving. Annals of Mathematics and Artificial 

Intelligence, 29(1/4), February 2001. 

2. M. Devillers, D. Griffioen, J. Romijn, and F. Vaandrager. Verification of a leader election protocol-formal 

methods applied to IEEE 1394. Formal Methods in System Design, 16(3):307-320, June 2000. 

3. Urban Engberg. Reasoning in the Temporal Logic of Actions - The Design and Implementation of an Interactive 

Computer System. PhD thesis, University of Aarhus, Denmark, 1995. 

4. S. Kalvala. A Formulation of TLA in Isabelle. In E.T. Schubert, P.J. Windley, and J. Alves-Foss, editors, 

8th International Workshop on Higher Order Logic Theorem Proving and its Applications, volume 971, pages 

214-228, Aspen Grove, Utah, USA, 1995. Springer-Verlag. 

5. Pertti Kellomaki. Mechanizing invariant proofs of joint action systems. In Proceedings of the Fourth Symposium 

on Programming Languages and Software Tools, pages 141-152, Visegrad, Hungary, June 1995. 

6. Pertti Kellomaki. Mechanical verification of Disco specifications. In Israeli-Finnish Binational Symposium on 

Specification, Development, and Verification of Concurrent Systems, Technion, Haifa, January 1996. 

7. Nancy Lynch, Roberto Segala, and Frits Vaandraager. Hybrid 1/0 automata. To appear in Information and 

Computation. Also, Technical Report MIT-LCS-TR-827d, MIT Laboratory for Computer Science Technical Report, Cambridge, MA 02139, January 13, 2003. 

theory.lcs.mit.edu/tds/papers/Lynch/HIOA-final.ps. 

8. Nancy Lynch and Frits Vaandrager. Forward and backward simulations - part ii: Timing-based systiems. Information and Computation, 128( 1):l-25, July 1996. 

9. Sayan Mitra. HIOA+: Specification language and proof tools for hybrid systems, 2003. Submitted for publication, 

http://theory.lcs.mit.edu/ mitras/research/LCPTHIOA.ps. 

10. Olaf Muller. A Verification Environment for I/O Automata Based on Formalized Meta-Theory. PhD thesis, 

Technische Universitat Munchen, Sept. 1998. 

11. S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M.K. Srivas. PVS: Combining specification, proof checking, 

and model checking. In Rajeev Alur and Thomas A. Henzinger, editors, Computer-Aided Verification, CAV '96, 

number 1102 in Lecture Notes in Computer Science, pages 411-414, New Brunswick, NJ, July/August 1996. 

Springer-Verlag. 

12. S. Owre and N. Shankar. Theory interpretations in PVS. Technical report, Computer Science Lab., SRI Intl., 

Menlo Park, CA, 2001. 
I Adams, Andrew 84 

Archer, Myla 16,103 

Dennis, Louise 84 

Di Vito, Ben 16,43 

Hurd, Joe 56 

Kellomaki, Pertti 91 

I 

I 

Author Index 

Kirchner, Florent 69 

Mitra, Sayan 103 

Muiioz. Cksar 16 

Owe, Sam 1 

Shankar, Natarajan 1 
REPORT DOCUMENTATION PAGE 

I 

The public re orting burden for this collection of information is estimated to average 1 hour per response including the time for reviewing instructions. searching existing data sources, 

gathering antmaintaining the data needed. and completing and reviewing the collection of information Send comments regarding this burden estimate or any other aspect of this collection 

of informairon, including sug siions for reducing this burden, to Department of Defense, Washington Headquarters Services. Directorate for Information Operations and Reports 

(0704-0188). 1215 Jefferson &vis Highway. Sulte 1204. Arlin on VA 22202-4302 Respondents should be aware that notwlthstanding any other provision of law, no person shall be 

subject to any penalty for failing to comply wlth a collection of in&rnatim If It does not display a currently valid OMB control number 

PLEASE DO NOT RETURN YOUR FORM TO THE ABOVE ADDRESS. 

1. REPORT DATE (OD-MM-YWY) I 2. REPORT TYPE 13. DATES COVERED (From - To) 

Form Approved 

OMB No. 07044188 

01-09-2003 

~~ 

5e.TAsK”MBER 

5f. WORK UNIT NUMBER 

23-704-03-50 

Conference Publication I 

I 

7. PERFORMING ORGANIZATION NAME(S) AND ADDRESS(ES) 

NASA Langley Research Center 

Hampton, VA 23681-2199 

9. SPONSORING!MONITORING AGENCY NAME(S) AND ADDRESS(ES) 

National Aeronautics and Space Administration 

Washington, DC 20546-0001 

4. TITLE AND SUBTITLE 

Design and Application of Strategies/Tactics in Higher Order Logics 

6. AUTHOR(S) 

Myla Archer, Ben Di Vito, and Cbar Muiioz (Editors) 

#. PERFORMING ORGANIZATION 

L-18328 

REPORT NUMBER 

5a. CONTRACT NUMBER 

5b. GRANT NUMBER 

5c. PROGRAM ELEMENT NUMBER 

5d. PROJECT NUMBER 

IO. NbS*I SPONSOWMONITOR’S ACRONYM(S) 

17. LIMITATION OF 

ABSTRACT 

uu 

11. SPONSOWMONITOR’S REPORT 

NUMBER(S) 

NASAICP-2003-212448 

18. NUMBER 19a. NAME OF RESPONSIBLE PERSON 

OF 

PAGES I 

STI Help Desk (email: help0sti.nasa.gov) 

l9b. TELEPHONE NUMBER (include area code) 

118 (301) 621-0390 

12. DlSTRlBUTION/AVAILABILITY STATEMENT 

Unclassified-Unlimited 

Subject Category 59 

Availability: NASA CAS1 (301) 621-0390 

13. SUPPLEMENTARY NOTES 

Distribution: Standard 

U 

An electronic version can be found at http://techreports.larc.nasa.govAtrs/ or http://ntrs.nasa.gov. 

14. ABSTRACT 

STRATA 2003, the First International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics, was held in 

Rome, Italy on September 8, 2003. This event was a satellite workshop of the 16th International Conference on Theorem Proving in 

Higher Order Logics, TPHOLs 2003. Papers were solicited on all aspects of development and application of user-defined strategies or 

tactics in higher order logic theorem provers. A particular emphasis was placed on contributions that describe either experience with 

PVS strategies or comparisons with strategy and tactic development in other theorem proving systems. Included was an invited paper 

from the staff of SRI International, the developers of the PVS tools. Also included was the text of a PVS strategy-writing tutorial. 

During the workshop, each paper was presented by one of its authors. 

U U 

15. SUWECTTERMS 

Formal Methods, Theorem Proving, Proof Strategies