Home

a proof editor for propositional and predicate calculus

Contents

1. lt id constant gt lt pred transf rule gt lt pred default val gt 36 zero lt id operator gt lt id constant gt connective lt id operator gt a Gy a9 transitive lt id operator gt lt id operator gt lt id operator gt proveFF lt id operator gt proveTF lt id operator gt prove lt id operator gt related lt id operator gt lt id operator gt conjunctional lt id operator gt equivalent lt id operator gt lt id operator gt a9 lt id operator gt quantifier lt id operator gt n lt id operator gt substitute lt id operator gt 6 0 lt id operator gt le ibniz e lt id operator gt defTrue lt id constant gt defFalse lt id constant gt defAnd lt id operator gt defOr lt id operator gt 37 lt rule statement gt fail lt string gt scopeBegin lt scope statement gt scopeEnd it lt rule condition gt then lt rule statement gt elseif lt rule condition gt then lt rule
2. 63 3 3 5 Defining operators E A 4 8 66 3 3 6 Defining functions anclada kB aes 67 3 3 7 Defining axioms and theorems 68 3 3 8 Defining rules a Poe Bey a Pe oe eed 68 3 3 9 Defining operator precedence 68 3 3 10 Defining operator properties 72 3 4 Working with proofs A IAEA 74 34AT Staring aA progi ici a le 003 a ee ew He ae ae a 74 tacts 20d a a pr glk ee A a 15 ada 27 s 76 Completing proofs 4 a RA EE 3 4 3 Applying operator quantifier properties 76 3 4 4 Parentheses and substitutions 78 3 4 5 Applying user defined rules 00 78 3 4 6 JD Error E e Saad A 78 3 6 Unimplemented features and known bugs aaa aa 85 Bibliography 88 vi List of Figures 2 1 Textual substitution 2 44 66 486 ds bk 9 11 2 2 Subexpressions and structure cc 42 2 9 PhE M n Gora ak nes A aie d olari Mok ake dew at A 50 3 1 Creating a new module 224 444 44444 Heck e Rete a aa ca 58 See SETE AVON ie pa a oi AAA ee a ek wR 61 33 Defining q u s sae Sak ee ae ek el aw ole ole 64 3 4 Defining constants xs e a ed ak he ee Ae ele le he ml Bl 65 ou Denning ia s de e e COR ee ese 6 3 6 Defining cional A Bad
3. ee a a 67 3 7 Defining axioms and theorems 004 69 3 8 Defining rules ea er oe e Si ee Ok de ok Za d a 70 3 9 Defining operator precedence o 71 3 10 Defining operator properties cc 73 3 11 Operator equivalent form 0 00 77 vil Chapter 1 Introduction This thesis presents an equational proof editor following the style used in the text A Logical Approach to Discrete Math GS93 Several tools have been developed recently that can serve as formal proof editors Among them one should mention the following e the Prozac editor for proof and program transformation vdS94a vdS94b developed in California Institute of Technology It tool is closest to a usable editor for proofs in the style of GS93 It has been implemented in Modula 3 which is the main reason why it cannot be used until now there is no reliable Modula 3 compiler for the Apple Macintosh Other reasons are its inefficient user interface the slightly different format it uses for proofs and the fact that it cannot be easily extended e the NUPRL proof development system C 86 developed in Cornell University It focuses on automatic proof development using natural deduction However the proof format that it uses and the complexity of this system make it inap propriate for lower level math courses the MathPad mathematical report writer BVW94 developed
4. IS_PROVE_TF op operator op has been declared proveTF IS_PROVE op operator op has been declared prove IS_RELATED op1 op2 operators op1 and op2 have been declared related 17 e IS_CONJUNCTIONAL op operator op has been declared conjunctional e IS_EQUIVALENT op1 op2 operators op1 and op2 have been declared equiv alent e ISDEF_TRUE a default true value has been defined e ISDEF_FALSE a default false value has been defined e ISDEF_AND a default conjunction operator has been defined e ISDEF_OR a default disjunction operator has been defined 2 2 5 Rules for operator properties Rules for operator properties are used internally by the editor They are defined with the statement rule Some of these properties can be applied to the current expression on the fly that is without any intermediate steps and hints Some others affect the behavior of operators and the way in which expressions are matched Operator properties that are used in transformations are e symmetric op specifies that operator op is symmetric This means that a subexpression of the form x op y can be replaced on the fly by y op x The following conditions must be satisfied TYPEOP1 op TYPEOP2 0p not HAS_DUAL op However the user can specify that the intermediate steps should not be omitted In that case a descriptive hint will be given and the equality operator will be used 18 e associative op specifies that op
5. LZERO lt id operator gt RZERO lt id operator gt ZERO lt id operator gt DEF_TRUE DEF_FALSE 41 CURR_EXPR CURR_FACT CURR_SUBEXP A small programming language allows the users to define their own rules The semantics of this language is described in 2 4 4 We tried to make this language as simple as possible so many features that may be needed have been left out User defined rules can be used in order to relax the style of proofs Some features of our editor such as scopes and auxiliary proofs cannot be used but from user defined rules 2 4 More detailed specifications In this section we give some more formal definitions of terms used in the previous sections and describe the user interface in more detail 2 4 1 Subexpressions We now define the notion of a subexpression Let S E be the set of subexpressions of E A formal definition of S E is given in Fig 2 2 2 4 2 Structure of expressions We now define the notion of an expression s structure We have to define two auxiliary notions outermost operator and primary subexpression Let O E be the tuple TA tuple is an ordered set that can contain multiple occurrences of the same element A tuple containing the elements za 2 Zn in this order is written as 21 29 The empty tuple is written as If z is an element and t is a tuple z lt
6. TYPEOP2 0p TYPERES op boolean e transitive op1 op2 op3 specifies that the sequence of steps expl opl exp2 op2 exp3 is equivalent to a step expl op3 exp3 21 omitting the hints The following conditions must be satisfied IS_CONNECTIVE op1 IS_CONNECTIVE op2 IS_CONNECTIVE op3 proveFF op specifies that if we have a sequence of steps equivalent to expl op exp2 and exp is a fact then by ending the proof there exp2 becomes a fact The following conditions must be satisfied IS_CONNECTIVE op TYPEOP1 op TYPEOP2 op boolean proveTF op specifies that if we have a sequence of steps equivalent to expl op exp2 and exp2 is a fact then by ending the proof there exp1 becomes a fact The following conditions must be satisfied IS_CONNECTIVE op TYPEOP1 op TYPEOP2 op boolean 22 e prove op is the same as giving both proveFF and proveTF The following conditions must be satisfied IS_CONNECTIVE op TYPEOP1 op TYPEOP2 op boolean e related op1 op2 specifies that if a sequence of steps equivalent to expl opl exp2 is a valid proof for the expression exp1 op2 exp2 Every operator is con sidered to be related to itself therefore no rules of the form related op op need to be given The following conditions must be satisfied IS_CONNECTIVE opi TYPEOP1 op1 TYPEOP2 op1 TYPEOP1 op2 TYPEOP2 op2 e conjunctional op s
7. and the expression that needs to be proved is of the form exp1 op2 exp2 then it is considered proved if the following condition is also satisfied IS_RELATED op1 op2 2 2 8 Quantifier properties The following quantifier properties have been predefined They can be applied on the fly in the same way as operator properties defined by rules The user can specify whether the intermediate steps will be omitted If intermediate steps are not omitted a descriptive hint will be given and the equality operator will be used e Missing range 28 op x E op x DEF_TRUE E Empty range op x DEF_FALSE E IDENTITY op One point rule Provided not occurs a E op x x E F Distributivity op R P op op x R Q op R P op Q Range split op R DEF_OR S P op op x R DEF_AND S P op x R P op op x S P e Range split Provided R DEF_AND S DEF_FALSE or IS_IDEMPOTENT op op x R DEF_OR S P op x R P op op x 8 P 29 Interchange of dummies Provided not occurs y R and not occurs x Q op x R op y Q P op y Q op x R P Nesting Provided not occurs y R op x y R DEF_AND Q P op x R op y Q P e Dummy renaming Provided not occurs y R P op R P op y R x y P x y
8. 3 6 For a general presentation of the proof editor and for understanding its basics the reader is directed to 2 1 and 82 2 The present document is a user s manual for the proof editor and assumes that the reader understands the principles of proof transformations and the basic terminology of this tool as described in its specifica tions document The user should also be familiar with the standard Macintosh user interface and have some experience using typical Macintosh applications 56 57 3 2 Working with files A module is the fundamental document with which the proof editor works Each module is associated with a file from which it is loaded and to which it is saved Modules can include other modules thus creating a module hierarchy The proof editor recognizes one module as the current one the one being edited All other modules that are contained in the current one can be used but not altered in any way At most one file can be edited at a time the file containing the current module Each module can contain definitions of types constants operators functions axioms theorems properties and rules All this information is represented in the proof editor s internal language which is described in 2 3 The proof editor works with two types of files proof editor files and text files The former can only be edited by the proof editor The latter can also be edited by any text editor however the user needs to understand
9. applied or substituted The corresponding commands are Transform Apply fact and Transform Substitute fact The user has to select the fact to be used from the facts window and optionally type a substitution of its free variables in the input window When using Transform Apply fact the current subexpression is matched with part of the current fact after all user specified substitutions have taken place The fact s free variables are matched with terms in the current subexpression If there are still free variables after the matching they are fixed A transformation step is created according to what is described in 2 2 6 When using Transform Substitute fact if the current subexpression is the default true value it is replaced by the current fact after all user specified substitu tions have taken place and remaining free variables are fixed Otherwise the current subexpression is matched with the current fact If it is an instance of this a trans formation step is created with the equality operator and the current expression is substituted by the default true value It should be noted here that although the matching of the current subexpression with the current fact is always correct that is the transformation steps are always valid it is not necessarily what the user expects Free variables can usually be matched in various ways resulting in completely different transformation steps If more than one way is possible the proof
10. otherwise it is false occurs v e The predicate that has been defined in 2 1 3 where v is a variable list and e is an expression list Arrays can also be used as expression lists e beginScope and endScope Defines a new scope If the current proof technique is not PROVE_TF an error occurs In this scope there can be the following scope statements assume Make an assumption Assumptions can be made only in the beginning of a new scope If this is not the case an error occurs If an array is given the statement is repeated for all elements of the array prove Start an auxiliary proof If the current proof technique is not PROVE_TF an error occurs The current proof before the rule was applied will depend on the new one If an array is given the statement is repeated for all elements of the array e fail Print a diagnostic message explaining why this rule cannot be applied and stop 50 Figure 2 3 The main menu 2 45 The interface capabilities of the programming environment We now describe these functions one by one File Edit Define Proof Transform Property Options New Symmetry Proof Open Conjunctionality Directories To fact Include Equivalent form Load From fact mee Close Missing range Save By transformation Save Empty range Delete step Save as O
11. a dual its two operands are reversed and the operator is replaced by its dual e Conjunctionality If the current subexpression is a chain of conjunctional opera 17 File Edit Define Proof Transform Property Options 117PM 2 A ii propcalc rlx Facts Prove p gt true true Pil q gt p amp amp q p TU Reflexivity of gt 3 71 p gt p true TU Right zero of gt 3 72 Proof by transforming toa fact p gt true true p gt true true TU Left identity of gt 3 7 true gt p TU Theorem 3 74 p gt false p Choose TU Theorem 3 75 false gt p true TU HWeakening strengthening p gt p lla TU Weakening strengthening p amp amp q gt p Weakening strengthening RuleWindow Module propcalc rix Assuming the antecedent Prove separately Case analysis Mutual implication Contradiction Contraposi tive Nodule propcalc tha Hodule propcalc def InputWindow Figure 3 11 Operator equivalent form tors it is transformed into a conjunction of these operators If it is a conjunction of conjunctional operators it is transformed into a chain e Equivalent form The dialog box of Fig 3 11 appears and the user must choose one of the equivalent forms of the current subexpression s outermost operator The quantifier properties that can be applied are described in 2 2 8 These have not been impleme
12. bug in the proof editor e Fatal errors Errors that cause the proof editor application to stop e Common errors Errors from which the proof editor can recover e Warning messages Usually not important possible errors If an internal error happens please send the author a report containing the error message and a description of how it happened as detailed as possible The same if the system crashes or if the proof editor does not behave as it should make sure to look at 3 6 though Here is a list of various common error messages in alphabetical order Assertion failed Internal error An assertion failed Please report this Cannot apply conjunctionality to this expression Operator conjunctionality cannot be applied to the current subexpression Cannot apply symmetry duality to this expression Operator symmetry or duality cannot be applied to the current subexpression Cannot change existing proof mode A proof mode has already been selected for the current proof and cannot be changed To change it you have to delete all steps of the proof 80 Cannot open a dependent scope in this proof A dependent scope can be opened only in a proof to a fact Cannot open file lt filename gt File lt filename gt cannot be opened for reading or writing If for reading it is possible that the file does not exist or cannot be found If for writing it is possible that the file already exists and cannot be overwritten Cannot read
13. constant gt lt id variable gt lt id function gt lt expr list gt lt expression gt C lt id operator gt lt dummy decl gt cc 99 lt ezpression gt lt expression gt lt seq subst gt lt var list gt lt expr list gt lt var list gt lt id variable gt lt id variable gt lt expr list gt lt expression gt lt expression gt cc 99 3 lt dummy decl gt lt part dummy decl gt lt part dummy decl gt lt part dummy decl gt lt var list gt lt id type gt LIST 2 3 7 Definition of axioms Axioms are defined by statements of the following form lt statement gt axiom lt type decl gt lt fact name gt lt fact condition gt states lt expression gt y where lt type decl gt lt part type decl gt lt part type decl gt 33 lt part type decl gt lt var list gt lt type gt lt fact name gt title lt string gt number lt string gt lt fact condition gt condition not occurs lt var list gt lt expr list gt 2 3 8 Definition of theorems Theorems are defined by statements of the form lt statement gt theorem lt type decl gt 1 lt fact name gt lt fact condition gt lt p
14. e The facts window This window contains a list of all facts axioms and the orems defined in the current module and all modules that this one includes The facts are sorted by module and are given in the order in which they have been defined By clicking on a module s name in the facts window the user can hide its facts They can be shown again with a second click Each fact is displayed in two lines The first line contains its title and number preceded by one to three letters characterizing the fact The first letter is one of the following A the fact is an axiom T the fact is a theorem a the fact is an assumption In case the fact is a theorem the second letter is one of the following P the theorem has been proved U the theorem has not been proved Finally the third letter is an optional c meaning that the fact can be applied under some conditions e The rules window This window contains a list of all user defined rules defined in the current module and all modules that this includes The rules are sorted 63 by module and are given in the order in which they have been defined By clicking on a module s name in the rules window the user can hide its rules They can be shown again with a second click For each rule only its name is displayed e The input window This window is used as a means of communication between the proof editor and the user 3 3 2 Including existing modules By using command F
15. editor will choose one of them If the user wanted something different they have to delete the step and try again by specifying 76 the substitutions manually To delete the last transformation step in the current proof the user can select command Proof Delete step 3 4 3 Completing proofs A proof can be completed by selecting command Proof QED Completing a proof is not always valid the proof s correctness is checked when the user selects this command as described in 2 2 7 Completing a proof does not automatically close it It can be undone by selecting Proof Delete step However after closing a complete proof the user cannot ever change it again unless they change the module s internal representation 3 4 4 Applying operator quantifier properties Operator and quantifier properties can be applied to the current subexpression by using the commands of menu Property When applying an operator property the current subexpression s outermost operators see 2 4 2 must be infix operators When applying a quantifier property the current subexpression must be an instance of one of the two sides of a quantifier predefined property see 2 2 8 For all these properties a transformation step with the equality operator is created The operator properties that can be applied are the following e Symmetry If the outermost operator of the current subexpression is symmetric its two operands are reversed Otherwise if it has
16. gt assume lt expression gt Y lt fact name gt 2 3 9 Definition of rules Rules are divided in four categories e Predefined rules for transforming the current subexpression on the fly e Predefined rules for transforming the current subexpression by using facts e Predefined rules for defining the default true and false values and also the default conjunction and disjunction operators 35 e User defined rules Rules can be defined with statements of the form lt statement gt rule lt pred oper property gt rule lt pred transf rule gt rule lt pred default val gt rule title lt string gt lt rule statement gt lt pred oper property gt symmetric lt id operator gt associative lt id operator gt idempotent lt id operator gt dual lt id operator gt lt id operator gt cn lt id operator gt mutualAssoc lt id operator gt leftIdent lt id operator gt lt id constant gt rightIdent lt id operator gt lt id constant gt a9 lt id operator gt pc identity lt id constant gt leftZero lt id operator gt lt id constant gt s G 6 9 rightZero lt id operator gt
17. leibniz op1 op2 specifies that if there is a fact of the form op1 y and the current expression contains x as a subexpression then a step can be made by replacing x by y in the current expression using operator op2 and the fact as a hint This property is an extension of the previous property substitute If IS_SYMMETRIC op1 then the step can be made even if the fact is of the form y opi x 26 If IS_DUAL op1 op1 and IS_DUAL op2 op2 and the fact is of the form y opi x then the step can be made using operator op2 and the fact as a hint The following conditions must be satisfied TYPEOP1 op1 TYPEOP2 op1 IS_CONNECTIVE op2 2 2 7 Proof techniques Three proof techniques are predefined e PROVE_FF Starting with a fact transform it to the expression that needs to be proved If the sequence of steps is equivalent to expl op exp2 and expl is a fact then exp2 becomes a fact The following condition has to be satisfied IS_PROVE_FF op e PROVE_TF Starting with the expression that needs to be proved transform it to a fact If the sequence of steps is equivalent to expl 27 op exp2 and exp2 is a fact then exp1 becomes a fact The following condition has to be satisfied IS_PROVE_TF op e PROVE_TR Starting with an expression transform it to another expression If the sequence of steps is equivalent to expl opl exp2
18. proofs In order to edit a theorem s proof the user selects the theorem from the facts win dow and clicks command Edit Open proof The proof window then displays the theorem s proof If the proof is not completed the user can edit it by using the com mands in menus Proof Transform and Property Otherwise the proof cannot be changed To close the proof that is currently being edited the user clicks command Edit Close proof When editing a proof the last expression appearing in the proof window is consid ered to be the current expression This expression is used in the next transformation step The user can drag the mouse to select a part of this expression the current subexpression If a subexpression is selected only this subexpression will be used in the next transformation step 3 4 1 Starting a proof There are three ways to start a proof each corresponding to a predefined proof technique see 2 2 7 The three relevant commands are e Proof To fact Start a proof to a fact e Proof From fact Start a proof from a fact The currently selected fact in the facts window is used as the fact to start from The user can type a substitution of this fact s free variables in the input window e Proof By transformation Start a proof by transformation The user must type the starting expression in the input window 15 3 4 2 Using facts One way to add steps to a proof is by using proved facts Such facts can be either
19. rule is currently selected in the rules window 83 Select a theorem first You have selected Edit Open proof without a theorem being selected in the facts window Syntax error in rule condition Check the user defined rule text for a syntax error see 2 3 The current fact cannot be applied The current fact cannot be applied to the current subexpression because no matching was found or the outermost operator is not a connective The current fact cannot be used conditions not satisfied The current fact s conditions are not satisfied so the fact cannot be used The current fact cannot be used not proved The current fact is an unproved theorem so it cannot be used The current fact cannot be used out of range The current fact is out of the range of theorems that can be used The current subexpression is invalid What is currently selected in the proof window is not a valid subexpression of the current expression The current subexpression is not a fact You have selected Transform Substitute fact but the current subexpression is neither the default true value nor an instance of the current fact There is no equivalent form for this expression There are no equivalent forms for the current subexpression s outermost operator 84 This statement should never be executed Internal error A statement was executed that was not supposed to Please report this Too few arguments in call to function A funct
20. t is the tuple that results from prepending z to t 42 c 0E U S E Eo U S E Ey 01 E2 02 9 1 En Uicicj lt n Ei 1 U Ua SIBI HE Es En fKE1 E2 En U SIE U S E3 U U S E E E U SIE 07 R E 169 R E U SIR U SIE E z FE 5 8 SE UU S E e e variable constant prefiz o postfix o Fy 01 E2 02 On 1 En infiz o1 infiz gt g infiz on 1 PE E2 Em function f E parenthesis oy R E quantifier o y E z e substitution 2 Memorandum v a variable 6 a constant 9 1 a function 1 Y lists of dummy variables E E R expressions e alist of expressions Figure 2 2 Subexpressions and structure 43 of all outermost operators of expression E Let P E be the tuple of all primary subexpressions of E A definition of these two notions is given in Fig 2 2 2 4 3 Expression matching Expression matching is a very important operation of our proof editor Tt is used internally in the transformation procedure and also in user defined rules However we do not give a completely formal definition for expression matching since this would be rather tedious Variables are generally divided in two categories e Free variables variables that are declared before an expression surrounded by brackets e g p q boolean p amp amp p gt q gt q Such variables
21. the table bind stronger than operators toward its bottom The lower table contains operators that have not yet been placed in the precedence table To place such an operator in the precedence table select the operator select a row in the precedence table and click at one of the three placement buttons e In same row place the operator in the row that has been selected e New row above create a new row just above the one that has been selected and place the operator there e New row below create a new row just below the one that has been selected and place the operator there 3 3 10 Defining operator properties By using command Define Property the user can define operator properties in ternal language predefined rules see 2 2 5 The dialog box in Fig 3 10 appears To define an operator property the user must select the property s name and specify its arguments Then by clicking on button Add the property is placed in the list of properties to be defined it can be removed by clicking on button Remove 13 S File Edit Define Proof Transform Property Options 1 15 PM 2 a a Untitled Facts No proof is being edited Module test Operator properties Property Arguments Mutually associative Proves Proves from fact Proves to fact Quantifier Added properties associative identity 0 Figure 3 10 Defining operator properties 74 3 4 Working with
22. 2 leftIdent op c specifies that c is the left identity of operator op This means that a subexpression of the form c op x can be replaced on the fly by x and vice versa The following conditions must be satisfied IS_CONSTANT c TYPEEXP c TYPEOP1 op TYPEOP2 op TYPERES op rightIdent op c specifies that c is the right identity of operator op This means that a subexpression of the form x op c can be replaced on the fly by ap x and vice versa The same conditions as for leftIdent must be satisfied identity op c is the same as giving both leftIdent op c rightIdent op c leftZero op c specifies that c is the left zero of operator op This means that a subexpression of the form c op x can be replaced on the fly by c and vice versa The same conditions as for leftIdent must be satisfied rightZero op c specifies that c is the right zero of operator op This means that a subexpression of the form x op c can be replaced on the fly by c and vice versa The same conditions as for leftIdent must be satisfied 20 e zero op c is the same as giving both leftZero op c rightZero op c The following properties affect the behavior of operators e connective op specifies that operator op is a connective operator This means that it can be used to connect expressions along the steps of a proof The following conditions must be satisfied TYPEOP1 op
23. 2 A Untitled Facts No proof is being edited Module test Number a Co ea Title Reflexivity of equality Free variables Variable Type Find free variables free variables SY InputWindow Figure 3 7 Defining axioms and theorems 70 6 File Edit Define Proof Transform Property Options 1 11 PM 2 A i Untitled Facts No proof is beipa_edited Module Title Assuming the antecedent Rule code if CURR_EHPR matches p q boolean p gt q then beginScope assume p prove q h endScope else fail The current expression is not an implication AM PUWindow Figure 3 8 Defining rules 71 6 File Edit Define Proof Transform Property Options 114PM 2 A i Untitled Facts O No proof is bej Hadula o p gt gt gt Operator precedence Precedence table Top highest Bottom lowest Window st Unplaced operators is e antecedent In same row New row above New row below Figure 3 9 Defining operator precedence 72 an operator has been placed in this table its precedence with respect to all other operators has already been defined This table consists of several rows In each row one or more operators can be placed If two operators are in the same row they have the same precedence Operators in rows toward the top of
24. 3 9 e TYPEOP op the type of the operand of prefix or postfix operator op a type name e TYPEOP1 op and TYPEOP2 op the types of the two operands left and right respectively of infix operator op a type name e TYPERES op the result type of operator op a type name e TYPEEXP exp the type of expression exp a type name e LIDENT op the left identity of infix operator op if it exists a constant e RIDENT op the right identity of infix operator op if it exists a constant e IDENTITY op the identity of infix operator op if it exists a constant e LZERO op the left zero of infix operator op if it exists a constant e RZERO op the right zero of infix operator op if it exists a constant e ZERO op the zero of infix operator op if it exists a constant e DUAL op the operator that has been declared dual to operator op by a rule If operator op is symmetric then it returns op e DEF_TRUE the boolean constant that has been declared to be the default true value 15 e DEF_FALSE the boolean constant that has been declared to be the default false value e DEF_AND the operator that has been declared to be the default conjunction operator e DEF_OR the operator that has been declared to be the default disjunction op erator e QUANTOPER op the name that will be used when operator op is used in a quantification If no quantifier rule has been given it returns op e CURR_EXPR t
25. A PROOF EDITOR FOR PROPOSITIONAL AND PREDICATE CALCULUS A Thesis Presented to the Faculty of the Graduate School of Cornell University in Partial Fulfillment of the Requirements for the Degree of Master of Science by Nikolaos Papaspyrou January 1995 Nikolaos Papaspyrou 1995 ALL RIGHTS RESERVED ABSTRACT In many universities lower level math courses on propositional and predicate calculus usually avoid using formalism in definitions and proofs at least in the beginning When formalization is later introduced the students are left with the impression that formalism is not essential or worth the effort On the contrary the Department of Computer Science of Cornell University adopts formalism in these courses from the very beginning Students learn not to fear formalism and develop their reasoning abilities by constructing rigorous proofs However the construction of formal proofs is not always easy When the magni tude of the problem increases it is easy to forget or neglect something and it is equally easy to loosen the formalism either by carelessness or on purpose A computer based proof editor that checks each step of a proof can help solve these problems The subject of this thesis is the design and implementation of a computer program that facilitates the construction of formal proofs The proof editor that has been developed can be used to familiarize students with formalism and help them construct rigorous and soun
26. Command File Save as first asks the user for the name of the file in which the current module is to be saved A standard dialog box for saving files appears Finally by selecting command File Close the user can close the current module If this has not been saved a warning message will appear and the user will be prompted to save it 3 2 3 Working with text files The proof editor lets the user work with text files These files can be edited with any text editor and later be imported again so that they can be used with the proof editor Although this is not necessary and is against the philosophy of the proof editor some people prefer working with text files Furthermore the proof editor does not allow all kinds of changes in a module e g facts cannot be deleted once they have been defined and sometimes the only way to change a module is by 60 editing its internal language representation The user must be very careful when editing these files as text and comply with the internal language s syntax described in 82 3 Command File Import works the same as File Open only it opens text files A standard dialog box appears when this command is selected Command File Export is equivalent to command File Save as for text files 3 2 4 Other File commands The remaining two commands in the File menu are e File Print LaTeX Print the current module as a IATpX file It has not been implemented in this version of the proof edit
27. actic or semantic errors 24 e defTrue c defines the default true value to be c The following conditions must be satisfied not ISDEF_TRUE IS_CONSTANT c TYPEFXP c boolean e defFalse c defines the default false value to be c The following conditions must be satisfied not ISDEF_FALSE IS_CONSTANT c TYPEFXP c boolean e defAnd op defines the default conjunction operator to be op The following conditions must be satisfied not ISDEF_AND TYPEOP1 op TYPEOP2 op TYPERES op boolean IS_ASSOCIATIVE op e defOr c defines the default disjunction operator to be op The following conditions must be satisfied not ISDEF_OR TYPEOP1 op TYPEOP2 op TYPERES op boolean IS_ASSOCIATIVE op 25 2 2 6 Rules for transformation steps The following rules are used internally by the editor in order to create transformation steps e substitute op1 op2 specifies that if there is a fact of the form opi y and the current expression is x then a step can be made to y using operator op2 and the fact as a hint If IS_SYMMETRIC op1 then the step can be made even if the fact is of the form y 001 x If IS_DUAL op1 op1 and IS_DUAL op2 op2 and the fact is of the form y op1 x then the step can be made using operator op2 and the fact as a hint The following conditions must be satisfied TYPEOP1 op1 TYPEOP2 op1 IS_CONNECTIVE op2 e
28. can be replaced by other expressions e Fixed variables variables that are considered to be fixed and cannot be sub stituted by other expressions When a free variable becomes bound to an expression every occurrence of this variable in the initial expression is substituted by this expression A binding is a tuple of pairs of the form v e where vis a free variable and e is an expression If B is a binding and E is an expression we define E B to be the result of the substitution in E of all variables that are bound in B in the order they appear in B A recursive definition of E B is given below 44 EQ E E v e lt B E v e B When matching two expressions the aim is to find a binding of the free variables that makes the expressions identical With respect to binding B variable v can be free bound or fixed Bindings can be merged The result 2160125 of merging two bindings Bi and Ba is a binding that has the property that for all expressions E Bi Bo E Bo By Note that the order of the two arguments in B 0B cannot be reversed We now describe the matching algorithm We define match E1 Bi E2 Ba to return a tuple of three elements f B1 BS The first element is a boolean Its value is true if and only if there are bindings Bi and Bi such that E BOB Es BL Bo If f is true the second and third elements of the result contain the two bindings respectively If f is false they bot
29. d proofs Special attention has been given to make this tool user friendly and easily extendable to calculi other than propositional or predicate The program has been developed for the Apple Macintosh It is written in C and is completely portable except for the part implementing the user interface Biographical Sketch Nikos Papaspyrou was born on January 26 1971 in Athens Greece He attended the 7th High School of Athens and graduated in June 1988 In September 1988 he was admitted to the Department of Electrical Engineering and Computer Science National Technical University of Athens NTUA He graduated in July 1993 with a GPA of 9 58 out of 10 He joined the Graduate School at Cornell University in August 1993 and completed the requirements for the M Sc Degree in September 1994 While a student at the NTUA Nikos Papaspyrou participated in three European Community Contests for Young Scientists Copenhagen 1990 Zurich 1991 and Sevilla 1992 with three computer science projects which took second first and first place in the greek national contest respectively He speaks three foreign languages English French and a little German Since 1985 he has played volleyball on the team of Pangrati Athens which is currently in the third division in Greece 111 Acknowledgements First and foremost I would like to express my respect and thanks to Professor David Gries who supervised my thesis and was always accessible and will
30. ditions have been implemented but cannot be created using the current interface Fact conditions have not been thoroughly tested 5 There is no way to hide obvious hints e g operator symmetry conjunctionality etc This should be in the options menu which has not been implemented For the same reason all files have to be in the same directory as the application file unless full path names are used when including files 6 Operator idempotency associativity identities and zeroes cannot be applied on the fly in transformation steps The author thinks that this is not necessary 86 usually there is a fact doing the same thing and it is not desired to hide the hints except for associativity 7 There is no default type for free variables and quantifier dummies All types have to be specified explicitly 8 Command File Print LaTeX has not been implemented 9 It is not possible to restrict the range of facts to be used when proving a theorem The following features are not present in chapter 2 but are considered to be useful and are treated as unimplemented features 1 There is no way to write comments in a proof especially when applying rules e g Proof by contradiction etc 2 It is not possible to see information about facts and rules apart from command File Show source There should be something easier there 3 It is not possible to see information about other symbols especially o
31. e Dummy reordering op x y R P op y x R P 2 3 The proof editor s internal language Although the syntax of this language may change we think it is necessary to define its basic characteristics and semantics Each file that is processed by the proof editor is of the form lt file gt lt statement gt The following paragraphs describe what statements are gt This is the internal language users need not write in it or read it 30 2 3 1 Using existing files The include statement is used in order to include the contents of an existing file in the current file Its syntax is lt statement gt include lt string gt It should be noted that the included file cannot be changed while editing the file from which it was included For example the proof of a theorem that was defined in the included file cannot be edited 2 3 2 Definition of types Types are defined by statements of the form lt statement gt define type lt id type gt lt id type gt When used in some declarations a type is defined as lt type gt lt id type gt ANY VARIABLE LIST 2 3 3 Definition of constants Constants are defined by statements of the form e lt statement gt define constant lt id constant gt lt id constant gt lt id type gt 2 3 4 Definition of operators Operators are defined by statements of the fo
32. e cannot be defined Nevertheless all types are considered non empty All types are simple our proof editor does not allow types to be built from other types The simplest expressions consist of single variables or constants Variables and constants must be defined before they can be used The definition of a variable or constant assigns to it a name and a type however to simplify the type system we assign a user defined default type to untyped variables There are three kinds of operators e prefix operators i e unary operators of the form o T 7 A prefix operator can be applied to operand z by writing ox e postfix operators i e unary operators of the form o T 77 A postfix operator can be applied to operand x by writing xo e infiz operators i e binary operators of the form o Ti x Ty Tr An infix operator can be applied to operands x y by writing x o y The user can specify operator precedence and other properties Parentheses can be used in order to enforce the order of operations that the user wants In case of ambiguity in the application of operators the proof editor must report an error e g ro yos 2 is ambiguous if it is not known that one of the two operators has greater precedence than the other or that 01 and o are mutually associative Operators can be declared associative see 2 2 5 This allows expressions of the form xo yo z Moreover mutual associativity a
33. efine Axiom and Define Theorem respectively These two will be described together since the process is exactly the same A dialog box similar to the one in Fig 3 7 appears The user must specify the fact s title and number they can be left blank but leaving both blank is not a good idea and the fact s expression Then by clicking button Find free variables the fact s expression is parsed and all free variables are placed in a list The user must then specify each free variable s type from the type popup menu 3 3 8 Defining rules The user can define new rules using command Define Rule The dialog box in Fig 3 8 appears where the user must specify the rule s title and its text The text of the rule is its representation in the proof editor s internal language omitting the initial rule and the title and ending with endrule For more information about the syntax and semantics of rules read 2 3 9 and 2 4 4 3 3 9 Defining operator precedence When a new operator is defined its precedence with respect to other operators is un defined This means that the operator cannot be used in expressions containing other operators without explicit parentheses In order to define an operator s precedence command Define Precedence must be used The dialog box in Fig 3 9 appears This dialog box has two tables The upper table is the precedence table If 69 6 File Edit Define Proof Transform Property Options 1 07 PM
34. erator op is associative This means that there is no ambiguity in expressions of the form x op y op z and no paren theses are needed Such an expression has more than one outermost operator This property can be used to transform on the fly a subexpression of the form x op y op z to x op y op z and vice versa The following condition must be satisfied TYPEOP1 0p TYPEOP2 op TYPERES op e idempotent op specifies that operator op is idempotent This means that a subexpression of the form x op x can be replaced on the fly by x and vice versa The following conditions must be satisfied TYPEOP1 0p TYPEOP2 op TYPERES op e dual op1 op2 specifies that operators op1 and op2 are dual This means that a subexpression of the form x op1 y can be replaced on the fly by y op2 x and vice versa The following conditions must be satisfied not IS_SYMMETRIC op1 not IS_SYMMETRIC op2 e mutualAssoc op1 op2 specifies that operators op1 and op2 are mutually associative This means that there is no ambiguity in expressions of the form x opi y op2 z and no parentheses are needed Such an expression has more than one outermost operator This property can be used to transform on the fly 19 a subexpression of the form x op1 y op2 z to x opi y op2 z and vice versa The following condition must be satisfied TYPEOP2 op1 TYPEOP1 op2 TYPERES op1 TYPERES op
35. ession if possible Distributivity Apply the distributivity quantifier property to the current subexpression if possible Range split Apply the range split quantifier property to the current subex pression if possible Interchange dummies Interchange the dummies of the quantifier that is currently selected as the current subexpression Nesting Apply the nesting quantifier property to the current subexpres sion if possible Rename dummies Rename the dummies of the quantifier that is currently selected as the current subexpression Reorder dummies Reorder the dummies of the quantifier that is currently selected as the current subexpression e Options Various options 55 Proof Options about proofs e g what hints should be displayed or in what form Directories Options about the directories where the system or user files are found Load Load options from a file Save Save options to a file Chapter 3 User s Manual 3 1 Introduction The proof editor that will be presented was developed in the Department of Com puter Science Cornell University as an M Sc thesis by Nikos Papaspyrou and was supervised by David Gries This tool can be used to facilitate the development of proof transformations The current version of the proof editor is 1 0 alpha for Apple Macintosh This version is not complete For more details about unimplemented features and known bugs refer to
36. from file lt filename gt File lt filename gt cannot be read Perhaps there is a problem with the disk Cannot resolve operator precedence Operator precedence between these operators has not been defined The expression containing them is ambiguous Cannot set precedence check all precedences Operator precedence cannot be set because it is already defined Check all prece dences to find where the problem is Cannot write to file lt filename gt File lt filename gt cannot be written Perhaps there is a problem with the disk or the disk is full Constant cannot be lt property gt This constant cannot be given this property Possible reasons are type incompat ibility or another constant has already been given the same property Check the conditions for this property in chapter 2 81 Different array in EXP A different array is given in an EXP expression from what was previously declared in parentheses Identifier has already been defined This identifier has already been defined for something else Use unique identifier names Incomplete proof This proof cannot be completed For details on proof correctness read 2 2 7 Invalid module expected module This file does not contain a valid module A text file must start with module Misplaced identifier A constant or variable identifier is found in an expression in a place where an operator is expected Misplaced operator An operator is found in an expre
37. gt lt id operator gt lt rule expression gt lt infiz oper gt lt rule expression gt lt rule term gt lt id constant gt lt id variable gt lt id function gt lt rule expr list gt lt rule expression gt Ep C lt id operator gt lt rule dummy decl gt cc 99 lt rule expression gt lt rule expression gt lt pred access term gt lt rule seq subst gt lt var list gt lt rule expr list gt lt rule dummy decl gt lt rule part dummy decl gt 3 lt rule part dummy decl gt lt rule part dummy decl gt lt var list gt lt id type gt LIST lt pred access type gt we 3 lt rule type decl gt lt part rule type decl gt lt part rule type decl gt 39 lt rule part type decl gt lt var list gt lt type gt lt pred access type gt lt pred predicate gt IS_CONSTANT lt expression gt IS_SYMMETRIC lt id operator gt IS_ASSOCIATIVE lt id operator gt IS_IDEMPOTENT lt id operator gt HAS_LIDENT lt id operator gt HAS_RIDENT lt id operator gt HAS_IDENTITY lt id operator gt HAS_LZERO lt id operator gt HAS_RZERO lt id operator gt HAS_ZERO l
38. gument Type h O postfix 2nd argument Type SE EJ Set precedence eWindow est InputWindow Figure 3 5 Defining operators 3 3 5 Defining operators By using command Define Operator the user can define a new operator The dialog box in Fig 3 5 appears The user must specify the name of the operator its position i e prefix postfix or infix the types of its arguments prefix and postfix operators take one argument while infix operators take two arguments and the result type If box Set precedence is checked after defining an operator the user will be asked to place it in the operator precedence table 67 E File Edit Define Proof Transform Property Options 105PM 2 lt a Facts test Untitled No proof is being edited Hodule Function name Types argument Argument Type est InputWindow Figure 3 6 Defining functions 3 3 6 Defining functions By using command Define Function the user can define a new function The dialog box in Fig 3 6 appears The user must specify the name of the function the types of its arguments and the result type Initially a newly defined function has no arguments which is not legal By clicking on button Add argument a new argument is added and the user must specify its type 68 3 3 7 Defining axioms and theorems New axioms and theorems can be defined using the two commands D
39. h Ey z 61 Bi Es Z 69 Ba f Bi BS match E1 Bi Ea Ba if f false then return false B BLQB By BLQB BY Bz for i 1 to amp do f Bi By match es B1 e5 Ba if f false then return false B BL B By BLQB 4T Bi gt 162 BY end do return true BY By Finally matching quantifiers is defined as To calculate match o Z Ri E B1 o Z Ra Ea Bo Ba matechDummy 21 72 f Bi BS match Ri B QB1 Ra B Q Ba if f false then return false 7 BY BS gt match E1 Bi By B E2 B ABLA Ba if f false then return false return true BY QB BY QB where matchDummy 1 72 is a binding of dummy variables such that the lists 71 and Z become identical Its definition is left out 2 4 4 The language for rules The simple programming language for user defined rules supports six statements so far It will probably be extended in the future It supports also a new type constructor array of and a new expression constructor EXP a op These will be described together with the if statement A brief description of the semantics of rule statements is given below The syntax of these statements is defined in 2 3 9 where the grammar is given It is not repeated 48 here We explain only what is not clear from the grammar The if statement is the most important a
40. h contain the empty tuple We start with a general rule about matching if match E1 Bi Es B2 f BY BS then match E2 Bo E1 B1 f Bo BY Therefore we do not need to handle symmetrical cases 45 We now define the the matching for parenthesized expressions variables and constants In the following the letter c denotes constants and the letter v denotes variables match E1 By E2 B2 match Ey By Ex Ba If v is free in By match v By Es B2 true v Es a B1 Ba If v is bound in Bi match v By Es B2 match v By By E2 Ba If v and va are fixed in B and Ba respectively and v1 ve match v1 By v2 B2 true Bi B2 Matching of expressions containing operators function applications and textual sub stitution is defined as mateh oE1 By 6109 B2 match E1 By E2 Ba match Bro By E20 Bo match E By Ea Ba To calculate match El o Ef By El o Ef Ba f By By match Ei By Ez B2 if f false then return false f BY BY match E BL B1 E BLOBa if f false then return false 46 return true 3706 21 06 05 To calculate match f El E EP Bi MEL E2 EZ Ba BY 0 By 0 for 1 to n do f BY BL gt match El By El Ba if f false then return false B gt B QB Ba BLQBa BY BIQB BY gt end do return true B1 B3 To calculate matc
41. he current expression e CURR_FACT the current fact if a hint is specified by the user after all substi tutions have been made e CURR_SUBEXP the current subexpression expression 2 2 4 Predicates The following predicates are predefined They can be used only in the definition of rules see also 2 2 5 and 2 3 9 IS_CONSTANT exp expression exp is the name of a constant e IS_SYMMETRIC op operator op has been declared symmetric IS_ASSOCIATIVE op operator op has been declared associative IS_IDEMPOTENT op operator op has been declared idempotent 16 HAS_LIDENT op operator op has been declared to have a left identity HAS_RIDENT op operator op has been declared to have a right identity HAS_IDENTITY op operator op has been declared to have both a left and a right identity and these are equal HAS_LZERO op operator op has been declared to have a left zero HAS_RZERO op operator op has been declared to have a right zero HAS_ZERO op operator op has been declared to have both a left and a right zero and these are equal IS_CONNECTIVE op operator op has been declared connective HAS_DUAL op operator op has been declared dual to another operator or op is symmetric IS_DUAL op1 op2 operators op1 and op2 have been declared dual IS_MUTUAL_ASSOC op1 op2 operators 001 and op2 have been declared mu tually associative IS_PROVE_FF op operator op has been declared proveFF
42. ile Include the user can include other existing modules in the current module A standard dialog box appears which enables the user to choose the proof editor file to be included 3 3 3 Defining types New types can be defined using command Define Type The dialog box in Fig 3 3 appears The user must specify the names of one or more types to be defined separated by commas or spaces 3 3 4 Defining constants New constants can be defined using command Define Constant The dialog box in Fig 3 4 appears The user must specify the names of one or more constants to be defined separated by commas or spaces and select their type from the popup menu that appears 64 File Edit Define Proof Transform Property Options 1 03 PM 2 A Untitled Facts Hodule test No proof is being edited Type name s Hodule test InputWindow Figure 3 3 Defining types 65 File Edit Define Proof Transform Property Options 1 04 PM 2 A i Untitled Facts Hodule test No proof is being edited Constant name s true false Type RuleWindow Hodule test InputWindow Figure 3 4 Defining constants 66 File Edit Define Proof Transform Property Options 1 05PM 2 lt a Untitled Facts No proof is being edited Hodule test Operator name Position Types O prefix 1st ar
43. in Eindhoven University of Technology This tool is an editor allowing the preparation of documents of mathematical nature Although it can be used for the construc tion of formal proofs in propositional and predicate calculus it is more ori ented towards text rather than formulae manipulation and does not provide any checking of validity Chapter 2 Specifications 2 1 Introduction This section describes the basics of the proof editor We first define some of the terms that will be used frequently The terms that are not defined have their usual meaning e g type identifier constant variable operator expression e Fact an expression whose result belongs to the special type boolean Not all boolean expressions are facts only the ones that are valid true in all states e Axiom a fact that is considered to be true with no evidence e Theorem a fact that is considered to be true and its proof is given e Step the result of the transformation of an expression to another expression The two expressions become related with a connective operator e Proof a sequence of steps or other constructs of the proof editor that is con sidered to be the evidence that supports a theorem e Rule a mechanism for deriving steps in a proof An inference rule as defined in GS93 is a syntactic mechanism for deriving truths Inference rules consist of a list of expressions called premises and an expression called the concl
44. ing to help with the numerous problems that came up I would also like to thank Professor Thorsten von Eicken and Professor Steve Vavasis for serving on my special committee My sincere thanks also go to my first advisor Professor Sam Toueg and the support staff of the Department of Computer Science at Cornell University for their outstanding help while I was a graduate student Finally I would like to thank my friends in Ithaca for the good times that we shared Last but not least my wholehearted thanks go to my family and friends in Greece for their love encouragement and support Table of Contents 1 Introduction 1 2 Specifications 3 Dek Tattroduction a e 6 AA 6 a mai Ba p 3 2 1 1 Facts proofs and scopes epica a a a a 4 2 1 2 Types and expressions o o 8 2 1 3 Textual substituti n ad a e e RR a 10 A e n ee oR ant iza Biante Ses ia oly oe tg a ee 7 a 12 2 2 Predefined items eee ae ee Ae Pa A A 12 Dol ANDES 94 0 Sh AAA A A ES 12 Dees VOPETATOLI are a a a ow eek 27 a 83 dat ni 13 Dene NCCESSOIS a Pine Se A oh ea 14 2 Predicates toreni p az 2 Gate od a eel i 27 sear ae on 15 2 2 5 Rules for operator properties 2 2004 17 2 2 6 Rules for transformation steps 04 25 224 Pro ft chnigueg x ar anh b ade amp e dee A A A A 26 2 2 8 Quantifier properties 27 2 3 The pr
45. int must be given after O indicating to which fact the initial expression has been transformed e from fact Starting from a fact the fact is transformed into the expression to be proved The same example expressed as a proof of this type is Theorem p q boolean title Absorption number 3 43a Prove pA pVq p Proof by starting from a fact Reflexivity of 3 5 with p pVq pVq pVq Idempotency of v 3 26 pVa pVpVa Golden rule 3 35 with g pV q pA pVq p O Note that now there is no need for a hint after the O symbol but before the first expression This hint indicates which fact we are transforming e by transformation Starting from some part of the expression to be proved that part is transformed to the remaining part The same example expressed as a proof of this type is Theorem p q boolean title Absorption number 3 43a Prove pA pVq p Proof by transformation PA pV q Golden rule 3 35 with g pvq pVDVg Idempotency of v 3 26 p pVq 0pVq Symmetry of 3 2 with g pVq Pp O Note that there is no need for a hint after the O symbol The connective operator now becomes part of the expression that we are proving To fact proofs have the characteristic that at each step the whole proof depends on proving the current expression Because of this characteristic such proofs allow arbi
46. ion call has fewer arguments than necessary Too few expressions in substitution There are fewer expressions than variables in a substitution Too many arguments in call to function A function call has more arguments than necessary Too many expressions in substitution There are more expressions than variables in a substitution Type mismatch A different type was found from the one expected Undefined lt object gt An object is used but not defined Unknown PED exception Internal error Something wrong with the exception handler Please report this Unrecognized lt object gt This object is not recognized Perhaps a spelling mistake Unterminated comment A comment has not been terminated and the end of the file has been reached 85 Unterminated string A string has not been terminated and the end of the file has been reached 3 6 Unimplemented features and known bugs Here is a list of features that have not been implemented in the current version of the proof editor although they are present in chapter 2 1 Quantifier properties have not been implemented Many things about quanti fiers have not been thoroughly tested so it can be said that in this version quantifiers do not work 2 User defined rules containing EXP terms do not work 3 Dependent proof scopes have been implemented but the current interface does not support them They cannot be used in this version 4 Facts that can be applied under con
47. is specified by the user Delete step Delete the last step in the current proof QED Complete the current proof e Transform Transforming the current expression Apply Apply the current fact to the current subexpression if possible and create a transformation step Substitute fact Substitute the current subexpression which should be an instance of the current fact by the default true value Apply rule Apply the current user defined rule if possible Insert parentheses Insert parentheses around the current subexpression Remove parentheses Remove all unnecessary parentheses in the current subexpression Perform substitution Perform all possible substitutions in the current subexpression e Property Applying operator and quantifier properties Symmetry Apply symmetry or duality of the outermost operator to the current subexpression if possible Conjunctionality Apply the conjunctionality of the outermost operator to the current subexpression if possible 54 Equivalent form Substitute the outermost operator of the current subex pression by any of its equivalent forms Missing range Apply the missing range quantifier property to the current subexpression if possible Empty range Apply the empty range quantifier property to the current subexpression if possible One point rule Apply the one point rule quantifier property to the current subexpr
48. list of variables and is a list of expressions It is true if any of the variables in z occurs free in any of the expressions in 6 the occurrence of a variable in an expression is free if it is not in the scope of any quantification that has this variable as a dummy The formal definition of textual substitution is given in Fig 2 1 The infix operator used in a quantification must be associative and symmetric It must also have an identity 2We allow only substitution of variables 11 if variable v is same as 2 otherwise ea Us Provided not occurs y z o J R E z 8 eg Rila Memorandum the list of variables 1 2 n the list of expressions 1 2 n a variable a constant operators a function a list of dummy variables expressions Figure 2 1 Textual substitution 12 2 1 4 Interface Regardless of the appearance of the interface windows menus etc some things are bound to be needed We will make an effort not to put any unnecessary restrictions on the interface What will certainly be needed is e The current expression This is the whole expression that is being edited When a proof is being edited the current expression is the last expression appearing in the proof e The current subexpression This is the subexpression of the current expression that has been selected for transformation If nothing has been selected the whole curre
49. llows expressions of the form a 01 y 09 2 In general consider an expression of the form Fy 91 Es 92 1 En where n gt 2 and operator precedence does not resolve the ambiguity This expression is not ambiguous if for ali lt i lt j lt n if o 0j is associative if 0 Ao o and are mutually associative 10 General functions can be defined by giving the types of the operands and the result type A function can in general be of the form f Ti x Tax X Th gt T where n gt 1 and can be applied to its operands 29 2 2 by writing f x21 19 Tn Nevertheless for our proof editor functions are just names Quantifications are expressions of the form o 2 R E where o is an infix operator Z is a list of dummy variables R is an optional boolean expression the range if it is omitted it is considered to be the default true value and E is an expression the body The scope of a dummy is the range and body 2 1 3 Textual substitution Textual substitution is the most important operation in our proof editor The nota tion that we will use is E z1 2 2n 1 2 n where n gt 1 E is the expression in which the substitution will take place 21 29 2 are the distinct variables that will be simultaneously substituted and e1 e2 en are the expres sions that will replace them We first define the predicate occurs z e where Z is a
50. nd is presented first e if What needs to be defined is the semantics of the conditions There are four primary conditions for the if statement The first is a predefined predicate The other three are MODE is PROVE_xxx This condition is true if the proof technique that is currently used is PROVE_xxx If no proof technique has yet been declared the proof has just started then the condition is still true and the current proof technique is set to PROOF_xxx x matches y This is the most important primary condition it allows the user to access the structure of an expression The expressions x and y can be either normal expressions with free variables declared in brackets or the special expression constructor EXP a op with a possibly a free variable declared in brackets and op an infix operator In EXP a op ais an array of expressions If the number of expressions in a is n and the expressions are F1 E2 En then the constructor EXP a op is equivalent to the expression Ej op Ea op op En Operator op has to be associative If array a is free when matching EXP a op expressions F1 Fe En are considered free but also their number is not determined However it must be n gt 2 49 When a condition of the form x matches y is given the proof editor is trying to match the two expressions x and y possibly by assigning values to free variables If a matching is possible the condition is true
51. ne point rule QED Import Distributivity Export Range split Print LaTeX Interchange dummies Show source Nesting Quit Type Rename dummies Constant Reorder dummies Open proof Operator Close proof Function Apply fact Cut Axiom Substitute fact Copy Theorem Apply rule Paste Rule Insert parentheses Clear Precedence Remove parentheses Show clipboard Properties Perform substitution We now give more details about the user interface We describe the functions that the user interface should provide In Fig 2 3 we organize these functions into a menu the main menu of our application Some of these functions are used more often than others so we will need more handy ways to access them but this depends on the 51 e File Various file operations New Open a new file with a dummy name Close the current one if any ask for confirmation if it has not been saved Open Open an existing file ask the user for its name Close the current one if any ask for confirmation if it has not been saved Include Include an existing file ask the user for its name in the current one after all other included files Close Close the current file ask for confirmation ifit has not been saved Save Save the current file If no name has been given same as Save as Save as Save the current file ask the user for its name Import Read a text file that contains internal la
52. nguage statements Export Write the current file as text Print LaTeX Print the current file to a IATpX document ask the user for its name Show source Show the source of the current file as it will be saved on disk that is show the internal language statements Quit Quit the application ask for confirmation if the current file has not been saved e Edit Editing commands Open proof Open the proof of the current theorem for editing 52 Close proof Close the current proof Cut Cut the selected text and place it in the clipboard Copy Copy the selected text in the clipboard Paste Insert the contents of the clipboard at the current editing point Clear Delete the selected text Show clipboard Show the contents of the clipboard e Define Various definitions Type Define a new type Constant Define a new constant Operator Define a new operator Function Define a new function Axiom Define a new axiom Theorem Define a new theorem Rule Define a new rule Precedence Define operator precedence Property Define operator properties e Proof Editing the current proof To fact Start a proof to a fact From fact Start a proof from the current fact with its variables substi tuted as specified by the user 53 By transformation Start a proof by transformation starting from the expression that
53. nt expression is taken e The current fact This is the fact that will be applied The user can specify the appropriate variable substitutions if necessary e The current rule This is the user defined rule that will be applied 2 2 Predefined items The following paragraphs present the predefined items of the proof editor 2 2 1 Types There are four predefined types e boolean the type of all facts 13 e ANY a wild card type Useful in definitions of axioms and theorems that contain equality and or textual substitution or for dummy variables in substitutions e VARIABLE a type for variables of any type Useful in definitions of axioms and theorems that contain textual substitution e LIST a type for lists of expressions Useful in definitions of axioms and theo rems that contain textual substitution as well as in quantifiers The first is a normal type whereas the other three are only used for special purposes 2 2 2 Operators An equality operator is predefined for every type T define operator infix T x T gt boolean The precedence of all equality operators is the same All equality operators have the following properties see also 2 2 5 rule symmetric rule connective rule transitive rule conjunctional rule prove rule leibniz 14 2 2 3 Accessors The following accessors are predefined see also 2 2 5 They can be used only when defining rules see also 2
54. nted in the current version of the proof editor so they will not be described in more detail now 18 3 4 5 Parentheses and substitutions There are three more commands that create transformation steps All of them create transformation steps with the equality operator These are e Transform Insert parentheses Insert parentheses around the current sub expression e Transform Remove parentheses Remove all unnecessary parentheses from the current subexpression e Transform Perform substitution Perform all possible substitutions in the current subexpression 3 4 6 Applying user defined rules By using command Transform Apply rule the user can apply a user defined rule The syntax and semantics of user defined rules can be found in 2 3 9 and 2 4 4 respectively To apply a rule the user needs only select it from the rules window Its application may depend on the current expression or subexpression the current fact and the contents of the input window 3 5 Error messages This section presents and explains briefly the various error messages that the proof editor will display when something goes wrong For each error message the line of code that generated it is shown for debugging purposes and if the error is related 79 to text parsing its context is given e g file name and line number Errors are categorized as follows e Internal errors Such errors should never happen They mean that there is a
55. oof editor s internal language o 29 2 3 1 Using existing files ccoo 4 cae e 30 2 3 2 Definition O types o 30 2 33 Definition of constants 30 2 3 1 Definition of operators 2 4494 a a aa 30 2 3 5 Definition of functions 31 2 3 0 EXDEGSSIOII sa mai Bocan A De A alta dl ea 31 2 3 7 Definition of axioms 2 a its a A a ia A 32 2 3 8 Definition of theorems o 33 2 3 9 Definition of rules do al ts e pl d e ds 34 2 4 More detailed specifications 0 0 02000 41 2 4 1 Subexpressions a 2 A A A 41 2 4 2 Structure of expressions 41 2 4 3 Expression matching y ta ea e a da as 43 2 4 4 The language for rules ee da 49 a 47 2 4 5 The interface a os A ee De eae 50 3 User s Manual 56 Sal INTO UCNO A A 2 3 o 8 56 32 files graaz is naia ees ee ee BS ee amp wees 57 3 2 1 Creating a new module 57 3 2 2 Editing existing modules odas aa Mai a 59 3 2 3 Working with text files 59 3 2 4 Other File commands Er rt hao Pa 60 3 3 Working with modules 2 02 0 0020004 60 3 3L Seren JAVON acesi s oe aoe AR ee Re E 60 3 3 2 Including existing modules 63 Defining AI 63 3 34 Defining constants o
56. or e File Show source Display the representation of the current module in the proof editor s internal language 3 3 Working with modules This section describes how the user can edit a module s contents by defining new types constants operators functions axioms theorems properties and rules For a description of editing proofs see the next section 3 3 1 Screen layout When a module is being edited the screen looks as in Fig 3 2 It is separated into four windows 61 S File Edit Define Proof Transform Property Options 11 47 AM 2 A test def Facts Prove x x i Hodule small A Associativity of 1 x 2 Cy 2 Proof by transf rmation xt i A Left identity of 2 Left identity of 2 with x x x gt itx x gt i z zx A Left complement of 3 gt Left complement of 3 with x x gt x 1 x z eee aS TP Right identity of 4 gt Left complement of 3 gt eal an x x aa gt Left identity of 2 with x x gt TU Right complement of 5 x i gt Left complement of 3 with x x gt i RuleWindow Hodule small JE InputWindow Figure 3 2 Screen layout 62 e The proof window In this window the biggest window on the screen the current proof is displayed when a proof is being edited
57. pecifies that a subexpression of the form xi op x2 op x3 op xn 1 op xn can be replaced on the fly by x1 op x2 DEF_AND x2 op x3 DEF_AND DEF_AND xn 1 op xn and vice versa Before this can be applied though a default conjunction oper ator must be defined The following conditions must be satisfied 23 TYPEOP1 op TYPEOP2 0p TYPERES op boolean e equivalent op1 op2 specifies that operators op1 and op2 are equivalent This means that a subexpression of the form x op1 y can be replaced on the fly by x op2 y and vice versa The following conditions must be satisfied TYPEOP1 op1 TYPEOP1 op2 TYPEOP2 op1 TYPEOP2 op2 TYPERES op1 TYPERES op2 It should be noted that operator equivalence is not transitive i e if it has been defined that equivalent op1 op2 and equivalent op2 op3 this does not mean that equivalent op2 op3 e quantifier new op op specifies that when operator op is used in a quan tification the new operator new op should be used instead Note that new op is only a second name for op However it can be used only as a quantifier The following conditions must be satisfied IS_ASSOCIATIVE op IS_SYMMETRIC op HAS_IDENTITY op Finally the following rules can be used to specify the default true and false values and the default conjunction and disjunction operators Provided that the replacement does not create any synt
58. perators It would be useful to be able to see a list of all properties defined for a particular operator 4 Before selecting something in a window the user has to click the window to make it active Therefore for selecting something in a non active window two clicks are necessary Besides the selected lines in a non active window are not shown 87 5 There should be an option to print a proof separately in a IATRX file instead of the whole file Finally here is a list of known bugs some very annoying of the current version 1 It is possible to edit a proof of a theorem that is defined in an included file By saving the file this proof is not saved 2 Clicking button Cancel in the first New module dialog box and then quitting the application causes a system crash 3 The system may crash in low memory situations although a low memory er ror handler has been implemented This may be because exceptions are not handled properly some flag was wrong when compiling 4 Some fatal errors should not be fatal Bibliography BVW94 Roland Backhouse Richard Verhoeven and Olaf Weber Mathpad User C 86 GS93 GS94a GS94b vdS94a vdS94b Manual Technical report Department of Computer Science Eindhoven University of Technology January 1994 Robert Constable et al Implementing Mathematics with the Nuprl Proof Development System Prentice Hall Englewood Cliffs N J 1986 David G
59. ries and Fred B Schneider A Logical Approach to Discrete Math Springer Verlag New York N Y 1993 David Gries and Fred B Schneider A New Approach to Teaching Mathe matics Technical report Department of Computer Science Cornell Uni versity February 1994 David Gries and Fred B Schneider Teaching Math More Effectively Through the Design of Calculational Proofs Technical report Depart ment of Computer Science Cornell University March 1994 Jan L A van de Snepscheut Mechanized Support for Stepwise Refinement Technical report Department of Computer Science California Institute of Technology January 1994 Jan L A van de Snepscheut Proxac an Editor for Program Transfor mation Technical report Department of Computer Science California Institute of Technology February 1994 88
60. rm 31 lt statement gt define operator lt id operator gt prefix postfix lt id type gt gt lt id type gt define operator lt id operator gt infix lt id type gt x lt id type gt gt lt id type gt The precedence of operators can be defined by statements of the form lt statement gt define precedence PREC lt id operator gt KEN PREC Ea lt id operator gt EN Several such statements for several operators create a partial order 0 The definition PREC op1 gt PREC op2 means that op2 binds stronger than op1 whereas the definition PREC op1 PREC op2 means that 1 0 has the same precedence as op2 2 3 5 Definition of functions Functions are defined by statements of the form lt statement gt define function lt id function gt lt id type gt x lt id type gt gt lt id type gt 2 3 6 Expressions Expressions are the most basic part of the internal language They are defined by the following rules lt expression gt lt term gt lt seq subst gt 6 A total order is imposed by the proof editor s interface 32 lt id operator gt lt expression gt lt expression gt lt id operator gt lt expression gt lt id operator gt lt expression gt lt term gt lt id
61. roof gt lt proof gt prove lt erpression gt Y lt proof tail gt In order for a theorem to be considered a fact the proof that follows it must be completed and valid These properties though cannot easily be specified syntacti cally and are ignored for the time being A proof is defined as follows lt proof tail gt fromFact lt hint gt lt erpression gt lt seq of steps gt qea toFact lt seq of steps gt qed lt hint gt lt depends clause gt transform lt erpression gt Y lt seq of steps gt qea lt seq of steps gt lt step gt lt expression gt y 34 lt step gt step lt id operator gt lt hint gt lt hint gt hint lt fact hint gt lt property hint gt lt fact hint gt substFact lt string gt lt seq subst gt lt property hint gt insparen rmvparen perfsub symmetric lt id operator gt dual lt id operator gt lt id operator gt conjunctional lt id operator gt J 2 equivalent lt id operator gt lt id operator gt lt depends clause gt depends lt proof scope gt enddep lt proof scope gt lt assumption gt lt proof gt lt assumption
62. ssion in a place where a term is expected No current expression exists No current expression exists in the current proof No default lt value gt has been defined A default value is needed and has not been defined No proof is being edited Some command that requires a proof to be edited was used without a current proof 82 Operator s cannot be lt property gt This operator cannot be given this property Possible reasons are type incompat ibility or another operator has already been given the same property Check the conditions for this property in chapter 2 Operator has no lt property gt This property is needed and has not been defined for this operator Operator precedence not totally ordered The operator precedence is not totally ordered This operator will not be placed in the precedence table Operator precedence over itself is forbidden You cannot define that an operator has higher precedence than itself Out of memory The proof editor application has run out of memory Try increasing the memory from Finder s command File Get Info Quantifier cannot be defined This quantifier cannot be defined Check the conditions specified in chapter 2 Rule cannot be applied This error message is the result of execution of a fail user defined rule statement Select a fact first You cannot apply a fact because no fact is currently selected in the facts window Select a rule first You cannot apply a rule because no
63. statement gt else lt rule statement gt endif lt scope statement gt assume array lt id variable gt lt rule expression gt prove array lt id variable gt 919 lt rule expression gt lt rule condition gt lt rule cond term gt or lt rule cond term gt lt rule cond term gt lt rule cond factor gt and lt rule cond factor gt lt rule cond factor gt lt rule condition gt not lt rule cond factor gt occurs lt var list gt lt rule expr list gt lt rule primary gt matches lt rule primary gt MODE ig PROVE_FF PROVE_TF PROVE_TR lt pred predicate gt lt rule primary gt I lt rule type decl gt lt rule expression gt L lt id variable gt array of lt id type gt 38 lt pred access type gt 1 EXP gt lt id variable gt lt infiz oper gt lt infiz oper gt lt id operator gt lt meta infiz oper gt cn 3 lt rule expr list gt lt rule expression gt lt rule expression gt lt rule expression gt lt rule term gt lt rule seg subst gt lt id operator gt lt rule expression gt lt rule expression
64. t id operator gt IS_CONNECTIVE lt id operator gt HAS_DUAL lt id operator gt IS_DUAL lt id operator gt lt id operator gt IS_MUTUAL_ASSOC lt id operator gt lt id operator gt IS_PROVE_FF lt id operator gt IS_PROVE_TF lt id operator gt IS_PROVE lt id operator gt IS_RELATED lt id operator gt lt id operator gt IS_CONJUNCTIONAL lt id operator gt IS_EQUIVALENT lt id operator gt 40 lt id operator gt ISDEF_TRUE ISDEF_FALSE ISDEF_AND ISDEF_OR lt pred access type gt TYPEOP lt id operator gt TYPEOP1 lt id operator gt TYPEOP2 lt id operator gt TYPERES lt id operator gt TYPEEXP lt expression gt lt meta infiz oper gt DUAL lt id operator gt CONJUNCT lt id operator gt QUANTOPER C lt id operator gt DEF_AND DEF_OR lt pred access term gt LIDENT lt id operator gt RIDENT lt id operator gt IDENTITY lt id operator gt
65. the internal language before editing these files 3 2 1 Creating a new module When the proof editor application is launched the dialog box in Fig 3 1 appears In this dialog box the user can create a new empty module by giving a module name and clicking button OK Alternatively the user can click button Open and then choose to open an existing file see 3 2 2 The same dialog box appears when the user selects command File New If another module is being edited when this happens it will be closed A warning message will appear if that module has not been saved The user can quit the proof editor by selecting command File Quit Again a 58 S File Edit Define Proof Transform Property Options 1139AM 2 New module Module name Figure 3 1 Creating a new module 59 warning message will appear if the current module has not been saved 3 2 2 Editing existing modules By selecting command File Open the user can open an existing proof editor file If another module is being edited at the time it will be closed the proof editor can work with one current module at a time This command displays a standard dialog box for opening files from which the user can select the file that he or she wants to open Command File Save saves the current module Tf this module was created by using command File New this is the same as selecting File Save as Otherwise the module is saved in the file with which it has been associated
66. trary dependencies that the user can specify by using rules For instance consider the following proof Theorem p q boolean Prove p 4 Proof by mutual implication Prove p gt q Prove q gt p O In this case the proof of p q depends on the two proofs p gt q and q gt p These two proofs will be called auxiliary proofs We now define the notion of scope A scope 18 a part of a proof to a fact containing additional assumptions and auxiliary proofs No auxiliary proof can span across scopes Scopes can be nested that is they can include other scopes Assumptions are facts that are considered valid without evidence However an assumption can have no free variables all variables in an assumption are considered fixed and cannot be substituted by anything Assumptions are only visible within the scope in which they are defined or scopes that are nested in this They can only appear in the beginning of a scope before any auxiliary proofs An example of a proof containing two nested scopes is the following Scopes are shown by indentation Theorem p q boolean number 4 1 Prove p gt q gt p Assume p Al Prove q gt p Assume q A2 Prove p Proof by transforming to a fact p O Assumption Al 2 1 2 Types and expressions Types are generally sets of values In our proof editor though types are just names The set of values that inhabit a typ
67. usion Such rules assert that if the premises are assumed to be truths then the conclusion is a truth also Our proof editor has some predefined inference rules e g Leibniz s rule and provides a small programming language for creating user defined rules The following paragraphs present a brief overview of the proof editor 2 1 1 Facts proofs and scopes There are two basic types of facts axioms and theorems The difference between the two is that axioms become facts immediately after they are typed whereas the orems become facts only when they are proved Each fact can have two user defined identifiers a title and a number e g Axiom p q boolean title Symmetry of number 3 2 States 2 A proof is usually a list of steps Each step consists of a connective operator and a hint The hint is an indication of the fact or the predefined property that is used for performing the step There are three types of proofs e to fact Starting from the expression to be proved it is transformed into a fact An example of such a proof is the following Theorem p q boolean title Absorption number 3 43a Prove pA pVq p Proof by transforming to a fact pA pVq p Golden rule 3 35 with q pVq pVqg pVpva Idempotency of V 3 26 2 4 4 O Reflexivity of 3 5 with p pVq The symbol O in the last line means that the proof has been completed Note that a h

Download Pdf Manuals

Related Search

Related Contents

(1) 複合装置に内蔵している起動装置  AXIS 233D Installation Guide  Capteurs de niveau par plongeur 249 sans cage de Fisherr  Avis 06-2013 du Comité scientifique de l`AFSCA  Installations-/Betriebsnachtrag  MJReichlerB Pratiques85 - Université de Neuchâtel  蓄電池付防災対応型太陽光発電システム  bath bench with padded arms  

Copyright © All rights reserved. Failed to retrieve file