MUSCADET version 4.1 User's Manual
Contents
1. H R X Y gt H1 R X Y addhyp N H1 E 7 H F X Y gt Yl F X addhyp N Y1 Y E yet Be careful with the spaces and are not the same This notation is not compulsory you may prefer to choose the apply symbol for example which is used in several TPTP problems or any other symbol and write everywhere apply R X Y instead of R X Y and apply F X Y instead of F X yY But as this apply symbol may not be known by the prover for each constant relation the equivalence must be given for example 04 20 11 20 VX VY apply c X Y XcY that is for the machine X Y apply inc X Y lt gt inc X Y This has been done for some problems about relations equivalence pre order total order well order which have been proposed for inclusion in the TPTP library for example the problem SET806 4 p which states that set equality defines a pre order relation Moreover upon request from Geoff Sutcliffe different names were used for respectively the constants and the relations of arity greater than 0 in the preceding example subset predicate and subset because other provers could not accept the same symbol for both Nevertheless Muscapet as humans here the matter is naive set theory do not have difficulty in using the same symbol The example in the file variant set806 4 p is the corresponding version of problem SET806 4 p 12 Distribution Mus2. listing display or l display or display A 5 4 2 Modifications in a proof call Additional arguments may be given in whatever order a new time limit and new display options in the form lt option gt to add to remove lt option gt tr for the complete trace pr for the useful proof szs for the result according to the SZS ontology Examples th example th 50 tr or th example_th 50 tr sets the time limit to 50 seconds and displays the complete trace followed by the useful proof th example th pr or th example th pr displays only the result theorem proved or not proved and the time used tptp SETO27 4 p pr szs or tptp SETO27 4 p pr szs displays only the result according to the SZS ontology 5 4 3 Modifications under ProLoG 04 20 11 13 The following commands modify the options until next change assign timelimit lt time gt or modifytimelimit lt time gt assert display lt option gt retract display lt option gt 5 4 4 Modifications of Provoc code file muscadet en Finally default values can be modified in the file muscadet fr by modifying the line timelimit or by removing or adding lines display 5 4 5 Instructions for on line use Instructions for use may be found again by typing th or tptp under Linux or th or tptp under PROLOG 5 4 6 Modification of the language choice It is possible to modify the default choice for the language
3. definition A subset B lt gt X X elt A gt X elt B definition X elt powerset A lt gt X subset A definition X elt A inter B lt gt xX elt A amp X elt B Remark defining infix operators must be done in all files where they occur Under Linux resp Protos call the executable resp pr dicat th with as an argument a file or a path to a file Under Protoc this argument must be an atom It must be written between quotes if necessary according to ProLoc conventions Examples th examplel resp th examplel Under Protos it is also possible to call th with a file containing only d finitions which will be read and memorized In this case do not put the corresponding include in the file of theorems this would duplicate the definitions then also the rules 12 Until version 2 6 it was possible to read definitions alone build and memorize the built rules in a file which could be read in a later execution This was because building rules was relatively long comparatively to proving theorems This possibility was removed in version 2 7 Because of the improvements in execution time of modern machines restoring it seems to me unnecessary For very large date bases as for the very large TPTP problems it would be necessary to select definitions and axioms in function of the given problems before building rules not only select rules after having
4. AA cco E E E as 20 T2 Distribution rcs sine scsi airen arine aa ea E nue teen EEEE eas ENERE OEREN RE ea 21 Vd e Refere NCES anas ereere aa aa aa sien wens es aE E E aa day soup a aa E a COKA ESTEER aat 21 1 Introduction The Muscaper theorem prover is a knowledge based system It is based on natural deduction following the terminology of Bledsoe Bledsoe 71 77 and uses methods which resemble those used by humans It is composed of an inference engine which interprets and executes rules and of one or several bases of facts which are the internal representations of theorems to be proved l French version in http www math info univ paris5 fr pastre muscadet manuel fr pdf 04 20 11 Rules are either universal and put into the system or built by the system itself by metarules from data definitions and lemmas given by the user They are in the form if lt list of conditions gt then lt list of actions gt Conditions are normally properties that are quickly verified Actions may be either elementary actions which are quickly executed or super actions which are defined by packs of rules The representation of a theorem to be proved or a sub theorem is a description of its state during the proof It is composed of objects that were created of hypotheses of a conclusion to be proved of rules called active rules possibly of sub theorems etc At the beginning it is only composed of a conclusion which is t
5. Cuba 2001 49 68 Pastre D Strong and weak points of the Muscaper theorem prover AI Communications 15 2002 147 160 http www math info univ paris5 fr pastre AICom AIC263 pdf Pastre D Complementarity of natural deduction and resolution principle in empirically automated theorem proving rapport interne 2006 http www math info univ paris5 fr pastre compl ND RP pdf Pastre D Complementarity of a natural deduction knowledge based theorem prover and resolution based provers in automated theorem proving rapport interne 2007 http www math info univ paris5 fr pastre compl NDKB RB pdf Pastre D Natural proof search and proof writing Conferences on Intelligent computer mathematics Workshop on Mathematically Intelligent Proof Search Paris 2010 http www math info univ paris5 fr pastre mips pdf http www math info univ paris5 fr pastre slides mips pdf Sutcliffe G The TPTP Problem Library and Associated Infrastructure The FOF and CNF Parts v3 5 0 Journal of Automated Reasoning 43 2009 337 362 23 PuscabET was the name given at that time to the first PRoLoc version de MuscapeET 04 20 11 DIa
6. action addhyp handles the hypotheses that have to be added in order to finally add only hypotheses that are elementary and not universal Conjunctions are split Universal hypotheses are not added Rather in the place of universal hypotheses new rules which are local for the sub theorem are created Here are some of the rules that define this super action addhyp N H E step action E to add a conjunction the elements of the conjunction are successively and recursively added H A amp B gt addhyp N A E addhyp N B E if H is already a hypothesis nothing is done hyp N H _ gt true the same for a trivial equality oe H X X gt true lexicographic order except for created objects z lt number gt which are in the order of their creation numerical H Y X atom X atom Y before X Y addhyp N X Y E2 if H is universal or is a implication rule s are created which are local for the theorem of number N ay _ gt create name rule rulehyp Name buildrules H _ N Name H A gt B gt create name _rule rulehyp Name buildrules H _ N Name else H is added assert hyp N H E 5 How to use Muscapet4 The package contains a Protoc source file muscadet en a script musca en which allows to work under Protoc and two small C files th en c and tptp en c which can be co
7. are active for a sub theorem to be proved is memorized by the fact rulactiv N R1 R2 R1 R2 is a list of names of rules that were automatically activated in an order that is important 4 3 Expression of rules The rules simplified that were used in the example are written rule N gt concl N A gt B Step addhyp N A NewStep newconcl N B NewStep rule N concl N XX C Step create objects and replace N XX C C1 Objects newconcl N C1l NewStep rule N def concl pred concl N C Step definition Name C lt gt D newconcl N D NewStep rule N stop hyp _concl concl N C Stepl ground C hyp N C Step2 not hyp N elt X B _ newconcl N true NewStep these three rules are given in the system rule N subset hyp N subset A B Stepl hyp N elt X A Step2 not hyp N elt X B _ addhyp N elt X B NewStep this rule was built by the system The parameter N helps to apply a rule to the sub theorem of number N Notice that if then is implicit It would have been possible to define ProLoc operator symbols if then but this was not indispensable since all is translated into ProLoc with predicates Conditions are generally the verification of the existence or of the absence of facts which are unit Protoc clauses hyp concl see the preceding section or of a definition which is in a certain form There may also be elem
8. statement or equalities between a functional and simple expression and a more complex expression The matching does not have to be very precise because if the classification as a lemma or as a definition is crucial for some statements it is unimportant for most of them 7 Elimination of functional symbols Strategies of Muscapet are designed to work with mathematical or logical predicates rather than with functional symbols Nevertheless Muscaper accepts statements written with functions but it eliminates them by giving a name to functional expressions which will replace this expression in the predicative formula So p f a will be replaced by f a b A p b The symbol is used to 15 Since version 3 TPTP has types or roles definition and lemma but their use is not that which is described here Definitions mentioned here are declared as axioms in TPTP 04 20 11 15 express that b is the object f a and the formula f a b will be handled as if it was a predicative formula p a b For formulas with variables it is a little more complicated A statement of the form p AX where f is a functional symbol is equivalent to the two following statements VY f X Y p Y and AY AX Y p Y Depending on the context one or the other of these two statements is preferable The reasons for this are developed in Pastre 89 For this a new quantifier is used which is named for the only equal to For the only Y e
9. the hypothesis H and the new conclusion is C replaces the conclusion by a c c and adds the two hypotheses a Cbandbcc In effect hypotheses H are analyzed before being added a super action addhyp H contains among others the rule if H is a conjunction then successively add all the elements of the conjunction This rule is of course recursively applied if necessary The conclusion is then replaced by its definition VX Xea gt Xec by applying the rule 04 20 11 2 Rule def_concl_ pred if the conclusion is C there exists a definition of the form C lt D then the new conclusion is D By the preceding rules V and there is then a new object x a new hypothesis xea and the conclusion is now xE c The following rule Rule c if there are hypotheses ACB and XE A then add the hypothesis Xe B is a rule that was automatically built by Muscapet from the definition of inclusion Here it is applied twice adds the hypotheses xe b then xe c which is the same as the conclusion to be proved The proof ends by applying the rule Rule stop _hyp_concl if the conclusion C is also a hypothesis then set the conclusion to true Muscapet is able to work in second order predicate calculus and the preceding example may be written in the form transitive C with the definition of the transitivity of a relation R transitive R VAVBVC R 4 B A R B C gt R A C After the conclusion transitive c is replaced by its definition the proof is
10. used to display the traces complete trace and or useful trace and other comments by giving it fr or en as an additional argument in the command or the pr dicate th or tptp Examples th examplel en or th examplel en Under Protos it can also be directly modified par assign lang en or simply en Nevertheless the names of the rules and actions will not be modified For this the english version must be used files en 5 4 7 Deletion Under Protoa to delete all the data relative to the last problem and solve a new problem without restarting Prooa type deleteall To delete only the facts which represent the state of the last proved or not proved theorem type deleteth which deletes all the facts which represent the state of the last theorem but the definitions and the built rules are not deleted 6 Definitions and lemmas Definitions are not the only mathematical knowledge that is given to the system Lemmas may also be given by means of a Protoc predicate lemma lt name gt lt statement gt For example the transitivity of the inclusion may be given as a lemma to prove theorems of algebraic topology by lemma trans_ subset subset A B amp subset B C gt subset A C On the other hand many statements which are given in the problems of the TPTP library are lemmas and not definitions 13 for example in domain MGT Management MP If a time point belongs to the environment the
11. MuscaDET Version 4 1 User s Manual http www math info univ paris5 fr pastre muscadet manuel en pdf 2011 Dominique PASTRE LIPADE University Paris Descartes pastre math info univ paris5 fr SMEL ag OIC HON sar 0d T E ead scat stows Sud tach card A A E 1 Die ANU LOS shears e E Gus it T Eaa o AE aa O a Ameen E N SA 2 ZV VP AMS TEV ILY of inclusion ra soe tts are eaan eco A aa E AE A Sa A Aaa A a a ai RE 2 2 2 Power set of the intersection of TWO sets ssssessssessesssesressessresressessresresstesessresssressseeesseresseee 3 SF POM M sc detI to Muscadet4 esnin e a A a a aa e a aTi 4 4 Machine representations iseenese ea N E E EE E E E E R R 7 4 1 Expression of mathematical Statements is 5sccscecwasseednsdescadssheateaaidesecaeednaedndduenduvabestiaasespebesahers 7 AD Expression of facissi a ra a pac Qu tin nly a E S 8 ASS D AU TE O i A0 SEAE E E E AE A E E EEE EE AE ENE AS 8 AA EXPLeESSION OF SUPel ACUIONS scenos iso a iae eE ERR E ERE A E E E reas E E EEEa 9 5 How t seMuscadet4 6 acs ai aun en a iE a E OEE A E EE titer O i 10 Sele HOPE OE prooi moine a a a a a aa e e a NTa 11 5 2 From files containing theorems and definitions s sseesseseessesseeseeseesssesressessreseessssssssresssresse 11 5 3 From the TETP Hbrary sereme ea E E A aE aN 13 5 4 Modification of default Opt Ons isc iyceisaceasersaz sees iedeonausapstechveosasiyedd wes tousecaes eel tavaee ition seewdststaaed 13 6 Definitions and Icin
12. as more lost than gained So it has been removed But it would nevertheless have to be 04 20 11 17 restored because the proof may also be more aesthetic For example to prove that the composition of two injective mappings f et g is injective one considers two objects a and a which have their images g f a and g f a equal A rule R built from the definition of mapping builds the objects b fla and b f a On the other hand another rule R c built from the definition of composition builds the objects c f a and c f a such that g c g c fla gfla Then bo c c b uniqueness of images of a and a and injectivity of g then that a a injectivity of f If R is applied before R c and c are first created and b and b are not created because a and a have already an image both objets b and b are then not created 10 Some strategies The following strategies are rather classic ones They come from natural deduction Sometimes it is necessary to avoid carrying out some treatments too early in order to avoid possible infinite branches or too much splitting 10 1 Processing of universal conclusions and of implications Their treatments are simple and systematically performed by the rule V and These rules have been seen in section 2 their type is universal and consequently they have priority Rule V ifthe conclusion isVX P X then create a new object x and the new conclusion is P x Rule if the conclu
13. building them 04 20 11 12 The proof will be saved in a file named res lt name of the theorem to be proved gt for example res_th1 Moreover some messages are displayed on the terminal to follow the prover s work 5 3 From the TPTP library http www cs miami edu tptp Under Linux resp Protoc call the executable resp predicate tptp with as an argument a path to a TPTP problem file or a TPTP problem name In this last case it is necessary to have defined an environment shell variable TPTP to the TPTP library setenv TPTP lt directory of the library gt Examples tptp home dominique TPTP TPTP v4 0 1 Problems SET SET002 4 p tptp SETO27 4 p Under Pro oc the argument must be an PROLOG atom then quotes are necessary occurences of capital letters tptp home dominique TPTP TPTP v4 0 1 Problems SET SETO 02 4 p tptp SETO27 4 p The proof will be saved in a file named res _ lt problem name gt for example res SET002 4 p Moreover some messages are displayed on the terminal to follow the prover s work 5 4 Modification of default options 5 4 1 Default options Default options file muscadet en are time limit 10 seconds display of the trace of the complete search of the proof no display of the useful proof yes result according to the SZS ontology no They may be modified To display them type listing timelimit or 1 timelimit or timelimit T
14. capsT4 is available at the address http www math info univ paris5 fr pastre muscadet muscadet html contains short directions for use muscadet en is the complete Pro oe file musca en is a Unix script which allows you to work under Protoc you must then call prove th or tptp See section 5 or type th or tptp with a point without any argument to diplay the instructions for use th fr c and tptp fr c are small C files which allow to work under Linux Compile them Let for example th and tptp be the obtained executables th allows to work with data previously saved in files see section 5 2 tptp allows to work on the TPTP library see section 5 3 th and tptp without any arguments diplay the instructions for use examples gives a directory of examples with data files and executions 17 in French muscadet fr 18 in French musca fr 19 in French demontrer 20in French th fr cettptp fr c 2l commands cc th en c o th and cc tptp en c o tptp 22 in French exemples 04 20 11 21 13 References Bledsoe 71 Bledsoe 77 Pastre 78 Pastre 89 Pastre 89a Pastre 93 Pastre 95 Pastre 98 Pastre 99 Pastre Ola Pastre 01b Pastre 02 Pastre 06 Pastre 07 Pastre 10 Sutcliffe 09 Bledsoe W W Splitting and reduction heuristics in automatic theorem proving Journal of Artificial Intelligence 2 1971 55 77 Bledso
15. disjoint This clearly shows that it is the property non disjoint that is mentally the most important property This is also the case for Muscapet which is better able to handle positive properties than negative properties In the first MuscabeT version moreover the definition of non disjoint was given and the fact that two sets were disjoint was expressed by the property non disjoint Muscapet2 was able to perform automatically the transformation from the definition of disjoint disjoint A B 3 X Xe A XE B It notices that the definition begins with a negation it then replaces this definition by both of the following definitions not disjoint A B 3 X X A Xe B and disjoint 4 B lt not disjoint 4 B In the TPTP library the statements are given together with there nature hypothesis axiom or conjecture 1 Their name even if it contains the word definition or defn must not be used by the system The conjectures in TPTP are the theorems to be proved in Muscapet In TPTP there is then a difference between hypothesis and axiom which is useless for Muscaper On the contrary in TPTP no distinction can be made between definition and lemma although it is important for MuscabetT For this reason all TPTP hypotheses and axioms are analyzed and are classified either as lemmas or as definitions Definitions are roughly universal properties that are equivalences between a predicative and simple expression and a more complex
16. e W W Non resolution theorem proving Journal of Artificial Intelligence 9 1977 1 35 Pastre D Automatic theorem Proving in Set theory Journal of Artificial Intelligence 10 1978 1 27 Pastre D Muscapet An Automatic theorem Proving System using Knowledge and Metaknowledge in Mathematics Journal of Artificial Intelligence 38 3 1989 Pastre D Muscapet Manuel de l utilisateur 1989 Rapport LAFORIA n 89 54 62p Pastre D Automated theorem Proving in Mathematics Annals on Artificial Intelligence and Mathematics 8 3 4 1993 425 447 Pastre D Entre le d claratif et le proc dural l expression des connaissances dans le syst me muscabeT Revue d Intelligence Artificielle 8 4 1995 361 381 Pastre D Puscapet Manuel de l utilisateur 1998 Rapport interne 62p Pastre D Le nouveau Muscaper et la TPTP Problem Library colloque sur la M taconnaissance Berder 1999 rapport LIP6 2000 002 http www lip6 fr reports lip6 2000 002 html 54 98 and http www math info univ paris5 fr pastre berder99 ps Pastre D Muscapet2 3 A Knowledge based Theorem Prover based on Natural Deduction International Joint Conference on Automated Reasoning IJCAR 2001 Conference on Automated Deduction CADE JC 685 689 Pastre D Implementation of Knowledge Bases for Natural Deduction 8th International Conference on Logic for Programming Artificial Intelligence and Reasoning 2nd International Workshop on Implementation of Logics
17. e below Among the actions steps numbering messages writing traces N rule Name lt condition or list of conditions gt lt action or list of actions gt lt step gt lt explanation gt lt list of the steps of the conditions gt memorizes the informations which will be later necessary to extract the useful trace 4 4 Expression of super actions Super actions are generally expressed by packs of rules if then or if then else To action X if then if then else is easily written in PRoLoG action X a T gt u 52 SSR ae by default optional The super action newconcl which contains only one rule replaces the conclusion of the sub theorem of number N by C if the conclusion is not already equal to C newconcl N C Step not concl N C _ step _action Step assign concl N C Step with step _action El var El step E gt El is E 1 assign step E1 7 Erue If 1 has not yet been instantiated which is the case in the rule the step number is incremented by 1 8 because gradually added during experimentations but they could be automatically added from simplified rules 04 20 11 9 If 1 has been instantiated which is the case in the rule gt where 1 has been instantiated by the first action addhyp described hereafter it is the same step assign updates the conclusion and the number step The super
18. e which does not have high priority performs the treatment of the first existential hypothesis that has not yet been treated then Muscapet again applies rules that have higher priority before treating the following existential hypothesis This allows Muscapet to create the new objects one by one and successively in all the directions 10 6 Processing of disjunctive conclusions Only simple and logical properties are applied A disjunctive conclusion is true if one of the elements of the disjunction is true If one of the elements of a disjunctive conclusion is a negation A A is added as a new hypothesis and A is removed from the conclusion Some treatments such as replacing the conclusion by its definition are also performed on one of the formulas of a disjunctive conclusion If the disjunction contains conjunctive sub formulas the conjunctions are pushed to the outside in order to obtain a conjunctive conclusion which in turn will lead to splitting 10 7 Processing of disjunctive hypotheses Simple rules handle trivial cases For example a hypothesis AVA is replaced by A Other example if one of the elements of the disjunction is already a hypothesis or is of the form X X this hypothesis is removed Then splitting may be done but as for existential hypotheses the disjunctive hypotheses are first added without treatment Later a rule which does not have high priority performs the treatment of the first disjunctive
19. eads to more flexibility more facilities for writing and even more efficiency Moreover it was possible to carry out many improvements and to write new strategies which were not possible in the first version It was also possible to use without having to implement them all the facilities of expression of ProLoc such as numerical calculus missing in Muscapet1 or infix and partially parenthesized notations by simply defining operators and precedences but this is not compulsory it is only more convenient for the user To indicate mathematical variables or constants ProLoc conventions are used variables start with upper case letters whereas constants start with low case letters So it is no longer necessary to precise if a symbol is a variable or a constant but this convention must imperatively be used Muscapet2 was able to work on problems of the TPTP Problem Library Thousands of Problems for Theorem Provers http www cs miami edu tptp New strategies were added which were better adapted to the style and to the axiomatizations of this library Moreover two convenient capabilities of Muscaper had to be left out The first one was the possibility to declare that some statements are either definitions or lemmas or know theorems These two types of statements are not treated in the same manner and MuscapeT must now analyse them to recognize them see section 6 The second capability was the fact that MuscapeTl knew the set belonging symbo
20. entary conditions Actions are either elementary actions which are expressed as Protoc predicates and express elementary programs create objects and replace or super actions which are defined by packs of rules addhyp newconcl etc see next section 04 20 11 8 The condition not hyp N elt X B _ avoids applying the rule if the theorem of number N already contains the hypothesis elt x B In the example this condition only avoids the call addhyp which would have no effect here but in other cases it is essential for example to avoid an infinite creation of objects For Muscapetl this condition was not necessary because a rule could not be applied twice for the same instantiations This had other disadvantages for example it was not possible to force a rule to be applied again for the same instantiations The elementary action create objects and replace N XX C C1 Objects returns in Objects a list of constants z z1 z2 etc which have not yet been used and replaces in C the variables of XX by these constants to give C1 Actually operational rules are more complex they contain additionnal conditions and actions which have been added by hand for the rules given to the system but which are automatically added for rules built by the system The first rules may be seen in the file muscadet en the last ones in the files of built rules rul _ Among the conditions the Step number which will be used in traces se
21. g 6a Speer eye teen mr eee E E S me erent ete nen ee aero 14 7 Elimination of TUNCHONALlSYMDOIS lt o iiccevsdesaidaresctedateedeguoshunadeusdeseaeaauercoes dadens veers taastonstadigctadanededts 16 8 SULA PUG arenen aE a A lea a o a acca E a a lacoste E E EEE 17 9 Activation and Order OF TULES oraniensis ai iiia danas A EESE EEEE ET E EEA aE A aE 17 KOBRO ERL EN A EE A ES E EN E E E ue ceed A oblonga 18 10 1 Processing of universal conclusions and of implications ceeeeeeceeeeeeseceeeseeceeeeeeeneeeens 18 10 2 Processing of conjunctive conclusions 2 0 eeceesceeseeeeseceeeeseeceseeeeeeceseeeseeeeseeeeeecstaeeeesneees 18 10 3 Processing of universal hypotheses iy54esce edhs cau teed ccscadsbuapalecenapeas ieee tuules nc dasteaaiavenesileta Coneas 19 10 4 Processing of existential CONCIUSIONS sites cusiane uit tare detiveruioa cid ier eat Wecuhonscv laden i ness 19 10 5 Processing of existential hypotheses 2 sec ssvesccascgsdes vesdseeeaccenses vessecadcgaues cope dvensenelenaettiadites 19 10 6 Processing of disjunctive conclusions sic5s scetevs saqanchosscasacsdnnesabvnenscvsdsanaeebunneateesantshxdetidunlenaads 19 10 7 Processing of disjunctive hypotheses a sis ceswe tccscchccncessdhesecdsy cadenend avencssecodyas lesttagennesastenea y 19 10 8 Knowledge specific to certain COmains ccceecccescceseceseeeeeeeeeceseeesceeeseeeseecnseceseeeeeeesaees 20 Tl Second order SLAC eI x sacs iner tahoe ute sae eh talon shes cl
22. h version 11 musca fr for the French version 04 20 11 zile theorem th1I03 A B C subset A B amp subset B C gt subset A C examplelbis op 200 xfy elt op 200 xfy subset theorem th103 A B C A subset B amp B subset C gt A subset C definition A subset B lt gt X X elt A gt X elt B example2 include example2 definitions transitivity of subset theorem thI03 A B C subset A B amp subset B C gt subset A C the power set of an intersection is equal to the intersection of the power sets theorem th1I21 A B subset powerset inter A B inter powerset y A powerset B with exemple2 definitions definition subset A B lt gt X elt X A gt elt X B definition elt X powerset A lt gt subset X A definition elt X inter A B lt gt elt X A amp elt X B example2bis include example2bis definitions op 200 xfy elt op 200 xfy subset c Op 150 x x inter transitivity of subset theorem thI03 A B C A subset B amp B subset C gt A subset C 6 the power set of an intersection is equal to the intersection of the power sets theorem thI21 A B powerset A inter B subset powerset A inter powerset B with example2bis definitions op 200 xfy elt op 200 xfy subset op 150 xfx inter
23. he file muscadet en To prove p p simply type prove p gt p Do not forget the dot at the end No space before the bracket Let us come back to the first example Introduce the definition of the inclusion by the ProLoc command assert definition subset A B lt gt X elt X A gt elt X B Then call for the proof prove A B C subset A B amp subset B C gt subset A C Do not forget dots The proof will be displayed on the standard output If you prefer use infix operators type op 200 xfy elt op 200 xfy subset assert definition A subset B lt gt X X elt A gt X elt B then prove A B C A subset B amp B subset C gt A subset C 5 2 From files containing theorems and definitions Data must be written as below op lt precedence gt lt type gt lt name gt eventually theorem lt name gt lt theorem to be proved gt definition lt definition gt lemme lt name gt lt lemma gt include lt data file gt lt PROLOG comment gt Do not forget the dots They are Proog terms All this data may be written in whatever order There may be several theorems which will be proved one after the other include allows to write data in one or several other file s Files examples examplel definition subset A B lt gt X elt X A gt elt X B 10 muscadet fr for the Frenc
24. he initial statement of the theorem to be proved and of a list of rules which are called active i e relevant for this theorem and which were built automatically Active rules when applied may add new hypotheses modify the conclusion create new elements create sub theorems or build new rules which are local for a sub theorem If the conclusion was set to true for example if the conclusion to be proved was added as a new hypothesis or if there is an existential conclusion 3X p X and a hypothesis p a then the theorem is proved If it is only a sub theorem this information is transmitted up to the theorem that created it 2 Examples In all this text ProLoc conventions will be used to write constants names starting with a lowercase letter or variables names starting with an uppercase letter or with the symbol _ Moreover this conventions will be extended to predicates which is not possible in ProLoa and by extension P X will be used to write whatever expression which depends on X 2 1 Transitivity of inclusion Prove the transitivity of inclusion VAVBYC ACB A BCC ACC with the definition of inclusion ACB amp VX XE A XEB To prove this theorem Muscapet creates objects a b and c by applying three times the rule Rule V ifthe conclusion is VX C X then create a new object x and the new conclusion is C x and the new conclusion is acbabcc gt acc Then the rule Rule gt if the conclusion is H C then add
25. hypothesis AvB that has not yet been treated and prepares splitting by replacing the conclusion C par A gt C A B gt C Splitting will then be done by the rule concl_ It is important not to split too early in order not to multiply splitting uselessly in the case of many useless disjunctive hypotheses 10 8 Knowledge specific to certain domains Knowledge specific to topological linear spaces Pastre 89 which were given in Muscapet in the form of operational rules have not yet been put into the following versions Rather than directly 16 It is not physically removed the fact that it has been treated is only memorized 04 20 11 19 translating them by Protoc clauses I intend to write them as mathematical statements and to write metarules which will be able to generate these operational methods On the other hand work on discrete geometry Pastre 93 was continued in Muscapet12 and this allowed us to obtain more satisfactory results while helping the system less 11 Second order statements We saw in section 2 1 that Muscapet is able to work in second order predicate calculus So for the example in section 2 1 example file example order2 the property of transitivity for a relation may be defined by transitive R VA VB VC R 4 B R B C R 4 C or transitive R E VAe E VBE E VCEE R A B A R B C R A O and the theorem may be transitive C or VE transitive c PEJ that is for the machine transitive inc
26. ion of the first sub theorem is pccpd and it is replaced by its definition WX XE pc gt Xe pd A new object x is created a new hypothesis xe pc is added and the new conclusion is xe pd The following rule which was automatically created from the definition of the power set Rule P if there are hypotheses P A B and Xe B then add the hypothesis XCA gives the hypothesis xcc The following rule Rule defconcl elt if the conclusion is Ae B there is a hypothesis Term B and a definition Xe Term amp P X then the new conclusion is P A replaces the conclusion by xe pa A xe pb The rule concl_A leads to a new splitting the conclusion of sub theorem 11 is xepa which is replaced by xca by the rule defconcl_ elt By the rules def_concl_pred W and t is created the hypothesis tex is added and the new conclusion is tea then the rule c gives the hypothesis te c The following rules were automatically created from the definition of the intersection Rule a1 if there are hypotheses ANB C and Xe C then add the hypothesis XE A Rule A2 if there are hypotheses ANB C and Xe C then add the hypothesis Xe B Rule 73 if there are hypotheses ANB C Xe A and XE B then add the hypothesis Xe C The rule M1 then gives the hypothesis te a which ends the proof of sub theorem 11 Sub theorems 12 then 2 corresponding to other cases coming from splitting are then proved 3 From Muscapetl to Muscapet4 3 1 Muscapet 1 A first version of Muscapet which i
27. l and that it is not possible in the TPTP library Rules which used it had to be generalized For example the rule defconcl_rel seen in section 2 2 has been replaced by the more general rule Rule defconcl_ rel if the conclusion is R A B there is a hypothesis Term B and a definition Xe Term amp Def then the new conclusion is the expression obtained by replacing X by A in Def Muscapet has participated to CASC competitions http www cs miami edu CASC since 1999 Muscapet of course could only compete in the first order divisions that is FOF FEQ and NEQ since it does not work with clauses The results Pastre 06 07 show the complementarity of Muscapet with regard to provers based on the resolution principle Pastre 99 gives an analysis of some insufficiencies of Muscapetl which were tackled in Muscapet2 and the description of some new strategies which were conceived during the work on the TPTP library The users of Muscapetl could also find in Pastre 98 a more detailed correspondence between some of the techniques of both versions In addition to unceasing enlargement of the bases of rules and improvements of proof strategies in the last versions of Muscadet2 for TPTP problems the user could call under Linux an executable C file which itself called Protoc and the prover The interest is that it is easier to use and that it is possible to write scripts to solve lists of problems On the other hand working under Protoc al
28. lows 5 There was already such an executable in CASC versions but it gave only the result prove or not proved and not the proof or the search of the proof 04 20 11 5 to look at the bases of facts after an execution or an interruption and even to test a rule by forcing it to be applied 3 3 MUSCADET3 Since 2008 the syntax of Muscapet3 Pastre 10a 10b has been that of the TPTP library Although this was not absolutely necessary the symbol used in the expression for the only Y f X such that p Y was replaced by to avoid the confusion with the of TPTP used in writing quantified formulas for all X p X t X p X exists X p X X p X for all X for_all Y p X Y L X E amp Y exists X exists Y p X Y are written 2 X Y p X Y A and B A amp B A or B A B not A A only f X Y PY only f X Y PY The second important modification of version 3 is the possibility of getting and displaying the useful trace For this it was necessary to be able to go back from the final step to antecedent steps To this end steps have been numbered and became new parameters for facts rules conditions and super actions A step corresponds to the effective application of a rule So a step may involve several actions Facts as hypotheses and conclusions are memorized with the number of the step where they have been obtained So several facts may have the same
29. mpiled and which allow to work under Linux The obtained executables will be named later on th and tptp Working under Protoc allows in particular to have access at the end of the proof or more important in case of failure to all facts representing the state of the theorem to be proved hyp concl sousth rules in particular built rules etc and even to directly test the application of a rule on the current state It is possible to work from a file containing a list of definitions and one or several theorems to be proved It is also possible to directly work on the problems of the TPTP library after having defined an environment shell variable TPTP to the TPTP library setenv TPTP lt directory of the library gt Under Protos it is also possible to call directly the predicate prove with as a parameter the statement of the theorem to be proved after having given the definitions of the mathematical concepts eventually used 9 muscadet fr musca fr th fr c and tptp fr c for the French version 04 20 11 10 The Protoc used is SWI Prolog which is freeware downloaded at the following address http www swi psy uva nl projects SWI Prolog download html and which is called by the command swipl In all cases you have to be in a directory that contains the Protoc file muscadet en or a same name link to this file 5 1 Direct proof only under Protos Call the Unix command musca en This invokes SWI Prolog and loads t
30. n th nd point of the environment cannot precede it input _formula mp environment end point axiom E T environment E amp in environment E T gt greater or equal end_time E T ay es 14 as Definition of greater or equal i t o greater and equal input_formula definition greater or equal axiom X Y greater or equal X Y lt gt greater X Y equal X Y 04 20 11 14 Definitions and lemmas both lead to building rules but not exactly in the same manner For example in a conclusion ACB will be replaced par its definition VX Xe A gt Xe B but ACC will not be replaced by ACB ABCC On the other hand from a lemma containing the sub formula p X gt q f X the rule if p X and AX Y then q9 is created and under some conditions the rule if p X then create Y and add the hypotheses f X Y and q Y is also created but from the definition of the power set XEP A amp XCA the system only creates the rule si Xe A and P A PA then add XCA it does not create the rule if XCA then create the power set of A Lastly Muscapet sometimes builds news definitions which are better adapted to its strategies This is the case for example for the property being disjoint for two sets of Two sets are disjoint if they have no common element The mathematician uses the adjective non disjoint he she does not say that two sets are not disjoint but that these two sets are non
31. or transitive inc powerset E For the definition of transitive since version MuscapeT2 there was some difficulty because the Protoc syntax does not allow the user to write R X Y if R is a variable I then introduced the functional symbol which allows R X Y to be written instead of this forbidden R X Y The definition is then written definition transitive R lt gt WERE Ze Rye YS Se TR A HS an ae ea Protoc does not unify r a b and R X Y consequently I wrote predicates to do it and which return R r X a and Y b This symbol was chosen by analogy with the Protoc operator In effect r a b r a b is true in Protoc if r is a constant r a b and r a b are unified in Muscapet although not in Protos On the other hand Muscaper replaces r a b by r a b as soonas r isa constant in order to produce traces which are easier to read Remark It is possible for the user to really write formulas as in mathematics and to translate for example by a Unix script R X Y into R X Y before starting PRoLoc This notation is also used for mathematical functions and applications f x y may be written and is unified in Muscapert with F X Y forthe instantiations F f X x and Y y The super action addhyp handles these expressions and adds the hypotheses in the more pleasant form r a b or x y insteadof r a b or f x y by the rules addhyp N H E
32. owerset _b etc But for longer terms the ease of reading was lost Moreover it became useful to know the order in which objects have been created to search for object verifying some properties Then the simple numbering has been chosen but the predicate flat still exists as well as the trace of its call so that it is easy to come back to this option In the super action addhyp H such a hypothesis F X P Y is handled as an existential hypothesis but more simply In effect in the super action addhyp H if H is an existential hypothesis 3X p X it is added as it is default action because creating too early the objects X such that p X could be catastrophic This hypothesis will be handled only later see section 10 5 On the other hand the hypotheses Y F X P Y are immediately handled To addhyp H if H is of the form Y F X P Y then if there is no hypothesis F X Z then create a new object Z and add the hypothesis F X Z in all cases add the hypothesis P Z that is in the machine addhyp N H E a 04 20 11 16 H only A X Y gt hyp N A X1 _ gt true create object N z X1 addhyp N A X1 E y replace Y X X1 Y1 addhyp N Y1 8 Building rules After the elimination of functional symbols from definitions and lemmas rules are automatically built from these statements These rules are more operational than the definitions themselves Examples of such built rules are given in sec
33. qual to AX p Y is true is noted Y AX p Y and represented by only X Y p Y Depending on the context this quantifier will then be handled either as a V or as an d or perhaps in a simpler manner or in a somewhat more complicated manner For example we saw the treatment of universal conclusions by the rule V The rule performs almost the same treatment but creates the object only if it does not yet exist Rule ifthe conclusion is of the form Y F X P Y then if there is a hypothesis of the form Z F X then the new conclusion is P Z else create a new object Z add the hypothesis Z F X and the new conclusion is P Z that is in the machine rule N concl_ only concl N only A X B hyp N A X1 gt nee N wy s ae ves names zl z2 etc 1A 7 create object N z X1 addobject N X1 addhyp traces replace B X X1 Bl1 newconcl N Bl I11 1 TL where replace B X X1 B1 replaces x by X1 in B and returns B1 create object N z X1 creates and returns in X1 the first object z1 z2 etc not yet created In old versions of Muscapet the names of created objetcts were built from corresponding terms by flattening them This gave traces easier to read for example owerset a powerset a a inter b inter a b P PoS powerset inter a_b powerset_ inter a_b powerset_a inter powerset_ b inter powerset_a_p
34. rove one or several theorems the statements of which are in one or several files so as the statements of definitions and lemmas 4 Machine representations Everything is expressed in Protos Mathematical statements are Protoc expressions Facts are unit Proto clauses Rules are Protoc clauses expressing declarative knowledge Elementary actions and some strategies are Protoc clauses defining procedural actions And super actions are ProLoG clauses grouping packs of rules for a given goal 04 20 11 6 The inference engine is composed of the Protoc interpreter and of some clauses which process the application of rules applyrulactiv and applyrul 4 1 Expression of mathematical statements The syntax is that of the TPTP library The logical connectives amp and or not gt lt gt are defined as infix operators with precedences in the order as the connectives are written down in mathematics They are right associative The universally quantified formulas are written X Y lt statement function of X Y gt The existentially quantified formulas are written X Y lt statement function of X Y gt The true and false constants may also be used The example theorem introduced in section 2 1 is written A B C subset A B amp subset B C gt subset A C The proof of the theorem T will be requested by the Protoc call prove T The definition of subset is subset A B l
35. s is also done by a recursive ProLoG predicate the metarules of which may lead to splitting 9 Activation and order of rules Activate a rule consists in putting it into the list of active rules which is memorized by means of the predicate rulactiv Rules will be tried in the listed order If this order is important it will have to be stated by metarules The super action activrul begins by creating links acti link that is it adds the facts link 0 P for all concepts P which are in the initial statement of the theorem to be proved for all those that are in the definitions of the preceding ones and recursively The symbols that are concepts are those that have a definition They were memorized when rules were built Then the rules are activated acti_ in a order that depends on their type given or built Among the rules that were built from definitions only those corresponding to links that were stated before are activated Untill version 2 5 the list of rules was analyzed and reordered if necessary in such a way that if a rule R is more general than another rule R then R will be tried before R The cases only considered concern the rules R and R such that R may create an object such that P R may create a object such that P and P is more general than P then R had to be before R In spite of this restriction this re ordering was long and as the number of rules of the studied problems increased time w
36. s now called Muscapet1 was described and analyzed in Pastre 89 89a 93 95 Muscapetl came after an initial program Datrte written in Fortran Pastre 76 78 which was already based on natural deduction in the sense of Bledsoe 71 77 and used methods which resemble those used by humans 4 This was a rule in the first versions of Muscaper It has been replaced by a more general rule because belonging to a set could no longer be known by the system this was a constraint of the TPTP Library see section 3 2 04 20 11 4 The inference engine of Muscapetl was written in PascaL and knowledge rules metarules and super actions was written in a language that was considered simple and declarative Muscapetl produced good results it was evaluated for several years but its use was limited In particular the language was not adapted to the expression of procedural strategies Writing such strategies was complex and it was difficult to read and understand them 3 2 Muscapet2 The following version called Muscapet2 versions 2 0 to 2 7 Pastre 01a 01b 02 06 07 has been completely written in Protoc The reason for this is that it is possible to use the same language to express declarative knowledge such as rules definitions hypotheses etc more procedural knowledge such as proof strategies and the inference engine itself The inference engine contains only few predicates since it is completed by the Protoc interpreter This l
37. sion is H C then add the hypothesis H and the new conclusion is C Their machine expressions are given in section 4 3 10 2 Processing of conjunctive conclusions The rule Rule concl_a if the conclusion is conjunctive then successively prove all the elements of the conjunction is expressed by rule N concl_and concl N A amp B E proconj N A amp B E Eend with proconj N C Econj Eend C A amp B gt true C A B true for the last one atom concat N N0 gensym NO N1 N1l N lthen2then createsubth N N1 A Ecreationsubth creation subth new step applyrulactiv Nl proof of the sub theorem concl N1 true Edemsubth newconcl N B Eretourth remove A which has just been proved B true gt Ereturnth Eend proconj N B Ereturnth Eend Vs The conclusion is set to true if proconj succeeds that is if all the elements of the conjunction were proved proconj recursively proves all the conclusions of the conjunctive conclusion A amp B by creating as many sub theorems as there are conclusions to be proved The numbers of the sub theorems are built from the number N by adding an hyphen then successive numbers 0 1 1 0 1 2 0 1 3 are the sub theorems of the sub theorem numbered 0 1 The new sub theorem of number N1 inherits properties of the theorem of number N super action createsubth e
38. step number The successful and effective application of a rule is memorized To allow to go back and also to be able to write a detailed justification and not only the sequence of steps the system also memorizes the name of the rule the new step the instantiated conditions the list of the steps of the conditions the instantiated and explicit actions and a text giving a justification This text is either given for general rules generally a logical explication or automatically built in the rule for example rule built from the definition of such concept or such axiom with their name or local rule built from such universal hypothesis This memorization is done either in the rule or in the super action in particular in the case of a recursive super action such as adding a hypothesis or proving a conjunctive conclusion 3 4 MuscaDET4 In version 4 in addition to other small improvements the most important changes concern the writing of the useful trace version 4 0 submitted to the CASC competition and the user interface version 4 1 The interface is more easily used and more complete either under Linux or under Protoc Options allow to directly modify the time limit the display level entire trace useful trace result according to the SZS ontology and the language In particular slides of Pastre 10 contain extracts of useful traces The version th is set up again and may be used under Linux or under Protoc The system can p
39. sts X lt statement function of x gt and the connectives were written and or not 7 which disappeared in Muscaper3 but was restored in Muscaper4 1 04 20 11 7 but the symbol used for set belonging must be explicitly indicated by the predicate that is elt In order to reduce writing mathematicians also currently use relativized quantifiers VXEA VYEB p X Y and AXe A AYeB p x Y which are abbreviations for VX VY XEA A YEB p X Y and AXAY XEAA Ye B p X Y In Muscapet2 it was possible to write for all X elt A for all Y elt B p X Y and exists X elt E exists Y elt B p X Y elt having been defined infix This possibility will be restored in the next version of Muscadet in the form X elt A Y elt B p X Y and X elt A Y elt B p X Y or more generally with any formula instead of X elt A Remark the statements of theorems must be closed the statements of definitions may contain variables which are implicitly universal 4 2 Expression of facts The fact that the statement C is the conclusion of the sub theorem to be proved with number N is represented by the unit Protog clause concl N C 1 where I est the number of the step where this fact was created Some other properties are handled in the same manner such as to be a hypothesis hyp N H I an object obj N O a sub theorem subth N N1 etc For active rules exceptionally the whole list of rules that
40. t gt X elt X A gt elt X B This definition is given by definition subset A B lt gt X elt X A gt elt X B where definition is a Protoc predicate stating that the argument statement is a mathematical definition The definitions of intersection and of power set are X elt X inter A B lt gt elt X A amp elt X B X elt X power set A lt gt subset X A It is possible as mathematicians do to use infix operators elt subset inter by defining them with their precedences by the Protos directives op 200 xfy elt op 200 xfy subset op 150 xfy inter then statements may be written TA B C A subset B amp B subset C gt A subset C A subset B lt gt X X elt A gt X elt B gt X X elt A inter B lt gt X elt A amp X elt B X X elt power set A lt gt X subset A but Proog will display A subset B amp B subset C gt A subset C we loose more than we gain in the readability of display Mathematicians usually write set definitions in the form X X p X for example ANB X XE A A XE B or MA X XCA This possibility also exists in Muscapet in the form A inter B X X elt A amp X elt B power set A X X subset A 6 In Muscaper2 and in the corresponding publications they were written for all X lt statement function of x gt and exi
41. the same as above One may also work with the power set of a set VE transitive c PEJ with transitive R E VAVBYVC AEE a BEE A CEE gt R 4 B A R B C R 4 C and XeEAE SVX XEESXCE Relativized quantifiers may be used in order to reduce writing transitive R E VAe E VBE E VCE E R A B R B C R 4 0 Xe DE amp VXEE XCE 2 2 Power set of the intersection of two sets Prove the following theorem VA VB P ANB se P A N P B with the definition of the intersection XEANB S amp S XEAAXEB or ANB X XEAAXEB of the power set of a set XERE SVX XEES XCE or PA X XCA and of the equality of sets A se B amp ACB A BCA After the creation of objects a and b as in the preceding example by a rather complex mechanism which will be described in section 7 Muscapet eliminates functional symbols and P To do this 2 Predicate variables are not possible in Prooc we will see in section 11 how to express R A B 3 YXEA P X is short for VX Xe A P X IXE A P X for IX XEA P X 04 20 11 3 66 99 it creates by means of the operator the objects aNb c Aa pa P b pb and panpb pd The new conclusion is then pe set pd After replacement of the equality of the conclusion by its definition that is pccpd pdcpc the rule Rule concl_A if the conclusion is a conjunction then successively prove all elements of the conjunction creates two sub theorems with numbers and 2 The conclus
42. tion 2 The names of the rules are built from the names of the concepts that are defined or from the names of the lemmas The super action buildrules analyses the statements and calls the recursive Proroc predicate buildrules E N Concept Name Body Antecedents which is a super action composed of metarules that perform the building of one or several rules in a procedural manner Concept is the concept that is defined in a definition or the symbol 1emma in the case of a lemma Name is the name of the rule that is currently being built It is built from Concept and has a number if several rules are built from the same Concept E is the statement that is handled At the beginning it is a piece of statement that is built by buildrules for each definition or lemma Body is the body of the rule which is empty at the beginning and is filled little by little N may a number In this case this means that the rule is not built from a definition but that the rule is built from a universal hypothesis of the sub theorem of number N and will be local only for this sub theorem Antecedents is first empty It then memorizes the antecedents little by little This parameter was introduced to allow the extraction of the useful trace buildrules E N Concept Name Body Antecedents analyses the expression E and depending on its form may extract sub formulas for a recursive call split it into several expressions add conditions then actions Adding condition
43. xcept for the conclusion which is only the sub formula A that is to be proved It is also pointed out that N has N1 as a sub theorem If the sub theorem N1 is proved conclusion true this information is sent to sub theorem N and A is removed from the initial conclusion of N 04 20 11 18 At the end the conclusion of sub theorem N is equal to true if and only if all its sub theorems have been proved 10 3 Processing of universal hypotheses There are no universal hypotheses since the super action addhyp instead of adding them considers them as lemmas and creates new rules which are local for the current sub theorem 10 4 Processing of existential conclusions The general and rather sophisticated treatment of Muscapetl has not yet been written in Muscapet2 nor in the following versions For the moment Muscapet only verifies that objects which satisfy the searched property actually exist 10 5 Processing of existential hypotheses An existential hypothesis may lead to the creation if one does not already exists of an object that satisfies the indicated property But this object must not be created each time an existential hypothesis is added because this could lead to generate infinitely many objects in only one direction and to not taking into account other directions Examples of such situations are analyzed in Pastre 89 93 For this reason these existential hypotheses are first added without treatment Later a rul
Download Pdf Manuals
Related Search