E 1.0x User Manual
Contents
1. 11The name is an historical accident and has no significance anymore 21 There are also two fully predefined learning clause selection heuristics Se lect them with xUseTSM1 for some influence of the learned knowledge or xUseTSM2 for a lot of influence of the learned knowledge 4 6 Other Options 5 Input Language 5 1 LOP E natively uses E LOP a dialect of the LOP language designed for SETHEO At the moment your best bet is to retrieve the LOP description from the E web site Sch99 and or check out the examples available from it LOP is very close to Prolog and E can usually read many fully declarative Prolog files if they do not use arithmetic or rely on predefined symbols Plain SETHEO files usually also work very well There are a couple of minor differences however e equal is an interpreted symbol for E It normally does not carry any meaning for SETHEO unless equality axioms are added e SETHEO allows the same identifier to be used as a constant a non constant function symbol and a predicate symbol E encodes all of these as ordinary function symbols and hence will complain if a symbol is used inconsistently e E allows the use of both and gt as infix symbols for equality a b is equivalent to equal a b for E e E does not support constraints or SETHEO build in symbols This should not usually affect pure theorem proving tasks e Enormally treats procedural clauses exactly as it treats declara2. 8 If the distribution and or use of the Program is restricted in certain countries either by patents or by copyrighted interfaces the original copyright holder who places the Program under this License may add an explicit geographical distribution limitation excluding those countries so that distribution is permitted only in or among countries not thus excluded In such case this License incorporates the limitation as if written in the body of this License 9 The Free Software Foundation may publish revised and or new versions of the General Public License from time to time Such new versions will be similar in spirit to the present version but may differ in detail to address new problems or concerns 31 Each version is given a distinguishing version number If the Program specifies a version number of this License which applies to it and any later version you have the option of following the terms and conditions either of that version or of any later version published by the Free Software Foundation If the Program does not specify a version number of this License you may choose any version ever published by the Free Software Foundation 10 If you wish to incorporate parts of the Program into other free programs whose distribution conditions are different write to the author to ask for permission For software which is copyrighted by the Free Software Foundation write to the Free Software Foundation we sometimes make exceptions
3. lt heu element gt lt heu element gt lt ident gt lt heuristic def gt lt ident gt lt heuristic gt lt heuristic gt As above a single identifier is only a valid heuristic if it has been de fined in lt heuristic def gt previously A lt heuristic def gt which degener ates to a simple heuristic defines a heuristic with name Default which the prover will automatically choose if no other heuristic is selected with the x expert heuristic Example To continue the above example eprover D ex1 Clauseweight ConstPrio 2 1 1 ex2 FIFOWeight PreferGoals H new 3 ex1 1 ex2 x new LUSK3 lop will run the prover on a problem file named LUSK3 lop with a heuristic that chooses 3 out of every 4 clauses according to a simple symbol count ing heuristic and the last clause first among goals and then among other clauses selecting by order of creation in each of these two classes 4 2 Term Orderings E currently supports two families of orderings The Knuth Bendiz Ordering KBO which is used by default and the Lexicographical Path Ordering LPO The KBO is weight based and uses a precedence on function symbols to break ties Consequently to specify a concrete KBO we need a weight function that assigns a weight to all function symbols and a precedence on those symbols The LPO is based on a lexicographic comparison of symbols and subterms and is fully specified by giving just a precedence C
4. means either the Program or any derivative work under copyright law that is to say a work containing the Program or a portion of it either verbatim or with modifications and or translated into another language Hereinafter translation is included without limitation in the term modification Each licensee is addressed as you Activities other than copying distribution and modification are not covered by this License they are outside its scope The act of running the Program is not restricted and the output from the Program is covered only if its contents constitute a work based on the Program independent of having been made by running the Program Whether that is true depends on what the Program does 1 You may copy and distribute verbatim copies of the Program s source code as you receive it in any medium provided that you conspicuously and appropriately publish on each copy an appropriate copyright notice and disclaimer of warranty keep intact all the notices that refer to this License and to the absence of any warranty and give any other recipients of the Program a copy of this License along with the Program You may charge a fee for the physical act of transferring a copy and you may at your option offer warranty protection in exchange for a fee 2 You may modify your copy or copies of the Program or any portion of it thus forming a work based on the Program and copy and 28 distribute such modifications or wor
5. symmetry and transitivity and a set of substitutivity axioms one for each argument position of every function symbol and pred icate symbol A Asa but print a single substitutivity axiom covering all positions for each symbol The short form S is equivalent to print saturated eigEIG If the op tion print sat info is set then each of the clauses is followed by a comment of the form info id pd pl sc cd nl no nv The following table explains the meaning of these values id Clause ident probably only useful internally pd Depth of the derivation graph for this clause pl Number of nodes in the derivation grap sc Symbol count function symbols and variables cd Depth of the deepest term in the clause nl Number of literals in the clause no Number of variable occurences nv Number of different variables H 26 A License The standard distribution of E is free software You can use modify and copy it under the terms of the GNU General Public License You may also have bought a commercial version of E from Safelogic A B in Gothenburg Sweden In this case you are bound by whatever license you agreed to If you are in doubt about which version of E you have run eprover V or eprover h GNU GENERAL PUBLIC LICENSE Version 2 June 1991 Copyright C 1989 1991 Free Software Foundation Inc 59 Temple Place Suite 330 Boston MA 02111 1307 USA Everyone is permitted to copy and distribute verbatim copies of this
6. too receive or can get the source code And you must show them these terms so they know their rights We protect your rights with two steps 1 copyright the software and 2 offer you this license which gives you legal permission to copy distribute and or modify the software 27 Also for each author s protection and ours we want to make certain that everyone understands that there is no warranty for this free software If the software is modified by someone else and passed on we want its recipients to know that what they have is not the original so that any problems introduced by others will not reflect on the original authors reputations Finally any free program is threatened constantly by software patents We wish to avoid the danger that redistributors of a free program will individually obtain patent licenses in effect making the program proprietary To prevent this we have made it clear that any patent must be licensed for everyone s free use or not licensed at all The precise terms and conditions for copying distribution and modification follow GNU GENERAL PUBLIC LICENSE TERMS AND CONDITIONS FOR COPYING DISTRIBUTION AND MODIFICATION 0 This License applies to any program or other work which contains a notice placed by the copyright holder saying it may be distributed under the terms of this General Public License The Program below refers to any such program or work and a work based on the Program
7. Your New Programs If you develop a new program and you want it to be of the greatest possible use to the public the best way to achieve this is to make it free software which everyone can redistribute and change under these terms To do so attach the following notices to the program It is safest to attach them to the start of each source file to most effectively 32 convey the exclusion of warranty and each file should have at least the copyright line and a pointer to where the full notice is found lt one line to give the program s name and a brief idea of what it does gt Copyright C 19yy lt name of author gt This program is free software you can redistribute it and or modify it under the terms of the GNU General Public License as published by the Free Software Foundation either version 2 of the License or at your option any later version This program is distributed in the hope that it will be useful but WITHOUT ANY WARRANTY without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE See the GNU General Public License for more details You should have received a copy of the GNU General Public License along with this program if not write to the Free Software Foundation Inc 59 Temple Place Suite 330 Boston MA 02111 1307 USA Also add information on how to contact you by electronic and paper mail If the program is interactive make it output a short notice like this when it
8. for this Our decision will be guided by the two goals of preserving the free status of all derivatives of our free software and of promoting the sharing and reuse of software generally NO WARRANTY 11 BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE THERE IS NO WARRANTY FOR THE PROGRAM TO THE EXTENT PERMITTED BY APPLICABLE LAW EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND OR OTHER PARTIES PROVIDE THE PROGRAM AS IS WITHOUT WARRANTY OF ANY KIND EITHER EXPRESSED OR IMPLIED INCLUDING BUT NOT LIMITED TO THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU SHOULD THE PROGRAM PROVE DEFECTIVE YOU ASSUME THE COST OF ALL NECESSARY SERVICING REPAIR OR CORRECTION 12 IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING WILL ANY COPYRIGHT HOLDER OR ANY OTHER PARTY WHO MAY MODIFY AND OR REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE BE LIABLE TO YOU FOR DAMAGES INCLUDING ANY GENERAL SPECIAL INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THE PROGRAM INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGES END OF TERMS AND CONDITIONS How to Apply These Terms to
9. from the conditions of this License If you cannot distribute so as to satisfy simultaneously your obligations under this License and any other pertinent obligations then as a consequence you may not distribute the Program at all For example if a patent license would not permit royalty free redistribution of the Program by all those who receive copies directly or indirectly through you then the only way you could satisfy both it and this License would be to refrain entirely from distribution of the Program If any portion of this section is held invalid or unenforceable under any particular circumstance the balance of the section is intended to apply and the section as a whole is intended to apply in other circumstances It is not the purpose of this section to induce you to infringe any patents or other property right claims or to contest validity of any such claims this section has the sole purpose of protecting the integrity of the free software distribution system which is implemented by public license practices Many people have made generous contributions to the wide range of software distributed through that system in reliance on consistent application of that system it is up to the author donor to decide if he or she is willing to distribute software through any other system and a licensee cannot impose that choice This section is intended to make thoroughly clear what is believed to be a consequence of the rest of this License
10. literal selection strategy SelectLargestNegLit GRPOO01 1 rm_eq_rstfp lop You will find the file GRP001 1 rm_eq_rstfp lop in the E PROVER direc tory As we aim at replacing the vast number of individual literal selection func tions with a more abstract mechanism we refrain from describing all of the cur rently implemented functions in detail If you need information about the set of implemented functions run eprover W none The individual functions are implemented and somewhat described in E HEURISTICS che_litselection h Except for SelectOptimalLit where the resulting strategy PSelectOptimalLit will allow paramodulation into positive literals only if no ground literal has been selected 19 4 4 The Watchlist Feature Since public release 0 81 E supports a watchlist A watchlist is a user defined set of clauses Whenever the prover encounters a clause that subsumes one or more clauses from the watchlist those clauses are removed from it The satu ration process terminates if the watchlist is empty or of course if a saturated state or the empty clause have been reached There are two uses for a watchlist To guide the proof search using a heuris tic that prefers clauses on the watchlist or to find purely constructive proofs for clauses on the watchlist If you want to guide the proof search place clauses you believe to be im portant lemmata onto the watchlist Also include the empty clause to make sure that the
11. prover will not terminate prematurely You can then use a clause selection heuristic that will give special consideration to clauses on the watch list This is currently supported via the priority functions PreferWatchlist and DeferWatchlist A clause evaluation function using PreferWatchlist will always select clauses which subsume watchlist clauses first Similarly using DeferWatchlist can be used to put the processing of watchlist clauses off There is a predefined clause selection heuristic UseWatchlist select it with xUseWatchlist that will make sure that watchlist clauses are selected rela tively early It is a strong general purpose heuristic and will maintain com pleteness of the prover This should allow easy access to the watchlist feature even if you don t yet feel comfortable with specifying your own heuristics To generate constructive proofs of clauses just place them on the watch list and select output level 4 or greater see section 6 3 Steps effecting the watch list will be marked in the PCL2 output file If you use the eproof script for proof output or run epclextract of your own subproof for watchlist steps will be automatically extracted Note that this forward reasoning is not complete i e the prover may never generate a given watchlist clause even if it would be trivial to prove it via refutation Options controlling the use of the watch list watchlist lt arg gt Select a file containing the watch list clau
12. selection function The inference system SP consists of the following inference rules e Equality Resolution ugvV R if o mgu u v and o u a R v is eligible for resolution ER Superposition into negative literals if o mgu ulp s a s Sah o t o u a o o s t SN is eligible for paramodula o ulp t vV SV R tion o u v is eligible for resolution and u p V Superposition into positive literals if o mgu ulp s o s Stace ian a t o u a o o s t SP is eligible for paramodula o ulp t vV SV R tion o u v is eligible for resolution and u p V e Equality factoring if o mgu s u o s tVuruVR JUD EF sels a t and o s t eligible for o t uVurvV R paramodulation Rewriting of negative literals PYR if lp o s and o s gt ofi sxt up olt gvyR Po l Rewriting of positive literals sxt uxvVR if ulp a s o s gt a t and RP if uv is not eligible for reso sxt ulpoa t euVR lution or u v or p Clause subsumption C a C V R where C and R are arbitrary CS partial clauses and is a C substitution Equality subsumption sxt ulp o s u lp o t VR ES s amp t Positive simplify reflect sxt ulp o s 4ulpo t VR PS s sxt R e Negative simplify reflect Contextual top level simplify reflect o CV RV s t CVvs t where s t is the negation o
13. starts in an interactive mode Gnomovision version 69 Copyright C 19yy name of author Gnomovision comes with ABSOLUTELY NO WARRANTY for details type show w This is free software and you are welcome to redistribute it under certain conditions type show c for details The hypothetical commands show w and show c should show the appropriate parts of the General Public License Of course the commands you use may be called something other than show w and show c they could even be mouse clicks or menu items whatever suits your program You should also get your employer if you work as a programmer or your school if any to sign a copyright disclaimer for the program if necessary Here is a sample alter the names Yoyodyne Inc hereby disclaims all copyright interest in the program Gnomovision which makes passes at compilers written by James Hacker lt signature of Ty Coon gt 1 April 1989 Ty Coon President of Vice This General Public License does not permit incorporating your program into proprietary programs If your program is a subroutine library you may consider it more useful to permit linking proprietary applications with the library If this is what you want to do use the GNU Library General Public License instead of this License 33 References Bac98 BDP89 BG94 CL73 Der91 DKS97 DS94al DS94b DS96 HBF 96 L Bachmair Pe
14. C 9 and o L is gt z maximal in o C or sel C 9 and o L is gt z maximal in o selC N C7 or sel C 0 and o L is gt maximal in o sel C NC e a L is eligible for paramodulation if is positive sel C and o L is strictly gt maximal in o C 3Non equational literals are encoded as equations or disequations P ti tn amp T In this case we treat predicate symbols as special function symbols that can only occur at the top most positions and demand that atoms terms formed with a top predicate symbol cannot be unified with a first order variable from V i e we treat normal terms and predicate terms as two disjoint types lt The calculus is represented in the form of inference rules For convenience we distinguish two types of inference rules For generating inference rules written with a single line separating preconditions and results the result is added to the set of all clauses For contracting inference rules written with a double line the result clauses are substituted for the clauses in the precondition In the following u v s and t are terms o is a substitution and R S and T are partial clauses p is a position in a term and A is the empty or top position Different clauses are assumed to not share any common variables Definition 3 3 The inference system SP Let gt be a total simplification ordering extended to orderings gt z and gt on literals and clauses and let sel be a
15. E 1 0x User Manual preliminary version Stephan Schulz October 22 2008 Abstract E is an equational theorem prover for full clausal logic based on su perposition and rewriting In this very preliminary manual we first give a short introduction for impatient new users and then cover calculus control options and input output of the prover in some more detail Contents Introduction Getting Started Calculus and Proof Procedure ily Aalis sat A hdd stists ds uta hth ty a SS ANa ea a a teh a este oe 3 2 4 Proof Procedure s reee ees ee P a ee ces ee es Usage 4 1 Search Control Heuristics a ATS Priority fonctions 03 g orara a iad Ah eek 4 1 2 Generic Weight Functions 4 1 3 Clause Evaluation Functions AVIA Heuristics sai ace Pa de SODA Eee eb aa 4 2 Term Orderings se ek we EE ae BO D a 4 2 1 Precedence Generation Schemes 4 2 2 Weight Generation Schemes 4 3 Literal Selection Strategies 2 2 a 4 4 The Watchlist Feature 00000 4 5 Learning Clause Evaluation Functions 4 5 1 Creating Knowledge Bases 0 4 5 2 Populating Knowledge Bases 21 4 5 3 Using Learned Knowledge 21 4 6 Other Options 0 0 002 eee eee 22 5 Input Language 22 Bel ORS yout ak amp dele de by Baty Bed te dy Rad dua SRS Beate ot id ded kd 22 5 2 PPTP Format as
16. New Prefer new clauses i e clauses that are processed for the first time PreferGoals Prefer goals all negative clauses PreferNonGoals Prefer non goals i e facts with at least one positive literal PreferUnits Prefer unit clauses clauses with one literal PreferNonUnits Prefer non unit clauses 10 PreferHorn Prefer Horn clauses clauses with no more than one positive liter als PreferNonHorn Prefer non Horn clauses ConstPrio Assign the same priority to all clauses ByLiteralNumber Give a priority according to the number of literals i e al ways prefer a clause with fewer literals to one with more literals ByDerivationDepth Prefer clauses which have a short derivation depth i e give a priority based on the length of the longest path from the clause to an axiom in the derivation tree Counts generating inferences only ByDerivationSize Prefer clauses which have been derived with a small num ber of generating inferences ByNegLitDist Prefer goals to non goals Among goals prefer goals with fewer literals and goals with ground literals more exactly the priority is in creased by 1 for a ground literal and by 3 for a non ground literal Clauses with lower values are selected before clauses with higher values ByGoalDifficulty Prefer goals to non goals Select goals based on a simple estimate of their difficulty First unit ground goals then unit goals then ground goals then other goals SimulateSO
17. S Use the priority system to simulate Set Of Support This prefers all initial clauses and all Set Of Support clauses Some non SOS clauses will be generated but not selected for processing This is neither well tested nor a particularly good fit with E s calculus but can be used as one among many heuristics If you try a pure SOS strategy you also should set restrict literal comparisons and run the prover without literal selection enabled PreferHorn Prefer Horn clauses note includes units PreferNonHorn Prefer non Horn clauses PreferUnitAndNonEq Prefer all unit clauses and all clauses without equational literal This was an attempt to model some restricted calculi used e g in Gandalf Tam97 but did not quite work out DeferNonUnitMaxEq Prefer everything except for non unit clauses with a max imal equational literal Don t paramodulate if its to expensive See above same result ByCreationDate Return the creation date of the clause as priority This im poses a FIFO equivalence class on clauses Clauses generated from the same given clause are grouped together and can be ordered with any evaluation function among each other 11 PreferWatchlist Prefer clauses on the watchlist see 4 4 DeferWatchlist Defer clauses on the watchlist see above Please note that careless use of certain priority functions can make the prover incomplete for the general case 4 1 2 Generic Weight Functions Generic weight
18. TP 3 syntax with the options tstp in tptp3 in tstp format and tptp3 format The last two options will also enable TPTP 3 format for proof output Note that many of E s support tools still require PCL2 format Various tools for processing TPTP 3 proof format are available via the TPTP web site http www tptp org In either TPTP format clauses and formulas with TPTP type conjecture or negated conjecture TPTP 3 only are considered goal clauses for the sos uses input types option 6 Output or how to interpret what you see E has several different output levels controlled by the option 1 or output level Level 0 prints nearly no output except for the result Level 1 is intended to give humans a somewhat readable impression of what is going on inside the infer ence engine Levels 3 to 6 output increasingly more information about the inside processes in PCL2 format At level 4 and above a large superset of the proof inferences is printed You can use the epclextract utility in E PROVER to extract a simple proof object In Level 0 and 1 everything E prints is either a clause that is implied by the original axioms or a comment or very often both 6 1 The Bare Essentials In silent mode output level 0 s or silent E will not print any output during saturation It will print a one line comment documenting the state of the proof search after termination The following possibilities exist e The prover found a proof T
19. able to encode heuristical control knowledge but rather are used to express certain elements of a search strategy or to restrict the effect of heuristic evaluation functions to certain classes of clauses It is quite trivial to add a new priority function to E so at any time there probably exist a few not yet documented here Syntactically a large subset of currently available priority functions is de scribed by the following rule lt prio fun gt PreferGroundGoals PreferUnitGroundGoals PreferGround PreferNonGround PreferProcessed PreferNew PreferGoals PreferNonGoals PreferUnits PreferNonUnits PreferHorn PreferNonHorn ConstPrio ByLiteralNumber ByDerivationDepth ByDerivationSize ByNegLitDist ByGoalDifficulty SimulateSOs PreferHorn PreferNonHorn PreferUnitAndNonEq DeferNonUnitMaxEq ByCreationDate PreferWatchlist DeferWatchlist The priority functions are interpreted as follows PreferGroundGoals Always prefer ground goals all negative clauses without variables do not differentiate between all other clauses PreferUnitGroundGoals Prefer unit ground goals PreferGround Prefer clauses without variables PreferNonGround Prefer clauses with variables PreferProcessed Prefer clauses that have already been processed once and have been eliminated from the set of processed clauses due to interreduc tion forward contraction Prefer
20. about the proof search and final clause sets The data should be fairly self explaining 6 3 Detailed Reporting At output levels greater that 1 E prints certain inferences in PCL2 format At level 2 it only prints generating inferences At level 4 it prints all generating and modifying inferences and at level 6 it also prints PCL steps giving a lot of insight into the internal operation of the inference engine This protocol is fairly readable and from level 4 on can be used to check the proof with the utility checkproof provided with the distribution 6 4 Requesting Specific Results There are two additional kinds of information E can provide beyond the normal output during proof search Statistical information and final clause sets with additional information First E can give you some technical information about the conditions it runs under The option print pid will make E printing its process id as a comment in the format Pid XXX where XXX is an integer number This is useful if you want to send signals to the prover in particular if you want to terminate the prover to control it from the outside The option R resources info will make E print a summary of used system resources after graceful termination User time 0 010 s System time 0 020 s Total time 0 030 s Maximum resident set size 0 pages Most operating systems do not provide a valid value for the resident set size and other memory rel
21. ased Distributed Deduction Processes Journal of Symbolic Com putation 21 4 5 523 541 1996 Th Hillenbrand A Buch and R Fettig On Gaining Efficiency in Completion Based Theorem Proving In H Ganzinger editor Proc of the 7th RTA New Brunswick volume 1103 of LNCS pages 432 435 Springer 1996 34 HJL99 McC94 MIL 97 MW97 NN93 RVO1 RV02 Sch99 Sch00 Sch01 Sch02 Sch04 Th Hillenbrand A Jaeger and B L chner System Abstract Waldmeister Improvements in Performance and Ease of Use In H Ganzinger editor Proc of the 16th CADE Trento volume 1632 of LNAI pages 232 236 Springer 1999 W W McCune Otter 3 0 Reference Manual and Guide Technical Report ANL 94 6 Argonne National Laboratory 1994 M Moser O Ibens R Letz J Steinbach C Goller J Schumann and K Mayr SETHEO and E SETHEO The CADE 13 Systems Journal of Automated Reasoning 18 2 237 246 1997 Special Issue on the CADE 13 ATP System Competition W W McCune and L Wos Otter The CADE 13 Competition Incarnations Journal of Automated Reasoning 18 2 211 220 1997 Special Issue on the CADE 13 ATP System Competition P Nivela and R Nieuwenhuis Saturation of First Order Con strained Clauses with the Saturate System In C Kirchner edi tor Proc of the 5th RTA Montreal volume 690 of LNCS pages 436 440 Springer 1993 A Riazanov and A Voronkov Vampire 1 1 System Descr
22. asine a bo ch ch hg ee he Oe ee 22 6 Output or how to interpret what you see 23 6 1 The Bare Essentials 000000000 ae 23 6 2 Impressing your Friends 0 2000 4 25 6 3 Detailed Reporting 2 2 2 2 0 0 2 0000 25 6 4 Requesting Specific Results 000 25 A License 27 1 Introduction This is a short and currently very sketchy documentation to the E equational theorem prover E is an purely equational theorem prover for first order logic with equality It is based on paramodulation and rewriting This means that E reads a set of formulas and or clauses and saturates it by systematically applying a number of inference rules until either all possible inferences have been performed or until the empty clause has been derived i e the clause set has been found to be unsatisfiable and thus a conjecture has been proved E is still a moving target but most recent releases have been quite stable and the prover is being used productively by several independent groups of people This manual should enable you to experiment with the prover and to use some of its more advanced features The manual assumes a working knowledge of refutational theorem proving which can be gained from e g CL73 For a short description of E including performance data see Sch04 A more detailed description has been published as Sch02 Most papers on E and much more information is available at or a few hops away from
23. ated resources so you should probably not depend on the last value to carry any meaningful information The time information is required by most standards and should be useful for all tested operating systems 14PCL2 is a proof output protocol language currently being designed by me as a successor to PCL DS94a DS94b DS96 25 E can be used not only as a prover but as a normalizer for formulae or as a lemma generator In this cases you will not only want to know if E found a proof but also need some or all of the derived clauses possibly with statistical information for filtering This is supported with the print saturated and print sat info options for E The option print saturated takes as its argument a string of letters each of which represents a part of the total set of clauses E knows about The following table contains the meaning of the individual letters e Processed positive unit clauses Equations i Processed negative unit clauses Inequations g Processed non unit clauses except for the empty clause which if present is printed separately The above three sets are interreduced and all selected inferences between them have been computed E Unprocessed positive unit clauses Unprocessed negative unit clauses G Unprocessed non unit clause this set may contain the empty clause in very rare cases a Print equality axioms if equality is present in the prob lem This letter prints axioms for reflexivity
24. ddition to the user defined op tions You may want to use wconstant for predictable behaviour lpo recursion limit lt arg gt Limits the recursion depth of LPO comparison This is useful in rare cases where very large term comparisons can lead to stack overflow issues It does not change completeness but may lead to unnecessary inferences in rare cases Note By default recursion depth is limited to 1000 To get effectively unlimited recursion depth use this option with an outrageously large argument Don t forget to increase process stack size with limit ulimit from your favourite shell 4 2 1 Precedence Generation Schemes Precedence generation schemes are based on syntactic features of the sym bol and the input clause set like symbol arity or number of occurrences in the formula At least the following options are supported as argument to order precedence generation unary_first Sort symbols by arity with the exception that unary symbols come first Frequency is used as a tie breaker rarer symbols are greater unary freq Sort symbols by frequency rarer symbols are bigger with the exception that unary symbols come first Yes this should better be named unary_invfreq for consistency but is not arity Sort symbols by arity symbols with higher arity are larger invarity Sort symbols by arity symbols with higher arity are smaller const_max Sort symbols by arity symbols with higher arity are larger bu
25. e selected e Normally E is complete However if the option delete bad limit is given or if automatic mode in connection with a memory limit is used E will periodically delete clauses it deems unlikely to be processed to avoid running out of memory In this case completeness cannot be ensured any more This effect manifests itself extremely rarely If it does E will print the following string Failure Out of unprocessed clauses This is roughly equivalent to Otter s SOS empty message e Finally it is possible to chose restricted calculi when starting E This is useful if E is used as a normalization tool or as a preprocessor or lemma generator In this case E will print a corresponding message Clause set closed under restricted calculus 13Unless the prover runs out of memory see below the user selects an unfair strategy in which case the prover may never terminate or some strange and unexpected things happen 24 6 2 Impressing your Friends If you run E without selection an output level or by setting it explicitly to 1 E will print each non tautological non subsumed clause it processes as a comment It will also print a hash for each clause it tries to process but can prove to be superfluous This mode gives some indication of progress and as the output is fairly restricted does not slow the prover down too much For any output level greater than 0 E will also print statistical information
26. ent symbols If this option is used in connection with order precedence generation the par tial ordering will be completed using the selected method otherwise the prover runs with a non ground total ordering The option without the optional argument is equivalent to precedence the empty precedence There is a drawback to using precedence Normally total precedences are rep resented by mapping symbols to a totally ordered set small integers which can be compared using standard machine in structions The used data structure is linear in the number n of function symbols However if precedence is used the prover allocates and completes a n x n lookup table to effi ciently represent an arbitrary partial ordering If n is very big this matrix takes up significant space and takes a long time to compute in the first place This is unlikely to be a problem unless there are at least hundreds of symbols 15 order weights lt arg gt Give explicit weights to function symbols The argument syn tax is a comma separated list of items of the form f w where f is a symbol from the specification and w is a non negative integer Note that at best very simple checks are performed so you can specify weights that do not obey the KBO weight constraints Behaviour in this case is undefined If all your weights are positive this is unlikely to happen Since KBO needs a total weight function E always uses a weight generation scheme in a
27. et of all finite SP derivations lt As SP only removes clauses that are composite with respect to the remaining set of clauses the calculus is complete For the case of unit clauses it degener ates into unfailing completion BDP89 as implemented in DISCOUNT E can also simulate the positive unit strategy for Horn clauses described in Der91 using appropriate selection functions Contrary to e g SPASS E does not implement special rules for non equa tional literals or sort theories as we expect this part to be taken care of by SETHEO in a later combined system Instead non equation literals are encoded as equations and dealt with accordingly 3 2 Proof Procedure Fig 1 shows a slightly simplified pseudocode sketch of the quite straightfor ward proof procedure of E The set of all clauses is split into two sets a set 6This rule can only be implemented approximately as the problem of recognizing tautolo gies is only semi decidable in equational logic Current versions of E try to detect tautologies by checking if the ground completed negative literals imply at least one of the positive literals as suggested in NN93 Note that the proof procedure has been further simplified for version 0 8 and up The pseudo code describes the current version Input Axioms in U P is empty while U begin c select U U U c Apply RN RP NS PS CSR DR DD DE simplify c P Apply CS ES TD i
28. f CSR i i ao a C V R CVs t s t and is a substitution 4A stronger version of RP is proven to maintain completeness for Unit and Horn prob lems and is generally believed to maintain completeness for the general case as well Bac98 However the proof of completeness for the general case seems to be rather involved as it re quires a very different clause ordering than the one introduced BG94 and we are not aware of any existing proof in the literature The variant rule allows rewriting of maximal terms of maximal literals under certain circumstances if ulp o s o s gt o t and if RP sxt urvVR uv is not eligible for resolution or set ulpco t 2uVR u vor p Aor c is not a variable renaming This stronger rule is implemented successfully by both E and SPASS Wei99 5In practice this rule is only applied if o s and o t are gt incomparable in all other cases this rule is subsumed by RN and the deletion of resolved literals DR Tautology deletion ace 6 TD if C is a tautology Deletion of duplicate literals sxetVsetVR sxtV R DD Deletion of resolved literals DR s gsVR Destructive equality resolution VR DE REONE if x y V o mgu zx y a R We write SP N to denote the set of all clauses that can be generated with one generating inference from I on a set of clauses N Dgp to denote the set of all SP derivations and Dyp to denote the s
29. f LNAI pages 67 81 4130 2006 Springer G Sutcliffe The TPTP Web Site http www tptp org 2004 2005 T Tammet Gandalf Journal of Automated Reasoning 18 2 199 204 1997 Special Issue on the CADE 13 ATP System Competition C Weidenbach B Afshordel U Brahm C Cohrs T Engel G Jung E Keen C Theobalt and D Topic System Abstract SPASS Version 1 0 0 In H Ganzinger editor Proc of the 16th CADE Trento volume 1632 of LNAI pages 378 382 Springer 1999 C Weidenbach Personal communication at CADE 16 Trento Un published 1999 C Weidenbach SPASS Combining Superposition Sorts and Split ting In A Robinson and A Voronkov editors Handbook of Auto mated Reasoning volume II chapter 27 pages 1965 2013 Elsevier Science and MIT Press 2001 C Weidenbach B Gaede and G Rock SPASS amp FLOTTER Ver sion 0 42 In M A McRobbie and J K Slaney editors Proc of the 13th CADE New Brunswick volume 1104 of LNAI pages 141 145 Springer 1996 36
30. f c is trivial or subsumed by P then delete c else if c is the empty clause then Success Proof found stop else T Temporary clause set foreach p P do if c simplifies p P P p T TUp T U e resolvents c ER T U e factors c EF T U paramodulants c P SN SP foreach p T do end fi end Failure Apply efficiently implemented subset of RN RP NS PS CSR DR DD DE p cheap simplify p P Apply TD or efficient approximation of it if p is trivial delete p else U U U cheap simplify p P fi Initial U is satisfiable P describes model Figure 1 Main proof procedure of E P of processed clauses and a set U of unprocessed clauses Initially all input clauses are in in U and P is empty The algorithm selects a new clause from U simplifies it w r t to P then uses it to back simplify the clauses in P in turn It then performs equality factoring equality resolution and superposition between the selected clause and the set of processed clauses The generated clauses are added to the set of unprocessed clauses The process stops when the empty clause is derived or no further inferences are possible The proof search is controlled by three major parameters The term ordering described in section 4 2 the literal selection function and the order in which the select operation selects the next clause to process E implements two different classes of term orderi
31. f the term ordering into account In particular the weight of a term that is maximal in its literal is multiplied by term_pen and the weight of maximal literals is multiplied by lit_pen Orientweight prio fweight vweight term_pen lit_pen pos_mult This weight function is a slight variation of Refinedweight In this case the weight of both terms of an unorientable literal is multiplied by a penalty term_pen Simweight prio equal_weight vv_clash vt_clash tt_clash This weight function is intended to return a low weight for literals in which the two terms are very similar It does not currently work very well even for unit clauses RTFS in lt che_simweight c gt to find out more 8Note that there now are many additional generic weight functions not yet documented 12 FIFOWeight prio This weight function assigns weights that increase in a strictly monotonic manner i e it realizes a first in first out strategy if used all by itself This is the most obviously fair strategy LIFOWeight prio This weight function assigns weights that decrease in a strictly monotonic manner i e it realizes a last in first out strategy if used all by itself which of course would be unfair and result in an extremely incomplete prover 4 1 3 Clause Evaluation Functions A clause evaluation function is constructed by instantiating a generic weight function It can either be specified directly or specified and given a name for
32. functions are templates for functions taking a clause and return ing a weight i e an estimate of the usefulness for it where a lower weight means that the corresponding clause should be processed before a clause with a higher weight A generic weight function is combined with a priority function and instantiated with a set of parameters to yield a clause evaluation function You can specify an instantiated generic weight function as described in this rule lt weight fun gt Clauseweight lt prio fun gt lt int gt lt int gt lt float gt Refinedweight lt prio fun gt lt int gt lt int gt lt float gt lt float gt lt float gt Orientweight lt prio fum gt lt int gt lt int gt lt float gt lt float gt lt float gt Simweight lt prio fun gt lt float gt lt float gt lt float gt lt float gt FIFOWeight lt prio fun gt LIFOWeight lt prio fun gt Clauseweight prio fweight vweight pos_mult This is the basic sym bol counting heuristic Variables are counted with weight vweight function symbols with weight fweight The weight of positive literals is multiplied by pos_mult before being added into the final weight Refinedweight prio fweight vweight term_pen lit_pen pos_mult This weight function is very similar to the first one It differs only in that it takes the effect o
33. his is denoted by the output string Proof found e The problem does not have a proof i e the specification is satisfiable and E can detect this No proof found Ensuring the completeness of a prover is much harder than ensuring cor rectness Moreover proofs can easily be checked by analyzing the output 23 of the prover while such a check for the absence of proofs is rarely possible I do believe that the current version of E is both correct and complete but my belief in the former is stronger than my belief in the later e A hard resource limit was hit For memory this can be either due to a per process limit set with limit or the prover option memory limit or due to running out of virtual memory For CPU time this case is triggered if the per process CPU time limit is reached and signaled to the prover via a SIGXCPU signal This limit can be set with limit or more reliable with the option cpu limit The output string is one of the following two depending on the exact reason for termination Failure Resource limit exceeded memory Failure Resource limit exceeded time e A user defined limit was reached during saturation and the saturation pro cess was stopped gracefully Limits include number of processed clauses number of total clauses and cpu time as set with soft cpu limit The output string is Faiure User resource limit exceeded and the user is expected to know which limit h
34. iption In R Gor A Leitsch and T Nipkow editors Proc of the 1st IJCAR Siena volume 2083 of LNAI pages 376 380 Springer 2001 A Riazanov and A Voronkov The Design and Implementation of VAMPIRE Journal of AI Communications 15 2 3 91 110 2002 S Schulz The E Web Site http www4 informatik tu muenchen de sim schulz WORK eprover h tml 1999 S Schulz Learning Search Control Knowledge for Equational De duction Number 230 in DISKI Akademische Verlagsgesellschaft Aka GmbH Berlin 2000 Ph D Thesis Fakult t fiir Informatik Technische Universitat M nchen S Schulz Learning Search Control Knowledge for Equational The orem Proving In F Baader G Brewka and T Eiter editors Proc of the Joint German Austrian Conference on Artificial Intelligence KI 2001 volume 2174 of LNAI pages 320 334 Springer 2001 S Schulz E A Brainiac Theorem Prover Journal of AI Commu nications 15 2 3 111 126 2002 S Schulz System Description E 0 81 In D Basin and M Rusinow itch editors Proc of the 2nd IJCAR Cork Ireland volume 3097 of LNAI pages 223 228 Springer 2004 35 SSCG06 Sut05 Tam97 WAB 99 Wei99 Wei01 WGR96 Geoff Sutcliffe Stephan Schulz Koen Claessen and Allen Van Gelder Using the TPTP Language for Writing Derivations and Finite Interpretations In Ulrich Fuhrbach and Natarajan Shankar editors Proc of the 3rd IJCAR Seattle volume 4130 o
35. is a work based on the Program the distribution of the whole must be on the terms of this License whose permissions for other licensees extend to the entire whole and thus to each and every part regardless of who wrote it Thus it is not the intent of this section to claim rights or contest your rights to work written entirely by you rather the intent is to exercise the right to control the distribution of derivative or collective works based on the Program In addition mere aggregation of another work not based on the Program with the Program or with a work based on the Program on a volume of a storage or distribution medium does not bring the other work under the scope of this License 3 You may copy and distribute the Program or a work based on it under Section 2 in object code or executable form under the terms of Sections 1 and 2 above provided that you also do one of the following a Accompany it with the complete corresponding machine readable source code which must be distributed under the terms of Sections 1 and 2 above on a medium customarily used for software interchange or 29 b Accompany it with a written offer valid for at least three years to give any third party for a charge no more than your cost of physically performing source distribution a complete machine readable copy of the corresponding source code to be distributed under the terms of Sections 1 and 2 above on a medium customarily used for s
36. k under the terms of Section 1 above provided that you also meet all of these conditions a You must cause the modified files to carry prominent notices stating that you changed the files and the date of any change b You must cause any work that you distribute or publish that in whole or in part contains or is derived from the Program or any part thereof to be licensed as a whole at no charge to all third parties under the terms of this License c If the modified program normally reads commands interactively when run you must cause it when started running for such interactive use in the most ordinary way to print or display an announcement including an appropriate copyright notice and a notice that there is no warranty or else saying that you provide a warranty and that users may redistribute the program under these conditions and telling the user how to view a copy of this License Exception if the Program itself is interactive but does not normally print such an announcement your work based on the Program is not required to print an announcement These requirements apply to the modified work as a whole If identifiable sections of that work are not derived from the Program and can be reasonably considered independent and separate works in themselves then this License and its terms do not apply to those sections when you distribute them as separate works But when you distribute the same sections as part of a whole which
37. later reference at once lt eval fun gt lt ident gt lt weight fun gt lt eval fun def gt lt eval fun def gt lt ident gt lt weight fun gt lt eval fun def list gt lt eval fun def gt Of course a single identifier is only a valid evaluation function if it has been previously defined in a lt eval fun def gt It is possible to define the value of an identifier more than once in which case later definitions take precedence to former ones Clause evaluation functions can be be defined on the command line with the D define weight function option followed by a lt eval fun def list gt Example eprover D ex1 Clauseweight ConstPrio 2 1 1 ex2 FIFOWeight PreferGoals sets up the prover to know about two evaluation function ex1 and ex2 which supposedly will be used later on the command line to define one or more heuristics The double quotes are necessary because the brackets and the commas are special characters for most shells There are a variety of clause evaluation functions predefined in the variable DefaultWeightFunctions which can be found in che_proofcontrol c See also sections 4 4 and 4 5 which cover some of the more complex weight functions of E 13 4 1 4 Heuristics A heuristic defines how many selections are to be made according to one of several clause evaluation functions Syntactically lt heu element gt lt int gt lt eval fun gt lt heuristic gt
38. license document but changing it is not allowed Preamble The licenses for most software are designed to take away your freedom to share and change it By contrast the GNU General Public License is intended to guarantee your freedom to share and change free software to make sure the software is free for all its users This General Public License applies to most of the Free Software Foundation s software and to any other program whose authors commit to using it Some other Free Software Foundation software is covered by the GNU Library General Public License instead You can apply it to your programs too When we speak of free software we are referring to freedom not price Our General Public Licenses are designed to make sure that you have the freedom to distribute copies of free software and charge for this service if you wish that you receive source code or can get it if you want it that you can change the software or use pieces of it in new free programs and that you know you can do these things To protect your rights we need to make restrictions that forbid anyone to deny you these rights or to ask you to surrender the rights These restrictions translate to certain responsibilities for you if you distribute copies of the software or if you modify it For example if you distribute copies of such a program whether gratis or for a fee you must give the recipients all the rights that you have You must make sure that they
39. mbol is the rank of it s equiva lence class with less frequent symbols getting lower weights invfreqrank Sort all function symbols by frequency of occurrence which in duces a total quasi ordering The weight of a symbol is the rank of its equivalence class with less frequent symbols getting higher weights freqranksquare As freqrank but weight is the square of the rank invfreqranksquare As invfreqrank but weight is the square of the rank invmodfreqrank Sort all function symbols by frequency of occurrence which induces a total quasi ordering The weight of an equivalence class is the sum of the cardinality of all smaller classes 1 The weight of a symbol is the weight of its equivalence classes Less frequent symbols get higher weights invmodfreqrankmax0 As invmodfreqrank except that the first maximal sym bol is given weight 0 constant Give the same arbitrary positive weight to all function symbols 4 3 Literal Selection Strategies The superposition calculus allows the selection of arbitrary negative literals in a clause and only requires generating inferences to be performed on these literals E supports this feature and implements it via manipulations of the literal ordering Additionally E implements strategies that allow inferences into maximal positive literals and selected negative literals A selection strategy is selected with the option literal selection strategy Currently at least the following stra
40. ment of the latest version of the prover for quite some time To find out more about the options available type eprover help or consult the source code included with the distribution 3 Calculus and Proof Procedure E is a purely equational theorem prover based on ordered paramodulation and rewriting As such it implements an instance of the superposition calculus de scribed in BG94 We have extended the calculus with some stronger contrac tion rules and more general approach to literal selection The proof procedure is a variant of the given clause algorithm 3 1 Calculus Term F V denotes the set of first order terms over a finite set of function symbols F with associated arities and an enumerable set of variables V We write t to denote the subterm of t at a position p and write t p t to denote t with t replaced by t An equation s t is an implicitly symmetrical pair of terms A positive literal is an equation s t a negative literal is a Emphasis added for E 0 7 and up which globally cache rewrite steps Yes this is outdated If it still applies to you get a new computer It will still work ok though negated equation s t We write s lt t to denote an arbitrary literal Literals can be represented as multi sets of multi sets of terms with s t represented as s t and st represented as s t A ground reduction ordering gt is a Noetherian partial ordering that is stable w r t the term str
41. ngs lexicographic term or derings and Knuth Bendix orderings A given ordering is determined by instan tiating one of the classes with a variety of parameters described in section 4 2 Literal selection currently is done according to one of more than 50 prede fined functions Section 4 3 describes this feature Clause selection is determined by a heuristic evaluation function which con ceptually sets up a set of priority queues and a weighted round robin scheme that determines from which queue the next clause is to be picked The order within each queue is determined by a priority function which partitions the set of unprocessed clauses into one or more subsets and a heuristic evaluation function which assigns a numerical rating to each clause Section 4 1 describes the user interface to this mechanism 4 Usage 4 1 Search Control Heuristics Search control heuristics define the order in which the prover considers newly generated clauses A heuristic is defined by a set of clause evaluation functions and a selection scheme which defines how many clauses are selected according to each evaluation function A clause evaluation function consists of a priority function and an instance of a generic weight function 4 1 1 Priority functions Priority functions define a partition on the set of clauses A single clause evalua tion consists of a priority which is the first selection criteria and an evaluation Priorities are usually not suit
42. oftware interchange or c Accompany it with the information you received as to the offer to distribute corresponding source code This alternative is allowed only for noncommercial distribution and only if you received the program in object code or executable form with such an offer in accord with Subsection b above The source code for a work means the preferred form of the work for making modifications to it For an executable work complete source code means all the source code for all modules it contains plus any associated interface definition files plus the scripts used to control compilation and installation of the executable However as a special exception the source code distributed need not include anything that is normally distributed in either source or binary form with the major components compiler kernel and so on of the operating system on which the executable runs unless that component itself accompanies the executable If distribution of executable or object code is made by offering access to copy from a designated place then offering equivalent access to copy the source code from the same place counts as distribution of the source code even though third parties are not compelled to copy the source along with the object code 4 You may not copy modify sublicense or distribute the Program except as expressly provided under this License Any attempt otherwise to copy modify sublicense or distribute the Prog
43. opulating Knowledge Bases The knowledge base contains information gained from clausal PCL2 protocols of E In a first step information from the protocol is abstracted into a more compact form A number of clauses is selected as training examples and anno tations about there role are computed The result is a list of annotated clauses and a list of the axioms initial clauses of the problem This step can be performed using the program direct_examples In a second step the collected information is integrated into the knowledge base For this purpose the program ekb_insert can be used However it is probably more convenient to use the single program ekb_ginsert which directly extracts all pertinent information from a PCL2 protocol and inserts it into a designated knowledge base The program ekb_delete will delete an example from a knowledge base This process is not particularly efficient as the whole knowledge base is first parsed 4 5 3 Using Learned Knowledge The knowledge in a knowledge base can be utilized by the two clause evalu ation functions TSMWeight and TSMRWeight Both compute a modifica tion weight based on the learned knowledge and apply it to a conventional symbol counting base weight similar to Clauseweight for TSMWeight and Refinedweight for TSMWeight An example command line is eprover x 1 TSMWeight ConstPrio 1 1 2 flat E KNOWLEDGE 100000 1 0 1 0 Flat IndexIdentity 100000 20 20 2 1 0 2
44. ram is void and will automatically terminate your rights under this License However parties who have received copies or rights from you under this License will not have their licenses terminated so long as such parties remain in full compliance 5 You are not required to accept this License since you have not Signed it However nothing else grants you permission to modify or distribute the Program or its derivative works These actions are prohibited by law if you do not accept this License Therefore by modifying or distributing the Program or any work based on the Program you indicate your acceptance of this License to do so and all its terms and conditions for copying distributing or modifying the Program or works based on it 6 Each time you redistribute the Program or any work based on the Program the recipient automatically receives a license from the original licensor to copy distribute or modify the Program subject to 30 these terms and conditions You may not impose any further restrictions on the recipients exercise of the rights granted herein You are not responsible for enforcing compliance by third parties to this License 7 If as a consequence of a court judgment or allegation of patent infringement or for any other reason not limited to patent issues conditions are imposed on you whether by court order agreement or otherwise that contradict the conditions of this License they do not excuse you
45. rsonal communication at CADE 15 Lindau Un published 1998 L Bachmair N Dershowitz and D A Plaisted Completion With out Failure In H Ait Kaci and M Nivat editors Resolution of Equations in Algebraic Structures volume 2 pages 1 30 Academic Press 1989 L Bachmair and H Ganzinger Rewrite Based Equational Theorem Proving with Selection and Simplification Journal of Logic and Computation 3 4 217 247 1994 C Chang and R C Lee Symbolic Logic and Mechanical Theorem Proving Computer Science and Applied Mathematics Academic Press 1973 N Dershowitz Ordering Based Strategies for Horn Clauses In J Mylopoulos editor Proc of the 12th IJCAI Sydney volume 1 pages 118 124 Morgan Kaufmann 1991 J Denzinger M Kronenburg and S Schulz DISCOUNT A Dis tributed and Learning Equational Prover Journal of Automated Reasoning 18 2 189 198 1997 Special Issue on the CADE 13 ATP System Competition J Denzinger and S Schulz Analysis and Representation of Equa tional Proofs Generated by a Distributed Completion Based Proof System Seki Report SR 94 05 Universitat Kaiserslautern 1994 J Denzinger and S Schulz Recording Analyzing and Present ing Distributed Deduction Processes In H Hong editor Proc 1st PASCO Hagenberg Linz volume 5 of Lecture Notes Series in Com puting pages 114 123 Singapore 1994 World Scientific Publishing J Denzinger and S Schulz Recording and Analysing Knowledge B
46. ses Syntax should be the same syntax as your proof problem E LOP TPTP or TSTP Just write down a list of clauses no watchlist simplification By default watch list clauses are sim plified with respect to the current set P Use this option to disable the fea ture 10Clauses are checked against the watchlist after normalization both when they are inserted into U or if they are selected for processing 20 4 5 Learning Clause Evaluation Functions E can use a knowledge base generated by analyzing many successful proof at tempts to guide its search i e it can learn what kinds of clauses are likely to be useful for a proof and which ones are likely superfluous The details of the learn ing mechanism can be found in Sch00 Sch01 Essentially an inference protocol is analyzed useful and useless clauses are identified and generalized into clause patterns and the resulting information is stored in a knowledge base Later new clauses that match a pattern are evaluated accordingly 4 5 1 Creating Knowledge Bases An E knowledge base is a directory containing a number of files storing both the knowledge and configuration information Knowledge bases are generated with the tool ekb_create If no argument is given ekb_create will create a knowledge base called E_KNOWLEDGE in the current directory You can run ekb_create h for more information about the configuration However the defaults are usually quite sufficient 4 5 2 P
47. t make constants the largest symbols This is allegedly used by SPASS Wei01 in some configurations const_min Sort symbols by arity symbols with higher arity are smaller but make constants the smallest symbols Provided for reasons of symmetry freq Sort symbols by frequency frequently occurring symbols are larger Ar ity is used as a tie breaker 16 invfreq Sort symbols by frequency frequently occurring symbols are smaller In our experience this is one of the best general purpose precedence gen eration schemes invfreqconstmin Same as invfreq but make constants always smaller than everything else invfreqhack As invfreqconstmin but unary symbols with maximal frequency become largest 4 2 2 Weight Generation Schemes Weight generation schemes are based on syntactic features of the symbol and the input clause set or on the predefined precedence The following options are available for order weight generation firstmaximal0 Give the same arbitrary positive weight to all function sym bols except to the first maximal one encountered order is arbitrary which is given weight 0 arity Weight of a function symbol f is n 1 i e its arity plus one aritymax0 As arity except that the first maximal symbol is given weight 0 modarity Weight of a function symbol f is n c where c is a positive constant W_TO_BASEWEIGHT which has been 4 since the dawn of time modaritymax0 As modarity except that
48. tegies are implemented NoSelection Perform ordinary superposition without selection NoGeneration Do not perform any generating inferences This strategy is not complete but applying it to a formula generates a normal form that does not contain any tautologies or redundant clauses 18 SelectNegativeLiterals Select all negative literals For Horn clauses this implements the maximal literal positive unit strategy Der91 previously realized separately in E SelectPureVarNegLiterals Select the first negative literal of the form X xY SelectLargestNegLit Select the largest negative literal by symbol counting function symbols count as 2 variables as 1 SelectSmallestNegLit As above but select the smallest literal SelectDiffNegLit Select the negative literal in which both terms have the largest size difference SelectGroundNegLit Select the first negative ground literal for which the size difference between both terms is maximal SelectOptimalLit If there is a ground negative literal select as in the case of SelectGroundNegLit otherwise as in SelectDiffNegLit Each of the strategies that do actually select negative literals has a corre sponding counterpart starting with P that additionally allows paramodulation into maximal positive literals Example Some problems become a lot simpler with the correct strategy Try e g eprover literal selection strategy NoSelection GRP0O01 1 rm_eq_rstfp lop eprover
49. the E home page http www eprover org Some other provers have influenced the design of E and may be refer enced in the course of this manual These include SETHEO MILT97 Ot ter McC94 MW97 SPASS WGR96 WAB 99 DISCOUNT DKS97 Wald meister HBF96 HJL99 and Vampire RV02 RVO1 2 Getting Started Installation of E should be straightforward The file README in the main direc tory of the distribution contains the necessary information After building you will find the stand alone executable E PROVER eprover E is controlled by a very wide range of parameters However if you do not want to bother with the details you can leave configuration for a problem to the prover To use this feature use the following command line options xAuto Select a literal selection strategy and a selection heuristic automagically based on problem fea tures tAuto Select a term ordering automagically memory limit xx Tell the prover how much memory measured in MB to use at most In automatic mode E will op timize its behaviour for this amount 20 MB will work 64 MB is reasonable 192 MB is what I use More is better but if you go over your physical memory you will probably experience very heavy swapping Example If you happen to have a workstation with 64 MB RAM the following command is reasonable eprover xAuto tAuto memory limit 48 PUZ031 1 rm_egq_rstfp lop This documentation will probably lag behind the develop
50. the first maximal symbol is given weight 0 aritysquared Weight of a symbol f n is n 1 aritysquaredmax0 As aritysquared except that the first maximal symbol is given weight 0 invarity Let m be the largest arity of any symbol in the signature Weight of a symbol f is m n 1 invaritymax0 As invarity except that the first maximal symbol is given weight 0 invaritysquared Let m be the largest arity of any symbol in the signature Weight of a symbol f n is m n 1 invaritysquaredmax0 As invaritysquared except that the first maximal symbol is given weight 0 precedence Let lt be the pre determined precedence on function symbols F in the problem Then the weight of f is given by g g lt f 1 the number of symbols smaller than f in the precedence increased by one 17 invprecedence Let lt be the pre determined precedence on function symbols F in the problem Then the weight of f is given by g f lt g 1 the number of symbols larger than f in the precedence increased by one freqcount Make the weight of a symbol the number of occurrences of that symbol in the potentially preprocessed input problem invfreqcount Let m be the number of occurrences of the most frequent symbol in the input problem The weight of f is m minus he number of occurrences of f in the input problem freqrank Sort all function symbols by frequency of occurrence which induces a total quasi ordering The weight of a sy
51. tive clauses Query clauses clauses with an empty head and starting with e g p X q X can optionally be used to define the a set of goal clauses by default all negative clauses are considered to be goals At the mo ment this information is only used for the initial set of support with sos uses input types Note that you can still specify arbitrary clauses as query clauses since LOP supports negated literals 5 2 TPTP Format The TPTP Sut05 is a library of problems for automated theorem prover Prob lems in the TPTP are written in TPTP syntax There are two major versions of the TPTP syntax both of which are supported by E Version 21 of the TPTP syntax was used up for TPTP releases previous to TPTP 3 0 0 12Version 1 allowed the specification of problems in clause normal form only Version 2 is a conservative extension of version 1 and adds support for full first order formulas 22 The current version 3 of the TPTP syntax described in SSCGO06 covers both input problems and both proof and model output using one consistent formalism It has been used as the native format for TPTP releases since TPTP 3 0 0 Parsing in TPTP format version 2 is enabled by the options tptp in tptp2 in tptp format and tptp2 format The last two options also se lect TPTP 2 format for the output of normal clauses during and after saturation Proof output will be in PCL2 format however As an alternative E also supports TP
52. ucture and substitutions and total on ground terms gt can be extended to an ordering gt on literals by comparing the multi set representation of literals with gt gt gt gt the multi set multi set extension of gt Clauses are multi sets of literals They are usually represented as disjunc tions of literals 5 2t V soXte VSnXtn We write Clauses F P V to denote the set of all clauses with function symbols F predicate symbols P and variable V If C is a clause we denote the multi set of positive literals in C by Ct and the multi set of negative literals in C by C7 The introduction of an extended notion of literal selection has improved the performance of E significantly The necessary concepts are explained in the following Definition 3 1 Selection functions sel Clauses F P V Clauses F P V is a selection function if it has the following properties for all clauses C e sel C CC e If sel C ACT f then sel C 0 We say that a literal is selected with respect to a given selection function in a clause C if sel C lt We will use two kinds of restrictions on deducing new clauses One induced by ordering constraints and the other by selection functions We combine these in the notion of eligible literals Definition 3 2 Eligible literals Let C LV R be a clause let o be a substitution and let sel be a selection function e We say a L is eligible for resolution if either sel
53. urrently it is possible to explicitly specify an arbitrary including incom plete or empty precedence or to use one of several precedence generating schemes Similarly there is a number of predefined weight function and the ability to assign arbitrary weights to function and predicate symbols The simplest way to get a reasonable term ordering is to specify automatic ordering selection using the tAuto option Options controlling the choice of term ordering 14 term ordering lt arg gt t lt arg gt Select a term ordering class or automatic selection Sup ported arguments are at least LPO LPO4 for a much faster new implementation of LPO KBO and Auto If Auto is se lected all aspects of the term ordering are fixed additional options will be or at least should be silently ignored order precedence generation lt arg gt G lt arg gt Select a precedence generation scheme see below order weight generation lt arg gt w lt arg gt Select a symbol weight function see below order constant weight lt arg gt c lt arg gt Modify any symbol weight function by assigning a special weight to constant function symbols precedence lt arg gt Describe a partial precedence for the term ordering The ar gument is a comma separated list of precedence chains where a precedence chain is a list of function symbols which all have to appear in the proof problem connected by gt lt or to denote equival
Download Pdf Manuals
Related Search