%!PS-Adobe-3.0
%%BoundingBox: 54 72 558 720
%%Creator: Mozilla (NetScape) HTML->PS
%%DocumentData: Clean7Bit
%%Orientation: Portrait
%%Pages: 9
%%PageOrder: Ascend
%%Title: http://www.dcs.napier.ac.uk/~helen/pubs/iwfm97/irishfm.htm
%%EndComments
%%BeginProlog
[ /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef
/.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef
/.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef
/.notdef /.notdef /space /exclam /quotedbl /numbersign /dollar /percent /ampersand /quoteright
/parenleft /parenright /asterisk /plus /comma /hyphen /period /slash /zero /one
/two /three /four /five /six /seven /eight /nine /colon /semicolon
/less /equal /greater /question /at /A /B /C /D /E
/F /G /H /I /J /K /L /M /N /O
/P /Q /R /S /T /U /V /W /X /Y
/Z /bracketleft /backslash /bracketright /asciicircum /underscore /quoteleft /a /b /c
/d /e /f /g /h /i /j /k /l /m
/n /o /p /q /r /s /t /u /v /w
/x /y /z /braceleft /bar /braceright /asciitilde /.notdef /.notdef /.notdef
/.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef
/.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef
/.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef
/space /exclamdown /cent /sterling /currency /yen /brokenbar /section /dieresis /copyright
/ordfeminine /guillemotleft /logicalnot /hyphen /registered /macron /degree /plusminus /twosuperior /threesuperior
/acute /mu /paragraph /periodcentered /cedilla /onesuperior /ordmasculine /guillemotright /onequarter /onehalf
/threequarters /questiondown /Agrave /Aacute /Acircumflex /Atilde /Adieresis /Aring /AE /Ccedilla
/Egrave /Eacute /Ecircumflex /Edieresis /Igrave /Iacute /Icircumflex /Idieresis /Eth /Ntilde
/Ograve /Oacute /Ocircumflex /Otilde /Odieresis /multiply /Oslash /Ugrave /Uacute /Ucircumflex
/Udieresis /Yacute /Thorn /germandbls /agrave /aacute /acircumflex /atilde /adieresis /aring
/ae /ccedilla /egrave /eacute /ecircumflex /edieresis /igrave /iacute /icircumflex /idieresis
/eth /ntilde /ograve /oacute /ocircumflex /otilde /odieresis /divide /oslash /ugrave
/uacute /ucircumflex /udieresis /yacute /thorn /ydieresis] /isolatin1encoding exch def
/c { matrix currentmatrix currentpoint translate
3 1 roll scale newpath 0 0 1 0 360 arc setmatrix } bind def
/F0
/Times-Roman findfont
dup length dict begin
{1 index /FID ne {def} {pop pop} ifelse} forall
/Encoding isolatin1encoding def
currentdict end
definefont pop
/f0 { /F0 findfont exch scalefont setfont } bind def
/F1
/Times-Bold findfont
dup length dict begin
{1 index /FID ne {def} {pop pop} ifelse} forall
/Encoding isolatin1encoding def
currentdict end
definefont pop
/f1 { /F1 findfont exch scalefont setfont } bind def
/F2
/Times-Italic findfont
dup length dict begin
{1 index /FID ne {def} {pop pop} ifelse} forall
/Encoding isolatin1encoding def
currentdict end
definefont pop
/f2 { /F2 findfont exch scalefont setfont } bind def
/F3
/Times-BoldItalic findfont
dup length dict begin
{1 index /FID ne {def} {pop pop} ifelse} forall
/Encoding isolatin1encoding def
currentdict end
definefont pop
/f3 { /F3 findfont exch scalefont setfont } bind def
/F4
/Courier findfont
dup length dict begin
{1 index /FID ne {def} {pop pop} ifelse} forall
/Encoding isolatin1encoding def
currentdict end
definefont pop
/f4 { /F4 findfont exch scalefont setfont } bind def
/F5
/Courier-Bold findfont
dup length dict begin
{1 index /FID ne {def} {pop pop} ifelse} forall
/Encoding isolatin1encoding def
currentdict end
definefont pop
/f5 { /F5 findfont exch scalefont setfont } bind def
/F6
/Courier-Oblique findfont
dup length dict begin
{1 index /FID ne {def} {pop pop} ifelse} forall
/Encoding isolatin1encoding def
currentdict end
definefont pop
/f6 { /F6 findfont exch scalefont setfont } bind def
/F7
/Courier-BoldOblique findfont
dup length dict begin
{1 index /FID ne {def} {pop pop} ifelse} forall
/Encoding isolatin1encoding def
currentdict end
definefont pop
/f7 { /F7 findfont exch scalefont setfont } bind def
/rhc {
{
currentfile read {
dup 97 ge
{ 87 sub true exit }
{ dup 48 ge { 48 sub true exit } { pop } ifelse }
ifelse
} {
false
exit
} ifelse
} loop
} bind def
/cvgray { % xtra_char npix cvgray - (string npix long)
dup string
0
{
rhc { cvr 4.784 mul } { exit } ifelse
rhc { cvr 9.392 mul } { exit } ifelse
rhc { cvr 1.824 mul } { exit } ifelse
add add cvi 3 copy put pop
1 add
dup 3 index ge { exit } if
} loop
pop
3 -1 roll 0 ne { rhc { pop } if } if
exch pop
} bind def
/smartimage12rgb { % w h b [matrix] smartimage12rgb -
/colorimage where {
pop
{ currentfile rowdata readhexstring pop }
false 3
colorimage
} {
exch pop 8 exch
3 index 12 mul 8 mod 0 ne { 1 } { 0 } ifelse
4 index
6 2 roll
{ 2 copy cvgray }
image
pop pop
} ifelse
} def
/cshow { dup stringwidth pop 2 div neg 0 rmoveto show } bind def
/rshow { dup stringwidth pop neg 0 rmoveto show } bind def
%%EndProlog
%%Page: 1 1
%%BeginPageSetup
/pagelevel save def
54 0 translate
%%EndPageSetup
newpath 0 72 moveto 504 0 rlineto 0 648 rlineto -504 0 rlineto closepath clip newpath
24 f1 0 697.5 moveto
(The Use of Theorem Provers in the Teaching and) show
24 f1 0 669.9 moveto
(Practice of Formal Methods) show
12 f0 0 640.7 moveto
(Helen Lowe) show
12 f0 0 614.1 moveto
(Department of Computing) show
12 f0 0 587.5 moveto
(Napier University) show
12 f0 0 560.9 moveto
(Edinburgh) show
12 f0 0 534.3 moveto
(EH14 1DJ) show
18 f1 0 501.6 moveto
(Introduction) show
12 f0 0 473.7 moveto
(In this paper we describe the use of the XBarnacle proof tool. We have used an earlier version of this) show
12 f0 0 460.4 moveto
(tool, based on the CLAM theorem proving system, for instructing students in proof techniques. We) show
12 f0 0 447.1 moveto
(learnt from this experience and as a consequence built XBarnacle, which although incorporating many) show
12 f0 0 433.8 moveto
(of the original features, and the same underlying theorem prover, employs a different interaction style.) show
12 f0 0 420.5 moveto
(We believe that this style is more in keeping with that needed to develop useful, ) show
12 f2 387.2 420.5 moveto
(useable) show
12 f0 423.8 420.5 moveto
( proof tools for) show
12 f0 0 407.2 moveto
(formal methods practitioners, not just for students.) show
18 f1 0 374.5 moveto
(Automated theorem provers) show
14 f1 0 344.3 moveto
(Automation versus interaction) show
12 f0 0 317.3 moveto
(Interactive theorem provers require the user to determine the steps to carry out, and should perhaps be) show
12 f0 0 304 moveto
(regarded as proof checkers. They are characteristically difficult to use. Complete automation is difficult) show
12 f0 0 290.7 moveto
(to achieve. Automated theorem provers are limited in what they can achieve unaided, and the user often) show
12 f0 0 277.4 moveto
(has a large role to play, essentially in provided the right environment for the system. We report on this) show
12 f0 0 264.1 moveto
(elsewhere, but one example is the use of lemmas in a proof \226 it may be the user\222s perspicuity in spotting) show
12 f0 0 250.8 moveto
(that a lemma is needed, and providing it, that saves a proof attempt from failure.) show
14 f1 0 221.9 moveto
(Tactic-based theorem systems) show
12 f0 0 194.9 moveto
(Tactic-based theorem provers, for example NuPRL \(Constable ) show
12 f2 303.9 194.9 moveto
(et al) show
12 f0 324.9 194.9 moveto
(., 1986\) arose from the need \(for) show
12 f0 0 181.6 moveto
(humans\) to raise the level of interaction. Many are used as interactive systems in which much of the) show
12 f0 0 168.3 moveto
(tedious low level and repetitive steps are carried out automatically, the user providing the high level) show
12 f0 0 155 moveto
(guidance for the proof. This style of theorem prover shows the way to incorporate more automation: if) show
12 f0 0 141.7 moveto
(the reasoning behind the user\222s choices can be encapsulated in a computer program, we may be able to) show
12 f0 0 128.4 moveto
(build automated theorem provers. ) show
14 f1 0 99.5 moveto
(The CLAM-OYSTER system) show
pagelevel restore
showpage
%%Page: 2 2
%%BeginPageSetup
/pagelevel save def
54 0 translate
%%EndPageSetup
newpath 0 72 moveto 504 0 rlineto 0 648 rlineto -504 0 rlineto closepath clip newpath
12 f0 0 709.2 moveto
(The theorem proving system CLAM \(Bundy ) show
12 f2 217.3 709.2 moveto
(et al) show
12 f0 238.3 709.2 moveto
(., 1990\) uses the underlying logic provided by Oyster,) show
12 f0 0 695.9 moveto
(a tactic-based system which is essentially a rational reconstruction of NuPRL. Both Oyster and CLAM) show
12 f0 0 682.6 moveto
(are implemented in Prolog. CLAM\222s tactics are specified in a meta-logic by the pre- and post-conditions) show
12 f0 0 669.3 moveto
(of ) show
12 f2 12.9 669.3 moveto
(methods) show
12 f0 52.8 669.3 moveto
( of the following form:) show
12 f2 0 642.7 moveto
(method) show
12 f0 35.6 642.7 moveto
(\() show
12 f2 39.5 642.7 moveto
(name) show
12 f0 65.4 642.7 moveto
(\() show
12 f2 69.9 642.7 moveto
(Args) show
12 f0 92.5 642.7 moveto
(\),) show
12 f2 0 616.1 moveto
(Input) show
12 f0 25.5 616.1 moveto
(,) show
12 f2 0 589.5 moveto
(Preconditions) show
12 f0 67.3 589.5 moveto
(,) show
12 f2 0 562.9 moveto
(Effects) show
12 f0 32.6 562.9 moveto
(,) show
12 f2 0 536.5 moveto
(Output,) show
12 f2 0 510.3 moveto
(tactic) show
12 f0 0 483.9 moveto
(\).) show
12 f0 0 457.3 moveto
(The ) show
12 f2 22.5 457.3 moveto
(preconditions) show
12 f0 88.5 457.3 moveto
( slot provides a specification of when a tactic is applicable, and the ) show
12 f2 412.4 457.3 moveto
(effects) show
12 f0 443 457.3 moveto
( slot) show
12 f0 0 444 moveto
(computes the output: this may be empty, as when a tactic finishes off a proof \(or a branch of a proof \226) show
12 f0 0 430.7 moveto
(proofs are tree structures in general\); or it may contain one or more sub-goals. ) show
12 f0 0 404.1 moveto
(CLAM uses a technique known as ) show
12 f2 168.8 404.1 moveto
(proof planning) show
12 f0 240.4 404.1 moveto
( \(Bundy, 1988\) to prove theorems automatically. First) show
12 f0 0 390.8 moveto
(a method is found which is ) show
12 f2 132.6 390.8 moveto
(applicable) show
12 f0 183.2 390.8 moveto
( to the original conjecture \(goal\), by checking that the) show
12 f2 0.9 377.5 moveto
(preconditions) show
12 f0 66.9 377.5 moveto
( hold for the goal. The planner then finds suitable methods for the sub-goals in the ) show
12 f2 464.5 377.5 moveto
(Output) show
12 f0 0 364.2 moveto
(slot, and so on until all branches have been proved. ) show
12 f0 0 337.6 moveto
(Although CLAM has been used for other proof methods, the most work has been carried out on proving) show
12 f0 0 324.3 moveto
(theorems by induction. This is because of their difficulty and therefore interest, and because of the) show
12 f0 0 311 moveto
(duality between proof by induction and recursive programs. Proving properties of a recursive function) show
12 f0 0 297.7 moveto
(will involve proof by induction. In what follows, we restrict the discussion to these proofs.) show
14 f1 0 268.8 moveto
(Limitations and potential) show
12 f0 0 241.8 moveto
(CLAM employs a small collection of powerful methods. The methods of induction, generalization,) show
12 f0 0 228.5 moveto
(symbolic evaluation, and ) show
12 f2 123.3 228.5 moveto
(rippling) show
12 f0 161.9 228.5 moveto
( \(of which, more later\)) show
12 f2 270.2 228.5 moveto
( ) show
12 f0 273.2 228.5 moveto
(are all that is needed for the majority of) show
12 f0 0 215.2 moveto
(theorems. It also does surprisingly well without the provision of lemmas: for some theorems where) show
12 f0 0 201.9 moveto
(Nqthm \(Boyer and Moore, 1979\), for instance, would need lemmas provided by the user, CLAM can) show
12 f0 0 188.6 moveto
(prove these \226 often special cases of them \226 in line as part of the main proof. However, users of CLAM,) show
12 f0 0 175.3 moveto
(particularly novices, experience difficulties in using CLAM.) show
12 f0 0 148.7 moveto
(1. Entering new definitions and theorems is problematic. There are not good browsing or editing) show
12 f0 0 135.4 moveto
(facilities. Getting a definition both correct and in a useful form is non-trivial, especially for) show
12 f0 0 122.1 moveto
(inexperienced people.) show
12 f0 0 95.5 moveto
(2. If the planner makes a wrong move, it is not possible to intervene to change it. Very experienced users) show
12 f0 0 82.2 moveto
(have a battery of tricks and workarounds to prevent this \226 novices do not, and it could be argued that) show
pagelevel restore
showpage
%%Page: 3 3
%%BeginPageSetup
/pagelevel save def
54 0 translate
%%EndPageSetup
newpath 0 72 moveto 504 0 rlineto 0 648 rlineto -504 0 rlineto closepath clip newpath
12 f0 0 709.2 moveto
(others should not need to.) show
12 f0 0 682.6 moveto
(3. The output is hard to understand, and there is not much flexibility in ) show
12 f2 342.6 682.6 moveto
(what) show
12 f0 366.1 682.6 moveto
( is shown \226 the \223all or nothing) show
12 f0 0 669.3 moveto
(syndrome\224, common to many systems.) show
12 f0 0 642.7 moveto
(CLAM has many positive features which suggest how these might be rectified.) show
12 f0 0 616.1 moveto
(1. The level at which the planner operates \226 that of the methods \226 is similar to how humans tackle) show
12 f0 0 602.8 moveto
(problems, and suggests a way of displaying the output.) show
12 f0 0 576.2 moveto
(2. The method preconditions are written in a meta-logic; they were originally thought of as being) show
12 f0 0 562.9 moveto
(declarative in nature, which suggests that they could be used as the basis of communication with the) show
12 f0 0 549.6 moveto
(user, for example in providing explanations.) show
12 f0 0 523 moveto
(However, to make use of these features we needed:) show
12 f0 0 496.4 moveto
(1. To rationally reconstruct the preconditions so that they were truly declarative.) show
12 f0 0 469.8 moveto
(2. To provide a proper interactive architecture for the system.) show
12 f0 0 443.2 moveto
(The resulting system was known as Barnacle.) show
18 f1 0 410.5 moveto
(The Barnacle proof tool) show
14 f1 0 380.3 moveto
(Interactive features) show
12 f0 0 353.3 moveto
(We originally built a system for use on PC Windows systems using LPA Prolog. This system was able) show
12 f0 0 340 moveto
(to give explanations \(see below\), and the user could interact with the system. Our original architecture) show
12 f0 0 326.7 moveto
(did not allow for unforeseen interaction: in some cases the system could second-guess the user, and) show
12 f0 0 313.4 moveto
(invite them to, for example, input a crucial lemma, but otherwise the user had to decide in advance \(or) show
12 f0 0 300.1 moveto
(maybe as a result of a previous attempt\) which controls to set. The user could) show
12 f0 0 273.5 moveto
(demand explanations for some or all methods) show
12 f0 0 246.9 moveto
(request the power of veto over some or all methods.) show
12 f0 0 220.3 moveto
(This inadvertently echoed the architecture of previous, non-interactive versions of CLAM, where) show
12 f0 0 207 moveto
(premeditation was the key to successfully proving some theorems, notably by providing hints, or by) show
12 f0 0 193.7 moveto
(using Prolog pattern matching, to force CLAM to take some step which it would not otherwise carry out) show
12 f0 0 180.4 moveto
(by default. After watching students trying to use this system, we soon decided that the user, not the) show
12 f0 0 167.1 moveto
(program, must be in control, but that the program should attempt to prove the theorem unaided, stopping) show
12 f0 0 153.8 moveto
(only on a signal from the user. This, whilst retaining the proof planning system, necessitated a) show
12 f0 0 140.5 moveto
(fundamental change in architecture. With the new mode of use, presentation of the proof attempt) show
12 f0 0 127.2 moveto
(became all-important \226 without good visual clues, the user does not know when or how to intervene in a) show
12 f0 0 113.9 moveto
(proof. Our previous work reported in Lowe, Bundy, and McLean \(1996\) provided a basis for designing) show
12 f0 0 100.6 moveto
(the graphical interface, demonstrating that users preferred a tree-structured, hierarchical mode of) show
12 f0 0 87.3 moveto
(presentation, and we built a new version, XBarnacle, incorporating these principles. ) show
pagelevel restore
showpage
%%Page: 4 4
%%BeginPageSetup
/pagelevel save def
54 0 translate
%%EndPageSetup
newpath 0 72 moveto 504 0 rlineto 0 648 rlineto -504 0 rlineto closepath clip newpath
14 f1 0 706.4 moveto
(Explanations) show
12 f0 0 679.4 moveto
(An early claim for proof planning with its specification of tactics by means of preconditions was that) show
12 f0 0 666.1 moveto
(this would enhance the explanatory power of systems. For example, the induction method has the) show
12 f0 0 652.8 moveto
(following preconditions \(we assume for the sake of simplicity that induction is over one variable only) show
12 f0 0 639.5 moveto
(but the argument generalizes to two or more variables for simultaneous induction\):) show
12 f0 0 612.9 moveto
(1. There is at least one universally quantified variable.) show
12 f0 0 586.3 moveto
(2. Given an induction schema applicable to such a variable, there is at least one matching rewrite rule) show
12 f0 0 573 moveto
(that can be applied to the induction conclusion.) show
12 f0 0 546.4 moveto
(3. Optionally, various other heuristics may apply. For example, it is good if ) show
12 f2 364.9 546.4 moveto
(all) show
12 f0 377.5 546.4 moveto
( occurrences of the) show
12 f0 0 533.1 moveto
(induction variable can be rewritten using available rewrite rules.) show
12 f0 0 506.5 moveto
(If preconditions are encoded in this declarative way, then we can easily produce explanations of the) show
12 f0 0 493.2 moveto
(form) show
12 f0 0 466.6 moveto
(We can perform induction on x) show
12 f0 0 440 moveto
(because x is a universally quantified variable) show
12 f0 0 413.4 moveto
(and there are available rewrite rules for \205) show
12 f0 0 386.8 moveto
(or) show
12 f0 0 360.2 moveto
(We cannot perform induction on y) show
12 f0 0 333.6 moveto
(because although y is a universally quantified variable) show
12 f0 0 307 moveto
(there are no available rewrite rules for \205) show
12 f0 0 280.4 moveto
(When we came to develop Barnacle, however, we found that because preconditions had not hitherto) show
12 f0 0 267.1 moveto
(been used for explanations, most were ) show
12 f2 186.9 267.1 moveto
(ad hoc) show
12 f0 219.2 267.1 moveto
( and procedural in nature, written in a style of Prolog that) show
12 f0 0 253.8 moveto
(while perhaps efficient was not suitable for use in explanations. As an example, take the preconditions) show
12 f0 0 240.5 moveto
(for generalizing a compound term by a variable as in) show
12 f0 0 213.9 moveto
(s\(s\(x\)\) + \(y + z\) = \(s\(s\(x\)\) + y\) + z \336u=s\(s\(x\)\) u + \(y + z\) = \(u + y\) + z) show
12 f0 0 187.3 moveto
(CLAM\222s existing preconditions were of the form) show
12 f0 0 160.7 moveto
(There is a sub-term X on the left-hand side) show
12 f0 0 134.1 moveto
(X obeys test1) show
12 f0 0 107.5 moveto
(X obeys test2) show
12 f0 0 80.9 moveto
(\205 \205 \205) show
pagelevel restore
showpage
%%Page: 5 5
%%BeginPageSetup
/pagelevel save def
54 0 translate
%%EndPageSetup
newpath 0 72 moveto 504 0 rlineto 0 648 rlineto -504 0 rlineto closepath clip newpath
12 f0 0 702.3 moveto
(X obeys testn) show
12 f0 0 675.7 moveto
(The same sub-term X exists on the right-hand side) show
12 f0 0 649.1 moveto
(In practice, this involves a lot of backtracking as CLAM comes up with sub-terms which fail one or) show
12 f0 0 635.8 moveto
(other of the tests \(various heuristics designed to avoid \223trivial\224 rewritings\); when finally a term exists) show
12 f0 0 622.5 moveto
(which passes all the tests, it may be found not to in the right hand side of the expression. Reordering the) show
12 f0 0 609.2 moveto
(preconditions just causes a different backtracking pattern. Any explanations produced from such) show
12 f0 0 595.9 moveto
(preconditions are wallpaper-like in scope and not very useful.) show
12 f0 0 569.3 moveto
(What is really needed is) show
12 f0 0 542.7 moveto
(There is a sub-term X on both the left and the right hand side such that) show
12 f0 0 516.1 moveto
(X obeys test1) show
12 f0 0 489.5 moveto
(X obeys test2) show
12 f0 0 462.9 moveto
(\205 \205 \205) show
12 f0 0 436.3 moveto
(X obeys testn) show
12 f0 0 409.7 moveto
(This trivial recasting of the preconditions makes all the difference to explanatory power.) show
12 f0 0 383.1 moveto
(Most preconditions in CLAM needed this recasting.) show
12 f0 0 356.5 moveto
(The next question to be answered is who the users are, in other words: who are the explanations) show
12 f0 0 343.2 moveto
(intended for? Are the needs of students and formal methods practitioners different, for example? The) show
12 f0 0 329.9 moveto
(early versions of Barnacle were aimed at the developers of CLAM, in common with many interfaces to) show
12 f0 0 316.6 moveto
(theorem provers which are developed in the first place to serve the needs of existing users of the) show
12 f0 0 303.3 moveto
(systems. Here we might see explanations such as the one for induction above cast as:) show
12 f0 0 276.7 moveto
(We can perform s\(x\) induction on x) show
12 f0 0 250.1 moveto
(because x is a universally quantified variable) show
12 f0 0 223.5 moveto
(and all/some wave occurrences of x are unflawed) show
12 f0 0 196.9 moveto
(This does not make much sense to anyone outside a small community of user-developers, yet it is of) show
12 f0 0 183.6 moveto
(great interest to them, as the unfamiliar terminology comes from the rippling method use of which, as) show
12 f0 0 170.3 moveto
(we shall see, is a vital guarantor of termination, a highly desirable property.) show
12 f0 0 143.7 moveto
(We hope that a one-to-many mapping of preconditions to explanations is possible, where different) show
12 f0 0 130.4 moveto
(explanations are produced from the same declarative preconditions according to the class of user.) show
18 f1 0 97.7 moveto
(Evaluation and Conclusions) show
pagelevel restore
showpage
%%Page: 6 6
%%BeginPageSetup
/pagelevel save def
54 0 translate
%%EndPageSetup
newpath 0 72 moveto 504 0 rlineto 0 648 rlineto -504 0 rlineto closepath clip newpath
14 f1 0 706.9 moveto
(Method of evaluation) show
12 f0 0 679.9 moveto
(Jackson \(1997\) reports on a pilot evaluation of the new architecture carried out by observing users\222) show
12 f0 0 666.6 moveto
(performance on theorem proving tasks using XBarnacle. In this study we observed that users with a) show
12 f0 0 653.3 moveto
(good understanding of the task \226 in this case, proof by induction \226 were able to use XBarnacle very) show
12 f0 0 640 moveto
(effectively, intervening quickly in exactly the right places to steer the system towards a proof. We intend) show
12 f0 0 626.7 moveto
(to carry out more extensive studies; this pilot study was primarily to teach us about the issues involved) show
12 f0 0 613.4 moveto
(in evaluation. There is virtually no evaluation of theorem provers in terms of tasks or users \226 most) show
12 f0 0 600.1 moveto
(evaluation is in performance related terms of the systems themselves such as theorems provable, time) show
12 f0 0 586.8 moveto
(taken, and so on.) show
14 f1 0 557.9 moveto
(User misconceptions) show
12 f0 0 530.9 moveto
(Our early studies show that users may be surprised and disoriented by the complexity and length of) show
12 f0 0 517.6 moveto
(\223simple\224 proofs, forgetting that although the ) show
12 f2 205.6 517.6 moveto
(theorem) show
12 f0 244.9 517.6 moveto
( may be simple, its ) show
12 f2 339.1 517.6 moveto
(proof) show
12 f0 366.8 517.6 moveto
( might not. A user may be) show
12 f0 0 504.3 moveto
(tempted to intervene in a proof when in fact the theorem prover left alone will find a proof eventually.) show
12 f0 0 491 moveto
(This problem may be partially overcome by exposing the novice to example \223easy hard\224 proofs.) show
12 f0 0 477.7 moveto
(Thereafter, success is reliant on the user being able to distinguish between slow progress and) show
12 f0 0 464.4 moveto
(floundering. Developers of methods need to pay more attention to producing more human-like proofs.) show
12 f0 0 451.1 moveto
(The critics mechanism \(Ireland and Bundy, 1994\) is a good technique for this end, as for example a) show
12 f0 0 437.8 moveto
(method critic might try to speculate \(and prove\) a lemma to be used to further the current inductive step,) show
12 f0 0 424.5 moveto
(instead of abandoning the rewriting in favour of a nested induction. Using lemmas in this way is a very) show
12 f0 0 411.2 moveto
(human-like activity. We aim to incorporate critics into Barnacle.) show
14 f1 0 382.3 moveto
(Some unresolved issues) show
12 f0 0 355.3 moveto
(In order to enable effective interaction, users need systems that communicate at their level, and which) show
12 f0 0 342 moveto
(present the task in the same terms as they usually think about it, thus appearing to have the same task) show
12 f0 0 328.7 moveto
(view as they do. Some of the detail of CLAM\222s methods \226 notably the use of rippling \226 represents a) show
12 f0 0 315.4 moveto
(departure in this respect.) show
12 f0 0 288.8 moveto
(Rippling is a powerful rewriting technique used for the step cases of inductive proof, in which both) show
12 f0 0 275.5 moveto
(rewrite rules and the induction conclusion are annotated. The details may be found in Bundy ) show
12 f2 447.2 275.5 moveto
(et al) show
12 f0 468.2 275.5 moveto
(.) show
12 f0 0 262.2 moveto
(\(1993\) and in Basin and Walsh \(1994\) but are quite difficult for non-specialists to understand. When a) show
12 f0 0 248.9 moveto
(rule is compared with a sub-term in the induction conclusion, not only the syntactic structure but also the) show
12 f0 0 235.6 moveto
(annotations must match. Annotations are placed on rules so as to decrease a metric: repeated application) show
12 f0 0 222.3 moveto
(of such rules to the induction conclusion can be guaranteed to terminate, since the metric will decrease.) show
12 f0 0 209 moveto
(One condition on annotated rules is that they must be ) show
12 f2 258.6 209 moveto
(skeleton preserving) show
12 f0 352.2 209 moveto
(: for example the rule) show
12 f0 0 182.4 moveto
(s\(X\) + Y \336 s\(X + Y\)) show
12 f0 0 155.8 moveto
(may be annotated thus:) show
12 f0 0 129.2 moveto
(s\(X\) + Y \336 s\(X + Y\)) show
12 f0 0 102.6 moveto
(Ignoring the parts annotated by heavy type \226 the skeletons \226 the left and right hand sides are identical.) show
12 f0 0 76 moveto
(This rule has other possible measure-decreasing, skeleton-preserving annotations so it does have at least) show
pagelevel restore
showpage
%%Page: 7 7
%%BeginPageSetup
/pagelevel save def
54 0 translate
%%EndPageSetup
newpath 0 72 moveto 504 0 rlineto 0 648 rlineto -504 0 rlineto closepath clip newpath
12 f0 0 709.2 moveto
(one, and is admissible in a step-case proof. However, the rule) show
12 f0 0 682.6 moveto
(X + Y = Y + X) show
12 f0 0 656 moveto
(has no such annotations, since it is not skeleton-preserving. Disallowing such rules in the cause of) show
12 f0 0 642.7 moveto
(termination means that human users maybe surprised by the seemingly unnecessarily complexity of) show
12 f0 0 629.4 moveto
(proofs.) show
12 f0 0 602.8 moveto
(The choices to be made, and the trade-offs, are essentially between supporting the user\222s style of theorem) show
12 f0 0 589.5 moveto
(proving, and the \223rippling\224 style. An allied question is how far we can expect the user to come in learning) show
12 f0 0 576.2 moveto
(some of the theory behind the theorem prover\222s approach, and whether this might be beneficial.) show
12 f0 0 549.6 moveto
(As far as the proof planning method is concerned, there may well be benefits in conveying this to the) show
12 f0 0 536.3 moveto
(user. After all, what we would be teaching is a ) show
12 f2 225.9 536.3 moveto
(strategy) show
12 f0 264.5 536.3 moveto
( for proving theorems by induction \226 something) show
12 f0 0 523 moveto
(which is missing, or could do with reinforcing, in the mathematical education of computing students.) show
12 f0 0 496.4 moveto
(As to the rippling story, this is more difficult. In the author\222s own experience, it is comparatively easy to) show
12 f0 0 483.1 moveto
(put over the idea of a measure, since this accords with students\222 knowledge of metrics in general, and the) show
12 f0 0 469.8 moveto
(concept of such a measure guaranteeing termination as a good thing. The details need not be taught, as) show
12 f0 0 456.5 moveto
(long as students are happy to accept that certain rules \226 notably commutativity \226 will not be used by the) show
12 f0 0 443.2 moveto
(theorem prover in the step cases of proofs.) show
12 f0 0 416.6 moveto
(A related question is that of notation. Developers of CLAM, who understand the rippling annotation,) show
12 f0 0 403.3 moveto
(expect to see some graphical representation of it in any displays of sub-goals or proof fragments. For) show
12 f0 0 390 moveto
(students learning about rippling, this is also useful. But for practitioners who do not wish to analyse the) show
12 f0 0 376.7 moveto
(proof at that level of detail, such displays are distracting and perhaps confusing. In XBarnacle, the) show
12 f0 0 363.4 moveto
(display of different kinds of annotation can be switched on or off, and the system customized so that) show
12 f0 0 350.1 moveto
(XBarnacle starts up in the mode most desirable for the given user.) show
12 f0 0 323.5 moveto
(Two choices, and the associated benefits and problems are:) show
12 f0 0 296.9 moveto
(Strict application of the rippling method, all rules applied must be skeleton-preserving and) show
12 f0 0 283.6 moveto
(measure-decreasing.) show
12 f0 0 257 moveto
(The benefits of restricting rewriting to this powerful control technique have been outlined above. The) show
12 f0 0 243.7 moveto
(style of interaction implied is that the user lets the prover go, with a high degree of trust, even when it) show
12 f0 0 230.4 moveto
(does not always apply the \223obvious\224 rule, stopping it only when it is \223obviously\224 going wrong. Cases of the) show
12 f0 0 217.1 moveto
(latter might be applying an over-generalization, when the user spots that the new conjecture is not a) show
12 f0 0 203.8 moveto
(theorem \(this happens sometimes\), or when there is an obvious divergence of the sub-goals, as where an) show
12 f0 0 190.5 moveto
(s\(x\) expression in the previous induction is replaced by an s\(s\(x\)\) term in the nest induction below \(users) show
12 f0 0 177.2 moveto
(will generally halt CLAM once they spot a \(s\(s\(s\(s\(\205\)\)\)\) pattern\).) show
12 f0 0 150.6 moveto
(The user intervenes early and often \226 when they spot a rewriting that they would make, and ignoring) show
12 f0 0 137.3 moveto
(questions of measure and skeleton preservation.) show
12 f0 0 110.7 moveto
(This approach is fraught with problems, not nonetheless feasible. First, some preconditions must be) show
12 f0 0 97.4 moveto
(made into soft constraints, overridable by the user. Secondly, some measures must be taken to save users) show
12 f0 0 84.1 moveto
(from themselves. The chief problem is that of non-termination and looping, which of course rippling is) show
pagelevel restore
showpage
%%Page: 8 8
%%BeginPageSetup
/pagelevel save def
54 0 translate
%%EndPageSetup
newpath 0 72 moveto 504 0 rlineto 0 648 rlineto -504 0 rlineto closepath clip newpath
12 f0 0 709.2 moveto
(designed to avoid. One way would be to allow commutativity laws etc. as lemmas, and to restrict their) show
12 f0 0 695.9 moveto
(use. For example, with a good library browser they could be stored as lemmas and invoked by the user) show
12 f0 0 682.6 moveto
(only to finish off a branch of a proof.) show
14 f1 0 653.7 moveto
(Summary) show
12 f0 0 626.7 moveto
(Starting from a theorem prover with a command line interface, CLAM, we have built two versions of a) show
12 f0 0 613.4 moveto
(semi-automated theorem prover with a graphical user interface. The first put too much onus on the user) show
12 f0 0 600.1 moveto
(to predict what intervention would be required, although it made some useful contributions to the study) show
12 f0 0 586.8 moveto
(of how users\222 prefer to see proofs displayed, and how they wish to interact. The second, whilst ) show
12 f2 453.2 586.8 moveto
(allowing) show
12 f0 495.2 586.8 moveto
(,) show
12 f0 0 573.5 moveto
(does not ) show
12 f2 45 573.5 moveto
(force) show
12 f0 69.6 573.5 moveto
( the user to interact, using an effective graphical, hierarchical, tree display to provide the) show
12 f0 0 560.2 moveto
(user with visual clues as to when and how to intervene in the proof attempt. Having built such a tool, we) show
12 f0 0 546.9 moveto
(are now in a position to investigate much more systematically than hitherto:) show
12 f0 0 520.3 moveto
(what the user ) show
12 f2 66.9 520.3 moveto
(needs) show
12 f0 94.2 520.3 moveto
( to know ) show
12 f0 0 493.7 moveto
(what the user ) show
12 f2 66.9 493.7 moveto
(wants) show
12 f0 94.9 493.7 moveto
( to know) show
12 f2 0 467.1 moveto
(how) show
12 f0 20 467.1 moveto
(,) show
12 f2 23 467.1 moveto
( when) show
12 f0 51.3 467.1 moveto
(, and ) show
12 f2 77.6 467.1 moveto
(at what level) show
12 f0 138.9 467.1 moveto
( to represent information.) show
12 f0 0 440.5 moveto
(We hope in this way that we can provide a tool which is not only useful for teaching students formal) show
12 f0 0 427.2 moveto
(methods, but that they will also find it useful enough to take away with them, thus furthering the cause) show
12 f0 0 413.9 moveto
(of proof in software development and verification.) show
14 f1 0 385 moveto
(References) show
12 f0 0 358 moveto
(D. A. Basin and T. Walsh, \(1994\). Annotated rewriting in inductive theorem proving. Technical report,) show
12 f0 0 344.7 moveto
(Max Planck Institute, Saarbr\374ken.) show
12 f0 0 318.1 moveto
(R.S. Boyer and J.S. Moore. ) show
12 f2 135.2 318.1 moveto
(A Computational Logic.) show
12 f0 250.8 318.1 moveto
( Academic Press, 1979.) show
12 f0 0 291.5 moveto
(A. Bundy. The use of explicit proof plans to guide inductive proofs. In R. Lusk and R. Overbeek \(eds.\),) show
12 f2 0.2 278.2 moveto
(Ninth Conference on Automated Deduction) show
12 f0 208.1 278.2 moveto
(, pages 111 \226 120. Springer Verlag, 1988.) show
12 f0 0 251.6 moveto
(A. Bundy, F. van Harmelen, C Horn, and A. Smaill \(1990\). The Oyster-Clam system. In Stickel, M E) show
12 f0 0 238.3 moveto
(\(ed.\), 10th Conference on Automated Deduction, pages 647-648. Springer-Verlag, Berlin. Lecture Notes) show
12 f0 0 225 moveto
(in Artificial Intelligence No. 449.) show
12 f0 0 198.4 moveto
(A. Bundy, A. Stevens, F. van Harmelen, A. Ireland, A. and Smaill, \(1993\). Rippling: A heuristic for) show
12 f0 0 185.1 moveto
(guiding inductive proofs. Artificial Intelligence, 62, pages 185-253.) show
12 f0 0 158.5 moveto
(R.L. Constable, S.F. Allen, H.M. Bramley, ) show
12 f2 209 158.5 moveto
(et al) show
12 f0 230 158.5 moveto
(. Implementing Mathematics with the NuPRL Proof) show
12 f0 0 145.2 moveto
(Development System. Prentice Hall, 1986.) show
12 f0 0 118.6 moveto
(A. Ireland, and A. Bundy \(1994\). Productive use of failure in inductive proof. Technical Report,) show
12 f0 0 105.3 moveto
(Research Paper No. 716, Department of Artificial Intelligence, University of Edinburgh.) show
12 f0 0 78.7 moveto
(M. Jackson. A Pilot Study of an Automated Theorem Prover Interface. To be submitted to the ) show
12 f2 453.6 78.7 moveto
(Third) show
pagelevel restore
showpage
%%Page: 9 9
%%BeginPageSetup
/pagelevel save def
54 0 translate
%%EndPageSetup
newpath 0 72 moveto 504 0 rlineto 0 648 rlineto -504 0 rlineto closepath clip newpath
12 f2 0 709.2 moveto
(Workshop on User Interfaces for Theorem Proving) show
12 f0 245.3 709.2 moveto
(, September, 1977.) show
12 f0 0 682.6 moveto
(H. Lowe, A. Bundy, and D. McLean \(1996\). The Use of Proof Planning for Co-operative Theorem) show
12 f0 0 669.3 moveto
(Proving, University of Edinburgh DAI Research Paper 745.) show
pagelevel restore
showpage
%%EOF