Redlog User Manual
Contents
1. 12 solution points 18 sorting atomic formulas 12 split trivial square sum 10 square free decomposition 10 standard simplifier 9 starting redlog 3 strict divistbulita cc 7 Substitution 7 subsumption 0 cee eee eee ee 16 T tableau ciu ke Ee ER nd 12 13 terr list eite in ita 23 term multiplicity list 23 term normal form 23 term order 15 UIT s ver atoa cipe ex Ee deme ee Ee MEN 22 trivial square aum sssunsesnee n 10 truth value asse ea rea ie 5 U universal closure oooooooomomoo 7 V verbosity output 15 22 W weak divisibility oo oooooooooo ih2. and level 1 The latter causes the whole formula to be simplified The simplification includes the following features Producing canonical forms for atomic formulas Proper treatment of truth values Flattening nested n ary operator levels and resolving invo lutive applications of not Changing repl to impl Considering interaction of atomic formulas on the same level switch rlsism Producing a canonical ordering among the atomic formulas on a given level switch rlsisort Recognizing equal subformulas on a given level switch rlsichk Passing down information that is collected during recursion switches rlsism rlsiidem In the OFSF case the atomic formula simplification includes the following Evaluation of variable free atomic formulas to truth values Function Chapter 3 Simplification 10 e Evaluation of trivial square sums to truth values switch rlsisqf Additive splitting of trivial square sums switch rlsitsqspl e Parity decomposition similar to square free decomposition of terms switch rlsipd with the option to split an atomic formula multiplicatively into two simpler ones switches rlsiexpl rlsiexpla e Moving the not operator into the relation with a single negated atomic formula Theory inconsistency may but need not be detected by rlsimpl In the first case an error is raised Else mind that under an inconsistent theory any formula is equivalent to the input rlsisqf Switch Simpl
3. straints The result is either infeasible or a two element list the first entry of which is the optimal value and the second entry is a list of points each one given as a substitution list where target has this value The point list does however not contain all such points For unbound problems the result is infinity JJ rloptis Switch Optimization one solution This is off by default If on rlopt returns at most one solution point Chapter 6 Miscellaneous 6 Miscellaneous 6 1 Global Switches rlsimpl Switch Simplify By default this switch is off With this switch on the function rlsimpl is applied at the expression evaluation stage rlrealtime Switch Real time By default this switch is off If on it protocols the wall clock time needed for REDLOG commands in seconds In contrast to the built in time switch the time is printed above the result rlverbose Switch Verbose By default this switch is off It toggles verbosity output with some REDLOG procedures The verbosity output itself is not documented up to now 6 2 Analyzing Formulas multiplicity list Data Structure A list of 2 element lists containing an object and the number of its occurrences Names of functions returning multiplicity lists typically end with ml rlatl formula Function List of atomic formulas Returns the set of atomic formulas contained in formula as a list rlatml formula Function Multiplicity list of atomic formulas Return
4. gt ivi v2 0 and vi 0 or v2 gt 0 v1 x v2 y 6 3 Other Stuff rlatnum formula Function Number of atomic formulas Returns the number of atomic for mulas contained in formula Mind that truth values are not considered atomic formulas rltnf formula term Function Term normal form terml is a list of terms This com bines DNF computation with tableau ideas A typical choice for terml is rlterml formula If the switch rltnft is off rltnf formula rlterml formula returns a DNF rltnft Switch Term normal form tree variant By default this switch is on causing rltnf to return a deeply nested formula Chapter 6 Miscellaneous 24 rlgentheo theory formula exceptionlist Function Generate theory formula is a positive quantifier free formula exceptionlist is a list of variables empty by default rlgentheo extends theory with inequalities not containing any variables from exceptionlist as long as the simplification result is better wrt this extended theory Returns a list extended theory sim plified formula Chapter 7 References 25 7 References Most of the references listed here are available on DS95 DS96 DSW96 LW93 Stu95 Stu96 Wei Wei88 Wei94a Wei94b Wei95 http www fmi uni passau de redlog Andreas Dolzmann and Thomas Sturm Simplification of quantifier free formulas over ordered fields Technical Report MIP 9517 FMI Universitaet Passau D 94030 Pas
5. 13 4 Normal epes c I d bes e RO XXE RR 16 4 1 Boolean Normal Forms oooocooooooocorcrrnromo sm 16 4 2 Other Normal Forms ie are Sour e SEDE AE EE eer ERIS 16 5 Quantifier Elimination and Variants 18 5 1 Quantifier Elimination ose A E 18 5 2 Generic Quantifier Elimination esee 20 5 3 Linear Optimization sintra sata Da E DRAMA Ganda 21 6 Miscellaneous lesse eese 22 6 1 Global Switches 1d ERR acte dere ata Rn 22 6 2 Analyzing Formulas 2 4 uctor e syne EE Us 22 SN QU pa ES ih RE REP EE 23 T Reler nces s suoi eg is 25 Function Index asa or oi 27 Variable Index x 2320 ee i ERE e 28 Data Structure Index 29 Concept Index Acknowledgements We acknowledge with pleasure the superb support by Herbert Melenk and Winfried Neun of the Konrad Zuse Institute Berlin during this project Furthermore we wish to mention numerous valuable mathematical ideas contributed by Volker Weispfenning University of Passau Using and Copying Permission is granted to use the free scientific REDLOG version available on http www fmi uni passau de redlog for scientific purposes Incorporation of the free scientific REDLOG version into other programs modification redistribution and commercial use are strictly prohibited There is a commercial REDLOG version marketed It provides the same functionality as the scientific one but includes a program documentation In contrast to the scientific
6. Chapter 5 Quantifier Elimination and Variants page 18 rlgqea formula theory Function Generic quantifier elimination with answer formula contains either only existential or only universal quantifiers Returns a list consisting of a theory and an elimination answer Com pare rlqea see Chapter 5 Quantifier Elimination and Variants page 18 and rlgge see Chapter 5 Quantifier Elimination and Variants page 18 After applying generic quantifier elimination the user might feel that the result is still too large while the theory is still quite weak There is a function rlgentheo which simplifies a formula by making further assumptions see Chapter 6 Miscellaneous page 22 Chapter 5 Quantifier Elimination and Variants 21 rlqegenct Switch Quantifier elimination generate complex theory This is on by default which allows to assume inequalities over non monomial terms with the generic quantifier elimination 5 3 Linear Optimization There is an optimization method implemented which uses the built in quantifier elimination encoding the target function by an additional con straint including a dummy variable This optimization technique has been described in Wei94a see Chapter 7 References page 25 rlopt constraints target Function Linear optimization constraints is a list of parameter free atomic formulas built up with lt or gt target is a poly nomial over the rationals target is minimized subject to con
7. algorithms is strongly influenced by our major research topics in this area i e quanti fier elimination and simplification Nevertheless REDLOG is designed as a general purpose computer logic system 1 2 Getting Started REDLOG is a REDUCE package which has to be loaded explicitly This is done by the following command within REDUCE load package rl Before starting work a context has to be selected 1 3 Contexts REDLOG is designed for working with several languages and theories in the sense of logic Both a language and a theory make up a context In addition a context determines the internal representation of terms The context to be used has to be selected explicitly This can be done in several ways The first possibility is using the rlset command rlset context arguments Function rlset argument list Function Set current context Currently valid choices for context are ofsf ordered fields standard form and dvfsf discretely val ued fields standard form With ofsf no further arguments are possible With dvfsf one can pass the maximal characteristic of the residue class fields wrt the valuation as a negative prime number The default is 0 leading to computations that are cor rect for all discretely valued fields rlset returns the old setting as a list that can be saved to be passed to rlset later When Chapter 1 Introduction 4 called with no arguments or the empty list rlset returns the current sett
8. automatic tableau sssesreeucns 12 B Boolean normal form 13 14 16 Boolean operator cece eee 5 brackets cierras m dee See se eas 5 branch wise tableau iteration 13 breadth first search o 19 C commercial versioO o o oooo ooo 1 conj nction asia iss He ale oe 5 conjunctive normal form 16 context default o ooooooo 4 context selection ooooooo ooo 3 count atomic formulas 23 CUL x ect e ta dete eet Ma ere ate due 16 depth first search 19 discretely valued field 6 dis UunctlOn icu eee best 5 disjunctive normal form 16 e De 7 E equatloB ii s be 6 7 equivalence 2 cece eee eens 5 existential closure eee eee 8 exploding Lem 11 expression input 5 6 7 8 expression Output 5 extended quantifier elimination 18 30 F Iockortsation 10 22 23 for loop action 5 formula structure 23 generic quantifier elimination 20 24 geometric problem 20 Groebner simplifier 13 idempotent simplification 12 implication cee eee ee eee 5 Inecdualta cc 6 7 input facilities 5 6 7 8 irreducible factors list 22 irreducible factors multiplicity list 22 iterative tableau 13 language default 4 languag
9. exceptionlist Function Universal closure exceptionlist is a list of variables empty by default Returns formula with all free variables universally quan tified except for those in exceptionlist Chapter 2 Format and Handling of Formulas rlex formula exceptionlist Function Existential closure exceptionlist is a list of variables empty by default Returns formula with all free variables existentially quantified except for those in exceptionlist rlmatrix formula Function Matrix computation Removes all leading quantifiers from for mula Chapter 3 Simplification 3 Simplification The goal of simplifying a first order formula is to obtain an equivalent for mula over the same language that is somehow simpler REDLOG knows three kinds of simplifiers The standard simplifier tableau simplifiers and Groeb ner simplifiers They are all described in DS95 Chapter 7 References page 25 3 1 Standard Simplifier The Standard Simplifier is a fast simplification algorithm that is fre quantly called internally by other REDLOG algorithms It can be applied automatically at the expression evaluation stage see Chapter 6 Miscella neous page 22 theory Data Structure A list of atomic formulas assumed to hold rlsimpl formula theory depth Simplify formula simplified recursively depth is an integer de scribing a level where recursion has to be stopped Defaults for the optional arguments are the empty theory
10. former one The focus of the implemented algorithms is on effective quantifier elimi nation and simplification of quantifier free formulas For ordered fields there are currently the following algorithms available Several techniques for the simplification of quantifier free formulas The simplifiers do not only operate on the Boolean structure of the formulas but also discover algebraic relationships For this purpose we make use of advanced algebraic concepts such as Groebner basis computa tions For the notion of simplification and a detailed description of the implemented techniques cf DS95 Chapter 7 References page 25 Quantifier elimination i e computing quantifier free equivalents for given first order formulas The current implementation is restricted to at most quadratic occurrences of the quantified variables We use a tech nique based on elimination set ideas Wei88 LW93 Wei Chapter 7 References page 25 A variant of the quantifier elimination procedure for geometric the orem proving Non degeneracy conditions are detected automatically DSW96 Chapter 7 References page 25 This has turned out useful also for physical applications such as network analysis Stu96 Chap ter 7 References page 25 Variants of both classical and generic quantifier elimination that provide answers e g satisfying sample points for existentially quantified formu las This has been referred to as the extended qua
11. formula theory Function rlgsd formula theory Function rlgsn formula theory Function Groebner simplifier formula is a quantifier free formula De fault for the optional argument is the empty theory These commands to invoke the Groebner simplifier differ only in the Boolean normal form which is computed at the beginning rlgsc computes a conjunctive normal form rlgsd a disjunctive normal form and rlgsn computes either a conjunctive or a disjunctive normal form in dependency on the structure of formula After computing the respective normal form the formula is simplified using Groebner simplification techniques The returned formula is equivalent to the input formula under the theory rlgsd x 0 and y 0 and x 2 2 y gt 0 or z 0 and x 3 z gt 0 gt x 0 and ze 0 rlgsc x neq O or y neq O or x 242 x y lt 0 and z neq O or x 3 z lt 0 gt x lt gt 0 orz lt gt 0 Chapter 3 Simplification 14 As described above the Groebner simplifiers rlgsc and rlgsd differ in the normal form computation at the beginning of the simplification For flat formulas the results of both are equal In general it is hard to decide which normal form conjunctive or disjunctive is smaller Moreover the simplification of the larger normal form can lead to a smaller final result than that of the smaller one One possible approach is to consider the top level operator of the formula e Use rlgsc for formulas with top level op
12. of Formulas After loading REDLOG and selecting a context there are first order for mulas available as an additional type of expressions 2 1 First order Operators Though the operators and or and not are already sufficient for rep resenting Boolean formulas REDLOG provides a variety of other Boolean operators for the convenient mnemonic input of Boolean formulas not Unary Operator and n ary Infix Operator or n ary Infix Operator impl Binary Infix Operator repl Binary Infix Operator equiv Binary Infix Operator The infix operator precedence is from strongest to weakest and or impl repl equiv rlbrop Fix Switch Bracket all operators By default this switch is on which causes some private printing routines to be called for formulas All subformulas are bracketed completely making the output more readable ex Binary Operator all Binary Operator These are the quantifiers The first argument is the quantified variable the second one is the matrix formula Optionally one can input a list of variables as first argument This leads to an expansion into several nested quantifiers true Variable false Variable These AM variables are reserved They serve as truth values mkand for loop action mkor for loop action Make and or Actions for the construction of large systematic conjunctions disjunctions via for loops Chapter 2 Format and Handling of Formulas 6 2 2 for i 1 3 mkand for j 1 3 mkor if j lt gt i th
13. Redlog User Manual Edition 1 0 for REDLOG Version 1 0 Andreas Dolzmann and Thomas Sturm MIP 9616 9 October 1996 Abstract REDLOG stands for REDuce LOGic system It provides an extension of the computer algebra system REDUCE to a computer logic system implement ing symbolic algorithms on first order formulas wrt temporarily fixed first order languages and theories Underlying theories currently available are ordered fields and discretely valued fields Though the focus of the imple mented algorithms is on effective quantifier elimination and simplification of quantifier free formulas REDLOG is intended and designed as an all purpose system REDLOG is freely available to the scientific community Copyright 1996 A Dolzmann and T Sturm Lehrstuhl fuer Mathematik Universitaet Passau Table of Contents NN eh e ee e ENEE 2 EL COMERC cahoots se ex a vae e aq e etr esa E dadas 2 12 Getting Starved iste etate e EE ES er ee 3 13 COMA SS cate e Ele boo ERROR eee e o Ale oor ote 3 14 On the Use of Switches 0 cece ees 4 2 Format and Handling of Formulas 5 2 1 First order Operator nai 5 22 OR SE Operators ne o auto bd dd does 6 20 DVESL ICO E RO Ie pe Gee 6 2 4 Extended Built in Commande 7 2 5 Advanced ECU ass ssa yale aaa e RR 7 gt SImplllcablon EE 9 SL Standard Simplifer x edax eo b as eA ERE ITI RES 9 dl Tableau uu pilar ati ex t EE ed t SR 12 3 3 Groebner Simplitier crac SEENEN ees
14. ation depth first search By default this switch is off It is ignored with the switch rlqeheu on which is the default Turning rlqedfs on makes rlge work in a depth first search manner instead of breadth first search This saves space and with decision problems it might save time In general it leads to larger results rlqeheu Switch Quantifier elimination search heuristic By default this switch is on which causes the switch rlqedfs to be ignored rlqe will decide between BFS breadth first search and DFs depth first search for each quantifier block where DFs is chosen when the problem is a decision problem rlqepnf Fix Switch Quantifier elimination make prenex normal form By default this switch is on which causes that rlpnf is applied to formula before starting the elimination process If the r1qe argument is already prenex this switch can be turned off This may be in particular useful with formulas containing equiv since currently rlpnf applies rlnnf and resolving equivalences can double the size of a formula rlqesr Advanced Switch Quantifier elimination separate roots This is off by default It affects the technique for substituting two solutions of a quadratic constraint during elimination The following two functions rlqeipo and rlqews are experimental im plementations The idea there is to overcome the obvious disadvantages of prenex normal forms with elimination set methods In most cases however the classical meth
15. atomic formulas are only evaluated if their left hand side is a domain element rlgsutord Advanced Switch Groebner simplifier user defined term order By default this switch is off Then all Groebner basis computations and reduc tions are performed with respect to the revgradlex term order If this switch is on the Groebner simplifier minds the term order selected with the torder statement For passing a variable list to torder note that rlgsradmemv is used as the tag variable for radical membership tests Chapter 4 Normal Forms 16 4 Normal Forms 4 1 Boolean Normal Forms rlcnf formula Function Conjunctive normal form formula is a quantifier free formula Returns a conjunctive normal form of formula rlcnf a 0 and b O or b 0 and c 0 gt as D or cs Oil and bs 0 rldnf formula Function Disjunctive normal form formula is a quantifier free formula Returns a disjunctive normal form of formula rldnf a 0 or b 0 and b 0 or c 0 gt a 0 andc 0 or b 0 rlbnfsac Fix Switch Boolean normal forms subsumption and cut By default this switch is on With Boolean normal form computation sub sumption and cut strategies are applied to decrease the number of clauses We give an example rldnf x 0 and y lt 0 or x 0 and y gt 0 or x 0 and y lt gt 0 and z 0 gt x 0 and y lt gt 0 rlbnfsm Switch Smart Boolean normal form By default this switch is off If on simplifier recognized implication is app
16. c Lente Mod etl Ma EN 13 T BST S ne seni cs sioe eee S 13 rlifacl ss vide vx ERIS 22 TlIYfacmllusc a p a ES 22 rlifstruct i e ia 23 ef Eh DEE 13 KE sos ris Slee eee eh ID EM 8 o yas eis 16 CLO Pt EE 21 TIPE espessas dete cowed ee a 17 VS retire in tanh abu REAL E situ 18 a EE 18 TGS posse eee eee ERES 20 UCIdgews tA tbe LEA 20 rlset cn e tesi EVER 3 rlsImploz d h etie Ieri 9 IlStr ct Morris 23 rlt ab ionge eee xd hend 12 rlterml i v2x uiu EET Es 23 TLCS TMM sa Sache et eee wes tune ese pau 23 TATI E ta A E Ee 23 S O 7 EE 7 Variable Index Variable Index rldeflangl sleep TISSDNE s vata tonite teats erede Tlgserfico4p EE 28 A A ee 19 TES ia AE 19 CITE alCiMe tia NO 22 Tis TC ds 12 EUS TeX PL AA Ae 11 KR RRE 11 Tita Cilia vee ieee 10 rIsliid m hs aay dt Seek 12 Kg RR EE 22 TISIPA EE 10 TlsYDO S4 tt M 11 BUS EE 11 GIS USM ise be eG weed ie EXON CPCRKS 12 al REENERT 12 rlslsQfic v Dudes vider bw uM 10 PSSS Piemonte cd 10 ritaDiD se stow ivan aa 13 TUCO Geta Ses i eee ALI 23 rlverbos8 Mini ee 22 T a Pa EE 5 Data Structure Index 29 Data Structure Index C S et 12 substitution list T E elimination answer 18 M T Concept Index Concept Index A A A ere imei mn 18 20 anti prenex normal form 17 20 atomic formula list 22 atomic formula multiplicity list 22 automatic simplification 22
17. e independently rlgsbnf Switch Groebner simplifier Boolean normal form By default this switch is on Then the simplification starts with a Boolean normal form computation If the switch is off the simplifiers expect a Boolean normal form as the argument formula Chapter 3 Simplification 15 rlgsvb Switch Groebner simplifier verbose By default this switch is on It toggles verbosity output of the Groebner simplifier Verbosity output is given if and only if both rlverbose and rlgsvb are on rlgsprod Advanced Switch Groebner simplifier product By default this switch is off If this switch is on then conjunctions of inequalities and disjunctions of equations are contracted multiplicatively to one atomic formula This reduces the number of atomic formulas but in most cases it raises the complexity of the terms Anyway most simplifi cations recognized by considering products are detected even if rlgsprod is off rlgsred Switch Groebner simplifier reduce polynomials By default this switch is on It controls the reduction of the terms wrt the computed Groebner bases The number of atomic formulas is never in creased Mind that by reduction the terms can become more complicated rlgserf Advanced Switch Groebner simplifier evaluate reduced form By default this switch is on It controls the evaluation of the atomic formu las to truth values If this switch is on the standard simplifier is used to evaluate atomic formulas Otherwise
18. e selection 3 linear programming 21 list of atomic formulas 22 list of terme 23 loading redlog ci 3 MAD As pas Dis as da 8 moving quantifiers inside 17 multiple occurrences 12 multiplicity list of atomic formulas 22 multiplicity list of irreducible factors 22 multiplicity list of terms 23 N DnegatlOnasz sos tae se vow tale tase da weed ats 5 negation normal form 16 normal form 13 14 16 17 23 number of atomic formulas 23 Concept Index O optimization lessen 21 ordered field cece eee eee eee 6 ordering 3 dk ed wae nhs ee ree 6 P parity decomposition 10 prefer orderings 11 prefer weak orderings 11 prenex normal form 17 19 20 protocols iip ERG ga meras po 15 22 Q quantifier cc cece eee eee 5 7 8 quantifier elimination 18 19 20 R radical membership test 14 real closed field o o o ooooo 6 Teal times Mite ssl Vee eA cis 22 reducton cece cetera 13 15 removing quantifiers 8 replication 0 eee eee eee eee 5 S scientific version 1 simplification 9 10 11 12 13 24 simplifier recognized implication 16 smart bnf computation 16 31 smart simplification
19. ely Chapter 2 Format and Handling of Formulas 7 equal Binary Infix operator neq Binary Infix operator div Binary Infix operator sdiv Binary Infix operator assoc Binary Infix operator nassoc Binary Infix operator The above operators may also be written as lt gt and respectively 2 4 Extended Built in Commands The REDUCE substitution command sub can be applied to formulas using the usual syntax substitution_list Data Structure substitution_list is a list of equations each with a kernel left hand side sub substitution_list formula Function Substitute Returns the formula obtained from formula by ap plying the substitutions given by substitution_list sub a x ex x x a 0 and all x x b gt 0 or ex a a b 0 gt ex xO x x0 lt O and all x0 b x0 gt O or ex a a b lt 0 sub works in such a way that equivalent formulas remain equiv alent after substitution In particular quantifiers are treated correctly part formula n1 n2 n3 Function Extract a part The part of formula is implemented analogously to that for built in types in particular the Oth part is the oper ator length formula Function Determine the length The length of formula is the number of arguments to the top level operator This is of particu lar interest with the n ary operators and and or Notice that part formula length formula is the part of largest index 2 5 Advanced Features rlall formula
20. en mkid x i mkid x j 0 gt true and false or false or xi x2 0 or xi x3 0 and false or xi x2 0 or false or x2 x3 0 and false or x1 x3 0 or x2 x3 0 or false OFSF Operators The OFSF context implements ordered fields over the language of ordered rings Proceeding this way is very common in model theory since one wishes to avoid functions which are only partially defined Furthermore we wish to point out that the quantifier elimination procedures for non linear formulas actually operate over real closed fields equal Binary Infix operator neq Binary Infix operator leq Binary Infix operator geq Binary Infix operator less Binary Infix operator p greaterp Binary Infix operator 2 3 The above operators may also be written as lt gt lt gt lt and gt respectively For OFSF there is specified that all right hand sides must be zero Non zero right hand sides in the input are hence subtracted immediately to the corresponding left hand sides There is a facility to input chains of the above relations which are also expanded immediately a lt gt b lt c gt d f gt a b lt gt O and b c lt 0 and c d gt 0 and d f 0 Here only adjacent terms are related to each other DVFSF Operators Discretely valued fields are implemented as a one sorted language using the operators and which encode lt lt and lt gt in the value group respectiv
21. ent relations when orderings are considered inconvenient rlsism Fix Switch Simplify smart By default this switch is on See the description of the function rlsimpl for its effects rlsimpl x gt 0 and x 1 lt 0 false rlsichk Fix Switch Simplify check By default this switch is on enabling checking for equal sibling subformulas rlsimpl x gt 0 and x 1 0 or x gt 0 and x 1 0 x gt 0 and x 1 0 rlsiidem Fix Switch Simplify idempotent By default this switch is on It is relevant only with switch rlsism on Its effect is that rlsimpl is idem potent i e an application of rlsimpl to an already simplified formula yields the formula itself rlsiso Fix Switch Simplify sort By default this switch is on It toggles the sorting of the atomic formulas on the single levels rlsimpl a 0 and b 0 or b 0 and a 0 gt a O0andb 0 3 2 Tableau Simplifier Although our deep simplifier already combines information located on different Boolean levels it preserves the basic Boolean structure of the for mula The tableau methods in contrast provide a technique for changing the Boolean structure of a formula by constructing case distinctions Com pared to the standard simplifier they are much slower cdl Data Structure Case distinction list is a list of atomic formulas considered dis junctively rltab formula cdl Function Tableau method The result is a tableau wrt cdl i e a sim plified equivalent of the disj
22. er Returns an elimination an swer obtained the following way w l o g the rlgea argument is prenex All quantifier blocks but the outermost one are elim inated For the latter the constructive information obtained by the elimination is saved e In case the considered block is existential for each evalua tion of the free variables we know the following Whenever a condition holds the input formula is true under the given evaluation and the solution is one possible evaluation for the outer block variables satisfying the matrix e The universally quantified case is dual Whenever a condi tion is false the input formula is false and the solution is one possible counterexample As an example we show how to find conditions and solutions for a system of two linear formulas Chapter 5 Quantifier Elimination and Variants 19 rlqea ex x x b1 gt 0 and a2 x b2 0 2 b2 gt a2 b1 a2xb2 gt O and a2 lt gt 0 x n a2 a2 lt 0 or a2 O and b2 lt 0 1x infinity1 The answer can contain new constants named either infinity or epsilon followed by a number All infinity s are positive and infinite and all epsilon s are positive and infinitesimal wrt the considered field Nothing is known about the ordering among the infinity s and epsilon s though this can be relevant for the points to be solutions With the switch rounded on the epsilon s are evaluated to zero rlqedfs Switch Quantifier elimin
23. erator and e Use r1gsd for formulas with top level operator or The procedure rlgsn implements this heuristic The Groebner simplifier uses the Groebner package of REDUCE to com pute the various Groebner bases By default the revgradlex term order is used and no optimizations of the ordering between the variables are applied The other switches and variables of the Groebner package are not controlled by the Groebner simplifier and may thus be adjusted by the user In contrast to the standard simplifier rlsimp1 the Groebner simplifiers can produce formulas with more atomic formulas than the input This however cannot happen if the switches rlgsprod rlgsred and rlgssub are off and the input formula is a simplified Boolean normal form The functionality of the Groebner simplifiers rlgsc rlgsd and rlgsn is controlled by numerous switches In most cases the default settings lead to a good simplification rlgsrad Switch Groebner simplifier radical membership test By default this switch is on If the switch is on the Groebner simplifier does not only use ideal membership tests for simplification but also radical membership tests This leads to better simplifications but needs considerably more time rlgssub Switch Groebner simplifier substitute By default this switch is on Certain subsets of atomic formulas are substituted by equivalent ones Both the number of atomic formulas and the complexity of the terms may increase or decreas
24. gt O0orat1i 0 rlsiexpl Switch Simplify explode By default this switch is on It is relevant with rlsisqf and one of rlsipd rlsifac or rlsitsqspl on With rlsiexpl on 7 6 5 4 3 2 a ta 3 a 3 a 3 a 3a a 1 gt 0 simplifies as in the description of the switch rlsiexpla whenever it occurs in a disjunction and it simplifies as in the description of the switch rlsipd else rlsipw Switch Simplification prefer weak orderings Prefers weak orderings in contrast to strong orderings with theory simplification rlsipw is off by default which leads to the following behavior rlsimpl a lt gt 0 and a gt 0 or b 0 gt a lt gt 0 and a gt 0 or b 0 This meets the simplification goal of small satisfaction sets for the atomic formulas leading e g to the following behavior rlsimpl a lt gt 0 and a gt 0 or b 0 a lt gt 0 and a gt 0 or b 0 rlsipo Switch Simplification prefer orderings Prefers orderings in contrast to inequations with theory simplification rlsipo is on by default which leads to the following behavior rlsimpl a gt 0 and a lt gt 0 or b 0 gt a gt 0 and a gt 0 or b 0 This meets the simplification goal of small satisfaction sets for the atomic formulas Turning it on leads e g to the following behavior rlsimpl a gt 0 and a gt 0 or b 0 gt a gt 0 and a lt gt 0 or b 0 Chapter 3 Simplification 12 Here we meet the simplification goal of conveni
25. ify square free By default this switch is on Enables sim plifications based on square free part computations square free decompositions and trivial square sums rlsimpl a 2 2 a b b 2 lt gt 0 gt atb lt gt 0 rlsimpl a 2 b 2 1 gt 0 gt true rlsifac Switch Simplify factorization By default this switch is on It is ig nored with rlsisqf off Explodes equations and inequations via factorization of their left hand side terms into disjunctions and conjunction respectively This is done in dependence on rlsiexpl and rlsiexpla rlsitsqspl Switch Simplify split trivial square sum This is on by default It is ig nored with rlsisqf off Trivial square sums are split additively depending on rlsiexpl and rlsiexpla rlsimpl a 2 b 2 gt 0 gt a lt gt 0 orb lt gt 0 rlsipd Switch Simplify parity decomposition By default this switch is on It is only relevant with the switch rlsisqf on rlsipd toggles the parity decomposition of terms occurring with ordering relations f a 1 3 a 1 4 gt 0 7 6 5 4 3 2 gt a ta 3 a 3a 3a 3a a 1 gt 0 Chapter 3 Simplification 11 rlsimpl f 3 2 gt a ta a 1 gt 0 rlsiexpla Switch Simplify explode always By default this switch is on It is rele vant with rlsisqf and one of rlsipd rlsifac or rlsitsqspl on f a 1 3 a 1 4 gt 0 T 6 5 4 3 2 gt a a 3 a 3 a 3a Gia a 1 gt 0 rlsimpl f gt a i1
26. ing Alternatively there are two ways to define a default context Either by setting a REDUCE fluid variable before loading r1 or by setting an environ ment variable before starting REDUCE rldeflang Fluid Default language This may be bound to a default context before loading r1 Typically one would add the following line to the reducerc file lisp rldeflang ofsf Notice that the Lisp list representation has to be used here If rldeflang is non nil rlset is automatically executed when loading rI Using an environment variable in contrast does not allow to specify extra arguments RLDEFLANG Environment Variable Default language This may be bound to a context in the sense of the first argument of rlset e g with the Bash shell one would say export RLDEFLANG ofsf With RLDEFLANG set any rldeflang binding is overloaded 1 4 On the Use of Switches REDLOG contains numerous switches Some of them have been introduced only for finding the right fine tuning of the functions They should not be changed anymore except for in very special situations For an easier orientation the switches are divided into three categories for documentation 1 Switch an ordinary switch 2 Fix Switch you do not want to change it 3 Advanced Switch you need a good knowledge about the underlying algorithms for making use of it Chapter 2 Format and Handling of Formulas 5 2 Format and Handling
27. ings of the International Symposium on Symbolic and Algebraic Computation in Oxford pages 258 263 New York July 1994 ACM Press Volker Weispfenning Solving parametric polynomial equations and inequalities by symbolic algorithms Technical Report MIP 9504 FMI Universitaet Passau D 94030 Passau Germany Jan uary 1995 Chapter 7 References Wei96 26 Volker Weispfenning Applying quantifier elimination to prob lems in simulation and optimization Technical Report MIP 9607 FMI Universitaet Passau D 94030 Passau Germany April 1996 To appear in the Journal of Symbolic Computa tion Function Index Function Index A all Gage aere WENN EE am 5 O Ren gov RD 5 ASSOC sua EES es 7 D GAY eaeque da c ace acie a es e a a 7 E equa ro bt 6 SUINA tas E Bil a 5 pq 5 BOQ isi e ILL LED Eius 6 Btreaterp eene 6 I AMP c ceu vestes mette emt 5 L Teng he ceu tt ee his etos T leq usu teeta SPR Ua dV eren 6 LS Piar cesos 6 M MEAN EE 5 MK OF ss ps edem Gs eve wa Pie ke Seer vats 5 N ASSOC wep oh pur ype ek ra EE T te gl e NUNT a a E EE 6 7 MLO Gadi ei eut EL mta cu D td 5 EE 5 P 27 R Topl ora cenicas EE 5 rialles a oe T Flapit oeei ii und ainda 17 rlataD usura Sich vowed sima conte byes 12 rlatl AI eE T 22 a afl 0 used da erede 22 Tela A A sh Sele el hoe eed a vu 23 aa Ke EEN 16 TINE EE 16 Cl is A eta MEME 8 rlgentheo ixc ize ir ir 24 e EE 20 e EE 20 TICS Gite ul fce eo a EE 13 TIS i
28. lied with CNF and DNF computations This leads to smaller normal forms but is considerably time consuming 4 2 Other Normal Forms rlnnf formula Function Negation normal form Returns a negation normal form of for mula This is an and or combination of either atomic or negated atomic formulas This function also copes with quantifiers In the OFSF case the result does not even contain negated atomic formulas since the negations can be encoded by relations We give an example rlnnf a 0 equiv b gt 0 gt a 0 and b gt 0 or a lt gt 0 and b lt 0 Chapter 4 Normal Forms 17 rlpnf formula Function Prenex normal form Returns a prenex normal form of formula The number of quantifier changes in the result is minimal among all prenex normal forms that can be obtained from formula by only moving quantifiers to the outside When formula contains two quantifiers with the same variable such as in dee 0 A Tue 0 there occurs a name conflict It is resolved according to the following rules e Every bound variable that stands in conflict with any other variable is renamed e Free variables are never renamed Hence rlpnf applied to the above example formula yields rlpnf ex x x 0 and ex x x lt gt 0 gt ex x0 ex x1 x0 O and x1 lt gt 0 rlapnf formula Function Anti prenex normal form Returns a positive formula equivalent to formula where all quantifiers are moved to the inside as far as possible rla
29. ntifier elimination problem Wei96 Chapter 7 References page 25 Linear optimization using quantifier elimination techniques Wei94a Chapter 7 References page 25 CNF DNF computation including both Boolean and algebraic simplifica tion strategies DS95 Chapter 7 References page 25 Several other normal form computations e g prenex normal form com putation minimizing the number of quantifier changes A lot of useful tools for constructing decomposing and analyzing for mulas Chapter 1 Introduction 3 For discretely valued fields there are not all algorithms available Cur rently this manual focuses on ordered fields Users interested in discretely valued fields are asked to study the ordered field documentation for now and to try out what works For the theoretical background of the discretely val ued fields algorithms cf Wei88 Stu95 Chapter 7 References page 25 For ordered fields it is planned to extend the quantifier elimination to higher degrees On the mathematical side the necessary methods are known Wei Wei94b Chapter 7 References page 25 This document serves as an user guide describing the usage of REDLOG from the algebraic mode of REDUCE For a detailed description of the sys tem s design see DS96 Chapter 7 References page 25 A program doc umentation is available only with the commercial version of REDLOG Finally we wish to point out that the range of available
30. od rlge has turned out superior Chapter 5 Quantifier Elimination and Variants 20 rlqeipo formula theory Function Quantifier elimination in position Returns a quantifier free equivalent to formula by iteratively making formula anti prenex and eliminating one quantifier rlqews formula theory Function Quantifier elimination with selection formula has to be prenex if the switch rlqepnf is off Returns a quantifier free equivalent to formula by iteratively selecting a quantifier from the inner most block moving it inside as far as possible and eliminating it 5 2 Generic Quantifier Elimination The following variant of rlqe enlarges the theory by disequations i e lt gt atomic formulas wherever this simplifies the quantifier elimination For geometric problems it has turned out that in most cases the additional as sumptions made are actually non degeneracy conditions The method has been described in detail in DSW96 see Chapter 7 References page 25 It has also turned out useful for physical problems such as network analysis see Stu96 Chapter 7 References page 25 rlgqe formula theory Function Generic quantifier elimination formula contains either only ex istential or only universal quantifiers Returns a list th f such that th is a superset of theory adding only disequations and f is a hopefully quantifier free formula equivalent to for mula assuming th For restrictions and options compare rlqe see
31. pnf ex x all y x 0 or y 0 and x z gt ex x x 0 or all y y 0 and ex x x z 0 Chapter 5 Quantifier Elimination and Variants 18 5 Quantifier Elimination and Variants REDLOG uses elimination set techniques for quantifier elimination Elim ination sets have been introduced in Wei88 Our implementation is based on the description of the linear case in LW93 and that of the quadratic case in Wei Chapter 7 References page 25 It includes however numerous sophisticated optimizations 5 1 Quantifier Elimination rlqe formula theory Function Quantifier elimination Returns a hopefully quantifier free equivalent of formula wrt theory where formulas has to obey certain degree restrictions The degree of all terms in the quanti fied variables must be at most 2 Moreover with the elimination of one quantifier the degree in the other quantified variables can increase In general it cannot be determined by inspection of the input formula whether the elimination will succeed There are various tricks for decreasing the degree of the input and of intermediate results built in In case that not all variables can be eliminated the resulting formula ist not quantifier free but still equivalent elimination_answer Data Structure A list of condition solution pairs i e a list of pairs consisting of a quantifier free formula and a set of equations rlqea formula theory Function Quantifier elimination with answ
32. s the atomic formu las contained in formula in a multiplicity list rlifacl formula Function List of irreducible factors Returns the set of all irreducible factors of the nonzero terms occurring in formula rlifacl xx x 2 1 0 gt x 1 x i rlifacml formula Function Multiplicity list of irreducible factors Returns the set of all irreducible factors of the nonzero terms occurring in formula in a multiplicity list Chapter 6 Miscellaneous 23 rlterml formula Function List of terms Returns the set of all nonzero terms occurring in formula rltermml formula Function Multiplicity list of terms Returns the set of all nonzero terms occurring in formula in a multiplicity list rlstruct formula kernel Function Structure of a formula Returns a list f sl f is con structed from formula by replacing each occurrence of a term with a kernel constructed by adding a number to kernel The substitution list sl contains all substitions to obtain formula from f rlstruct x y 0 and x 0 or y gt 0 v gt v1 0 and v2 0 or v3 gt 0 vi x y v2 x v3 y rlifstruct formula kernel Function Irreducible factor structure of a formula Returns a list f s1 f is constructed from formula by replacing each occurrence of an irreducible factor with a kernel constructed by adding a number to kernel The returned substitution_list s1 contains all substi tions to obtain formula from f rlstruct x y 0 and x 0 or y gt 0 v
33. sau Ger many October 1995 Andreas Dolzmann and Thomas Sturm Computer algebra meets computer logic Technical Report MIP 9603 FMI Uni versitaet Passau D 94030 Passau Germany February 1996 Andreas Dolzmann Thomas Sturm and Volker Weispfenning A new approach for automatic theorem proving in real geometry Technical Report MIP 9611 FMI Universitaet Passau D 94030 Passau Germany May 1996 Ruediger Loos and Volker Weispfenning Applying linear quan tifier elimination The Computer Journal 36 5 450 462 1993 Special issue on computational quantifier elimination Thomas Sturm Lineare Quantorenelimination in bewerteten Koerpern Diploma thesis FMI Universitaet Passau D 94030 Passau Germany February 1995 Thomas Sturm Using symbolic methods for automatic reason ing over networks Preliminary draft FMI Universitaet Passau D 94030 Passau Germany October 1996 Volker Weispfenning Quantifier elimination for real algebra the quadratic case and beyond To appear in AAECC Volker Weispfenning The complexity of linear problems in fields Journal of Symbolic Computation 5 1 3 27 February 1988 Volker Weispfenning Parametric linear and quadratic optimiza tion by elimination Technical Report MIP 9404 FMI Univer sitaet Passau D 94030 Passau Germany April 1994 To appear in the Journal of Symbolic Computation Volker Weispfenning Quantifier elimination for real algebra the cubic case In Proceed
34. unction over the specializations wrt all atomic formulas in cdl rlatab formula Function Automatic tableau method Tableau steps wrt a case distinc tion over the signs of all terms occurring in formula are computed Chapter 3 Simplification 13 and the best result i e the result with the minimal number of atomic formulas is returned rlitab formula Function Iterative automatic tableau method formula is simplified by iterative applications of rlatab The exact procedure depends on the switch rltabib rltabib Switch Tableau iterate branch wise By default this switch is on It controls the procedure rlitab If rltabib is off rlatab is iteratively applied to the argument formula as long as shorter results can be obtained In case rltabib is on the respective next tableau step is not applied to the last tableau result but to each branch The iteration stops when the obtained formula is not smaller than the respective input 3 3 Groebner Simplifier The Groebner simplifier is a special simplifier of the OFSF package It con siders order theoretical and algeraic simplification rules between the atomic formulas of the input formula Currently the Groebner simplifier is not idem potent The name is derived from the main mathematical instrument used for simplification Computing Groebner bases of certain subsets of terms occurring in the atomic formulas For calling the Groebner simplifier there are the following functions rlgsc
35. version it may be used for commercial purposes incorporated into other programs and modified For obtaining the commer cial version mail to redlog fmi uni passau de Our group also provides mathematical and technical support For all REDLOG versions there is no warranty for the program to the extent permitted by applicable law Except when otherwise stated in writ ing 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 Bug Reports and Comments Send bug reports and comments to redlog fmi uni passau de Any hint or suggestion is welcome In particular we are interested in short reports on practical problems to the solution of which our software has contributed Chapter 1 Introduction 2 1 Introduction 1 1 Overview REDLOG stands for REDuce LOGic system It provides an extension of the computer algebra system REDUCE to a computer logic system implementing symbolic algorithms on first order formulas wrt temporarily fixed first order languages and theories Underlying theories currently available are ordered fields and discretely valued fields where the focus is on the
Download Pdf Manuals
Related Search