E 1.4 User Manual - Software and Systems Engineering
Contents
1. FunWeight lt prio fun gt lt int gt lt int gt lt float gt lt float gt lt float gt lt fun gt lt posint gt I SymOffsetWeight lt prio fun gt lt int gt lt int gt lt float gt lt float gt lt float gt lt fun gt lt int gt TNote that there now are many additional generic weight functions not yet documented 12 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 of 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 curre2. E theorem prover 6 eligible for paramodulation see liter als eligible eligible for resolution see literals eli gible eligible literals see literals eligible equality resolution 7 equality factoring 5 equality resolution 5 equations 3 GNU General Public License 28 GNU Lesser General Public License 28 GPL 28 LGPL 28 literal 3 literals eligible 4 5 ordering 4 proof procedure 9 reduction ordering 4 rewriting 5 6 selection functions 4 simplify reflect 6 SP calculus 5 SPASS 6 8 subsumption 6 subterm 3 superposition 5 tautology deletion 7 term ordering 15 31
3. 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 Based Distributed Deduction Processes Journal of Symbolic Com putation 21 4 5 523 541 1996 28 HBF 96 HJL99 McC94 MIL 97 MW97 NN93 RV01 RV02 Sch99 Sch00 Sch01 Sch02 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 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 I
4. Sort all function symbols by frequency of occurrence which induces a total quasi ordering The weight of a symbol 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 sel
5. paramodulation into positive literals only if no ground literal has been selected 9Clauses are checked against the watchlist after normalization both when they are inserted into U or if they are selected for processing 20 sure that the 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
6. 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 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 orderings 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
7. constant W_TO_BASEWEIGHT which has been 4 since the dawn of time modaritymax0 As modarity except that 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 ism 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 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 18 freqrank
8. on a lexicographic comparison of symbols and subterms and is fully specified by giving just a precedence Currently 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 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 15 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 func
9. 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 related 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 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 26 H H A Processed positive unit clauses Equations Processed negative unit clauses Inequations 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 Unprocessed positive
10. 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 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 if c is trivial or subsumed by P then Delete ignore c else if c is the empty clause then Success Proof found sto else P T Temporary clause set foreach p P do if c simplifies p P P P U U dld is direct descendant of p T TU p done P U c 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
11. strategy Try e g eprover literal selection strategy NoSelection GRP001 1 rm_eq_rstfp lop eprover literal selection strategy SelectLargestNegLit GRP001 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 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 saturation 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 8Except for SelectOptimalLit where the resulting strategy PSelectOptimalLit will allow
12. unit clauses Unprocessed negative unit clauses Unprocessed non unit clause this set may contain the empty clause in very rare cases Print equality axioms if equality is present in the prob lem This letter prints axioms for reflexivity symmetry and transitivity and a set of substitutivity axioms one for each argument position of every function symbol and pred icate symbol As a 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 pd pl sc cd nl no nv Clause ident probably only useful internally Depth of the derivation graph for this clause Number of nodes in the derivation grap Symbol count function symbols and variables Depth of the deepest term in the clause Number of literals in the clause Number of variable occurences Number of different variables 27 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 version 2 0 or later or the GNU Lesser General Public License version 2 1 or later 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 lice
13. E 1 4 User Manual preliminary version Stephan Schulz August 20 2011 Abstract E is an equational theorem prover for full first order logic based on superposition 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 1 Introduction 2 Getting Started 3 Calculus and Proof Procedure elt MCalCulus ia td aa tek ote ee A a a hd ees bs a N 32 Proof Procedure m see Ge bates ae bokeh ese eee a A 4 Usage 4 1 Search Control Heuristics oo 4 1 1 Priority functions 6 aos d od eoa ae wee we h 4 1 2 Generic Weight Functions s sooo 4 1 3 Clause Evaluation Functions AVA Heuristics e e a 0p ook Ba bE A ek Pee Pe os 4 2 Term Orderings o f so once ee eG ed o e a E 4 2 1 Precedence Generation Schemes 4 2 2 Weight Generation Schemes 0 4 3 Literal Selection Strategies 2 ee en 4 4 The Watchlist Feature 20 000 4 5 Learning Clause Evaluation Functions 4 5 1 Creating Knowledge Bases 0 4 5 2 Populating Knowledge Bases 22 4 5 3 Using Learned Knowledge 0 22 4 6 Other Options sn ona ee E a ik Ee ee ee eh te a 22 5 Input Language 22 Beds HOP cs es 6s by aos Sele th he Bee cy ad Beer eM ad od Ae SE 22 5 2 TPTP Format
14. TPTP language and it adds a number of useful features E supports TPTP 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 11Version 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 23 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 Essential
15. als 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 SimulateSOS 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 11 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 e
16. 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 clauses 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 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 21 You can run ekb_create h for mo
17. cw soe ee be ee ee De ee 23 6 Output or how to interpret what you see 24 6 1 The Bare Essentials 0 0 0200000 eee 24 6 2 Impressing your Friends aoaaa 25 6 3 Detailed Reporting 0 0 0 2 0 020000 25 6 4 Requesting Specific Output 200 26 A License 28 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 the 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 the E home page http w
18. ect pure theorem proving tasks e Enormally treats procedural clauses exactly as it treats declarative 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 The current version 3 of the TPTP syntax described in SSCG06 covers both input problems and both proof and model output using one consis tent 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 TPTP syntax version 3 is the currently recommended format It is supported by many provers it is more consistent than the old
19. ection strategy is selected with the option literal selection strategy Currently at least the following strategies 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 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 19 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
20. ersion 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 a 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 1 mphasis 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 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 s t represented as s t A ground reduction ordering gt is a Noetherian partial ordering that is stable w r t the term structure and substitu
21. he 2nd IJCAR Cork Ireland volume 3097 of LNAI pages 223 228 Springer 2004 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 of 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 30 Index clause evaluation 13 terms 3 clause splitting 7 contextual simplify reflect 6 variables 3 DISCOUNT 8 xyzzy 3
22. ht ConstPrio 1 1 2 flat E_KNOWLEDGE 100000 1 0 1 0 Flat IndexIdentity 100000 20 20 2 1 0 2 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 10The name is an historical accident and has no significance anymore 22 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 aff
23. iating a generic weight function It can either be specified directly or specified and given a name for later reference at once 13 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 4 1 4 Heuristics A heuristic defines how many selections are to be made according to one of several clause evaluation function
24. ikely to happen Since KBO needs a total weight function E always uses a weight generation scheme in addition to the user defined op tions You may want to use wconstant for predictable behaviour 16 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 symbol
25. imal 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 p maximal in o sel C NCT e o 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 sorts We sometimes write the literal P t1 in T as P t1 tn and P ti tn T as aP ti tn for simplicity 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 D C F is a set of unused constant predicate symbols Different clauses are assumed to not share any common variables Definition 3 3 The i
26. nference 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 selection function The inference system SP consists of the following inference rules e Equality Resolution ER ugvV R if o mgu u v and o u a R v is eligible for resolution e Superposition into negative literals if o mgu ulp s a s E ET o t o u a o o s t SN is eligible for paramodula o ulp amp t AvV SV R tion o u v is eligible for resolution and u p V e Superposition into positive literals if o mgu ulp s o s ET a t a al ols t SP is eligible for paramodula o ulp tl uV SV R tion o u v is eligible for resolution and u V e Equality factoring if o mgu s u o s tVuruVR aN EF 5 2 a t and o s t eligible for o tfuVurvV RB paramodulation Rewriting of negative literals RN ee fd Sood E sxt ulpco t ZuVR sei aa i Ki Rewriting of positive literals SLE HROVR if ulp a s o s gt o t and RP if uv is not eligible for reso sxt ulpcoa t euVR lution or u vorp A e Clause subsumption C o CVR where C and R are arbitrary CS E partial clauses and is a C substitution Equality subsumption sxt ulp o s u lp o t VR ES sat Positive simplify reflect sxt ulpco s 4ulpco t VR PS Eo sxt R Negative simplif
27. nse you agreed to If you are in doubt about which version of E you have run eprover V or eprover h See the file COPYING in the main directory for the full text of the licenses References Bac98 BDP89 BG94 CL73 Der91 DKS97 DS94al DS94b DS96 L Bachmair Personal 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
28. ntly work very well even for unit clauses RTFS in lt che_simweight c gt to find out more 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 FunWeight prio prio fweight vweight term_pen lit_pen posmult fun fweight This evaluation function is a variant of Refinedweight The first 6 parameter are identical in meaning The function takes an arbitrary number of extra parameters of the form fun fweight where fun is any valid function symbol and fweight is a non negative integer The extra weight assignments will overwrite the default weight for the listed function symbol SymOffsetWeight prio prio fweight vweight term_pen lit _pen posmult fun fweight This evaluation function is similar to FunWeight The first 6 parameter are identical in meaning The extra arguments allow both positive and negative values and are used as once off weight modifiers added to the weight of all clauses that contain the defined symbol 4 1 3 Clause Evaluation Functions A clause evaluation function is constructed by instant
29. p P Apply TD or efficient approximation of it if p is trivial Delete ignore p else U U U cheap simplify p P fi Initial U is satisfiable P describes model Figure 1 Main proof procedure of E 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 suitable 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
30. 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 10 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 PreferNew 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 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 go
31. quivalence class on clauses Clauses generated from the same given clause are grouped together and can be ordered with any evaluation function among each other 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 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 fun 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
32. r strategy in which case the prover may never terminate or some strange and unexpected things happen 24 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 he 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 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 t
33. re information about the configuration However the defaults are usually quite sufficient 4 5 2 Populating 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 TSMWeig
34. ries 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 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 or TPTP 3 output 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 13PCL2 is a proof output designed as a successor to PCL DS94a DS94b DS96 25 6 4 Requesting Specific Output 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
35. s 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 This 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 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 12Unless the prover runs out of memory see below the user selects an unfai
36. s Syntactically lt heu element gt lt int gt lt eval fun gt lt heuristic gt 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 14 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 Bendix 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
37. s with higher arity are smaller const_max Sort symbols by arity symbols with higher arity are larger but 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 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 invfregqhack As invfreqconstmin but unary symbols with maximal frequency become largest 17 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 n 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
38. ssue 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 Description 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 htm1 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 Miinchen 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 29 Sch04 SSCG06 Sut05 Tam97 WAB 99 Wei99 Wei01 WGR96 S Schulz System Description E 0 81 In D Basin and M Rusinow itch editors Proc of t
39. tion symbols which all have to appear in the proof problem connected by gt lt or to denote equivalent 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 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 unl
40. tions 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 the multi set multi set extension of gt Clauses are multi sets of literals They are usually represented as disjunc tions of literals s 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 gt 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 NCT 9 then sel C 9 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 L V 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 C 9 and o L is gt z max
41. ww 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 Choose a literal selection strategy and a clause evaluation heuristic automagically based on problem features 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 96 MB is reasonable 768 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_eq_rstfp lop This documentation will probably lag behind the development of the latest v
42. y V o mgu z y if R and S do not share any variables d D has not been used in a previous definition R does not contain any sym bol from D and S does not consist of only symbols from D if is a variable renaming R and S do not share any vari ables d D R does not contain any symbol from D and S does not consist of only symbols from D We write SP N to denote the set of all clauses that can be generated with one generating inference from J on a set of clauses N Dsp to denote the set of all SP derivations and Dp to denote the set of all finite SP derivations lt 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 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 Non equational literals are encoded as equations and dealt with accordingly 3 2 Proof
43. y reflect Contextual top level simplify reflect ao CVRVs t CVs t where s t is the negation of CSR i ue 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 sxt ulppco t rxuVR u vor p Xora 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 TD nee Deletion of duplicate literals sxtVsetVR sotVR DD Deletion of resolved literals s zsVR DR E Destructive equality resolution cr yVR DE DE ZR Introduce definition RvS dVR 7dvVS e Apply definition a dVR RvS o dVR dvs AD if C is a tautology if x
Download Pdf Manuals
Related Search