Home

Redlog User Manual

1. 14 substitution 12 14 25 26 31 subsuniption 2 my rem RR eds 27 super quadratic special case 30 SUP POM Us Zub eite Pes ws ne mre eR deas 1 SWItGH spes 2cdhe dant RISE xe ew cade ed 4 T tableatis 23 eng coh PIER Rbve s 23 28 Index tag variable 5 eee e 26 term lisi lewis mecele 14 term multiplicity list 14 term normal form 28 term ord r 4 2 2 2 0 0 0r6 dbase 25 THEOT Ys Soie aa EM ree 5 34 theory implicit 0 00 16 Vue iis zs cire ee eas ee 13 trivial square sum 18 19 truth value 8 12 13 16 17 20 25 30 U universal closure 22000 8 unsplit atomic formulas 25 Update MET 1 49 V valuation p adic 000 5 valuation relation 0 20 valued field s c42s 0 eee 4800 bee eew eee 5 variable ligt 8 2i csse vende os 14 variable renaming 28 variable free atomic formula 17 20 verbosity output 00 13 25 virtual substitution sees 29 wall clock time cocer 13 weak divisibility 10 weak orderings 60 18 Short Contents Iu trOdldBDCbODas boca ec 2 ww a ee wwe RC ROR OR a CR CR RR 2 2 Leoadimg and Context Selection ass R9 ee eda si eeae aa 5 3 Format and Handling of Formulas 2223 9 mmm man 7 4 OMINDURCHLION 62240644 eee ee rede dase e
2. lulius 2 15 real numbers RR exu 2 real imnge osnbnteserx datu qase dons 13 reciprocal ecc kde ER samen 9 reduce polynomials 24 25 relabiOnB 225a dnt Fee eela ae 5 remove quantifiers 14 rename variables lusus 28 feplicatlOm imeem IRE tiranas e REP T reyvgradlex ii 24d sorre madis 25 S sample solution luus 29 SAVEISPACE drs bb Asal ee aree ntes ari ge 30 SAVE TIME co loue G4 bb betaine PE ur ens 30 search heuristic 00000005 30 Separate TOOTS 4 05 pss sods Geddes a seve ta ers 91 set of atomic formulas 13 set of irreducible factors 13 set of variables 0000000 14 sign conditions 2 e sedans 26 simplification 23 24 34 simplification of atomic formulas 17 19 20 21 13 15 16 17 18 19 21 simplifier recognized implication 27 small satisfaction sets lusus 18 smart BNF computation 2T smart simplification 16 17 SODULIOTI o s ihe 30 36 solution points seeeeseeees 29 sort atomic formulas 17 split atomic formula 16 17 18 19 20 21 split trivial square sum 19 squarefree part 18 19 20 standard simplifier 15 25 Starting REDLOG 222i m n eyed 5 strict divisibility x24 oss in 10 strict orderings s erii rere 18 structure of formula
3. 21 explode terms 16 T7 expression input 7 8 10 11 expression output T extend theory ets 34 35 extended quantifier elimination 29 F factorization 13 14 18 19 20 21 factors irreducible 13 14 Tix Switsers rai e ER RR gard od Go aes 4 flatten nested operators 16 for loop action coe IRE 11 formula structure 0005 14 free variables 00000 14 functions dace rdi eee tee sce bet eye 5 G GOD gies same Be aie uestes Auct ed eaten 20 generate theory 34 35 generic cylindrical algebraic decomposition 35 generic Hermitian quantifier elimination Magid depo e pae poeta donde 35 generic quantifier elimination 34 geometric problem 3 34 greatest common divisor 20 Groebner basis uueeeeuuss 24 Groebner simplifier 23 24 guess full CAD size 32 H Hermitian quantifier elimination 34 H6UPISHIC 2s botes esae iere ee Reed 30 47 home page oues meme AID Iwe4eIA 1 I IBALDP o oaii eiea Epa isenseeiduetideneiv 5 ideal membership test 24 idempotent simplification Lie LN plicatlom heros ote aee cepere espe 7 implicit theory 16 18 inequality 2 26 lome rre 8 I0 11 infea sibl ev ei Ee 36 infindbyo se silice e Bg
4. 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 applying 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 ex x0 x x0 lt 0 and all x0 b x0 gt 0 or exa a b lt 0 sub works in such a way that equivalent formulas remain equivalent 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 operator Compare rlmatrix see Section 3 11 Basic Functions on Formulas page 13 for extracting the matrix part of a formula i e removing all initial quantifiers length formula Function Length of formula This is the number of arguments to the top level operator The length is of particular interest with the n ary operators and and or Notice that part formula length formula is the part of largest index 3 10 Global Switches There are three global switches that do not belong to certain procedures but control the general behavior of REDLOG Chapter 3 Format and Handling of Formulas 13 rlsimpl Switch Simplify By default this switch is
5. S SUB vis ie veawate nase EQ ud i 3 12 T Switches and Variables Switches and Variables Documentation of Switches and Variables TIAdM CON es eee beet these heed ae 9 rlanuexdeb g ss 2 incceeced coeds cae 33 rlanuexdifferentroots 33 rlanuexgcdnormalize 34 rlanuexpsremseq sees 33 rlanuexsgnopt eee oe 34 rlanuexverbose esses 33 rlbnfsacc ener esr nE reed 21 FYlIDBfTBSU DI u pbi oues aec 27 TIDTOp ealdeewetruepet hi stie Dedenipens T rlc adaptroj nie decease bowen es 33 rlcadaprojalw yS cem ek 33 rl adbasSonly ws i Geta ies 32 rlcaddebug 4 io ee ais 33 rlcadextonldy 25 eke kane teks 32 rl 6adfac bo ip eu p b ERO 32 rlcadfulldimonly 2 329 s 32 rlcadhongproj 22 0d 3s res 33 rlcadisoal roots 2 deb Re 33 rlcadparti l c2 liscseo e d in ones 32 rlcadpbfwvs i BRI DI et 32 rlcadprojonly i Re ERE ERIS 32 rlcadrawformul a ee 32 33 TI GAA scrinio LI aed alae eed 32 TIGAGCr AMET CG eee set s seine lak ieee pes 32 rlcadverbose 2 c tb dads 33 REDEFEANG eie dr Rem reg pers 6 rldeflangl seeb er eure ad 6 rlgsbnf ii cie b Rr pP eee oes 25 IlgSOerf llsslte ub eb ce AEA 25 rlgsprod skecemet girip ii Tee 25 TigsTadi 3 cietcepigsescanmee Soe ede 24 rlgsradmemv ee nce eee 25 26 43 TIGSLE 6 i nice dee eae aes besa 25 PUGS SUD 6 2a cca beni aed dee ae nnda 25 Ilgsutord a aco nd aed ale bez 25 PUGS VD ie oe
6. Simplifier page 15 the Groebner simplifiers can in general produce formu las containing more atomic formulas than the input This 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 takes considerably more time Chapter 4 Simplification 25 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 decrease 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 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 formula
7. ad dees Red Ji N MASSOC e i wissen Fg og dha Vises dacs Yuri EUER 10 HnCODE qd 4e EEG DI Ga E dnd 10 neQq lipeesbe vig c E RET 8 10 11 DM 7 Ofciss QUbIewsesPBbeebxe eere eevee cae Y P Patt atte cheeks rE DI 12 n 0 Ee ree ee 7 Plallsiieeeresbee rw eda weed ae 8 nl 0 0 ee a aa ear area 28 PLACARD es acre Pie eS bet RS PRIME Aa tis 23 bg vr ae ee EE 13 PLAC oi edren etes dba svete aed ae oss 13 PLACHUM 6 324 ata d need Qe RE 13 Elbvarl oo a OE 14 rlcad eo re RR ittea tenio ERES 31 rlcadguessauto 0005 32 rlcadporder 2 22 tI satis 32 IlOnfz i3 ced nba cup rs 2r rldecdeg 2l Godsend seiri d bd 26 rldecdegli si ded de Rd 26 rldnf eR ERES 27 ElOX o eese 03 ote ga PEU aes 8 Pl xplatsie cig esse law EEPeRE winded 21 Functions Ilg dd 222932125 ntn pe gree Piae 35 rlgentheO i Ue IRR Sene 34 rlghqe iusso ea Breede ae aS 35 TICE ii 4 sane snig pi sa oh RE ge bad 34 Ilgd a s eda EEEE 34 Jg I EP 24 rlgsd ic ne duda dg bene bei pes 24 PU GSW ici he ow ned Hawa te Wedd pande 24 rlhgecgcsesctewbRtsr RE Gee yug 34 rlif86l l se tae iS Babee eris 13 rllfacmilclscreldee dX eR TIG 13 rlifstruct oon RM ae ke eiee le ft 14 TIDAD se oboe se het ease hee he 23 sa i Ko e csiocee eh ehde pase ente ween e 35 rlmatrixo seh ene eee Ae baie 14 TIINAT orie geina eaaa e ames 21 IlODt Deben s E a E ets 35 41 TQS E E E E E E EETA 29 san Ke E E E E E 29 TUGCUP Os lo Dee Du E TEE 31 LlqeW
8. off With this switch on the function rlsimpl is applied at the expression evaluation stage See Section 4 1 Standard Simplifier page 15 Automatically performing formula simplification at the evaluation stage is very similar to the treatment of polynomials or rational functions which are converted to some normal form For formulas however the simplified equivalent is by no means canonical 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 Advanced Switch Verbose By default this switch is off It toggles verbosity output with some REDLOG procedures The verbosity output itself is not documented 3 11 Basic Functions on Formulas rlatnum formula Function Number of atomic formulas Returns the number of atomic formulas contained in formula Mind that truth values are not considered atomic formulas In PASF the amount of atomic formulas in a bounded formula is computed syntactically without expanding the bounds multiplicity_list Data Structure A list of 2 element lists containing an object and the number of its oc currences Names of functions returning multiplicity_lists typically end on ml rlatl formula Function List of atomic formulas Returns the set of atomic formulas contained in formula as a list rlatml formula Function Multiplic
9. resp The operators bimpl brepl and bequiv may be written as gt lt and lt gt resp equal Binary Infix operator The operator equal may also be written as 3 8 DCFSF Operators d Binary Infix operator The operator d denotes higher derivatives in the sense of differential algebra For instance the differential equation g a2 0 is input as x d 1 2 x 0 d binds stronger than all other operators equal Binary Infix operator neq Binary Infix operator The operator equal may also be written as The operator neq may also be written as lt gt 3 9 Extended Built in Commands Systematic conjunctions and disjunctions can be constructed in the algebraic mode in analogy to e g for sum mkand for loop action mkor for loop action Make and or Actions for the construction of large systematic conjunc tions disjunctions via for loops Chapter 3 Format and Handling of Formulas 12 for i 1 3 mkand for j 1 3 mkor if j lt gt i then mkid x i mkid x j 0 gt true and false or false or xi x2 0 or x1 x3 0 and false or x1 x2 0 or false or x2 x3 0 and false or xi x3 0 or x2 x3 0 or false Here the truth values come into existence due to the internal implementa tion of for loops They are always neutral in their context and can be easily removed via simplification see Section 4 1 Standard Simplifier page 15 see Section 3 10 Global Switches page 12
10. rlsiatadv Switch Turns the advanced PASF speciefic simplification of atomic formulas on For details see See Section 4 1 9 PASF specific Simplifications page 21 Beside the standard simplification PASF provides a powerfull standard simplifier extension based on the package susiI This feature uses special properties of PASF formulas to reduce the formula size using the concept of implicit theory Chapter 4 Simplification 23 rlsusi Switch Turns the advanced SUSI simplification on Per default this switch is on 4 2 Tableau Simplifier Although our standard simplifier see Section 4 1 Standard Simplifier page 15 already combines information located on different boolean levels it preserves the basic boolean structure of the formula The tableau methods in contrast provide a technique for changing the boolean structure of a for mula by constructing case distinctions Compared to the standard simplifier they are much slower For details on tableau simplification see DS97 cdl Data Structure Case distinction list This is a list of atomic formulas considered as a disjunction rltab formula cdl Function Tableau method The result is a tableau wrt cdl i e a simplified equiv alent of the disjunction over the specializations wrt all atomic formulas in cdl rltab a 0 and b O or d O and e 0 or a 0 and c 0 a 0 a lt gt 0 a 0 and b 0 or c O or d 0 and e 0 rlatab formula Funct
11. sophisticated simplifications for atomic formulas in the style of rlsiatadv on see Section 4 1 4 OFSF specific Standard Simplifier Switches page 18 rlsifac Switch Simplify factorization By default this switch is on Toggles certain sim plifications that require integer factorization See Section 4 1 7 DVFSF specific Simplifications page 20 for details 4 1 9 PASF specific Simplifications Due to a simple term structure a lot simplification can be performed on PASF atomic formulas with the total goal of reducing the absolute summ of the coefficients In the PASF context the atomic formula simplification includes the following e Evaluation of trivial domain valued atomic formulas to truth values e g variable free atomic formulas A special case of this simplification feature is the evaluation of congruences with modulus equal to 1 f cong y x z 0 1 rlsimpl f gt true e Modulo reduction The coefficients of a PASF in congurence modulo m can be reduced to be not greater than m 1 After the application of this simplification rule all coefficients could vanish to zero f cong T xtb y 11 3 rlsimpl f gt x Qey 2 737 0 f cong 8 x 4 y 16 4 rlsimpl f gt true e Content elimination in atomic formulas Every atomic un equation can be done content free by dividing all the coefficients by their great est common divisor Similar simplification rule can be applied for the congruences In c
12. weg deus 30 input facilities 1 8 TO 11 integer factorization 20 21 InVefSQ ag esso Dead alee age oLb aS aes 9 inyol tive Bot 22l5 2 gerer seis 16 irreducible factors 13 14 irreducible factors list 13 irreducible factors multiplicity list 13 iterative tableau 23 L language Eee ERES RCRED E 5 27 language default 0 6 language selection 04 5 uud PEPTIDE 12 linear optimization 35 36 list of atomic formulas 13 list of irreducible factors 13 list Of terms cose crib steed bee 14 list s of variables 00 0 14 loading REDLOG 2e e 5 local quantifier elimination 35 M matrix of a formula 14 move quantifiers inside 28 multiple occurrences lusus 17 multiplicatively split atomic formula 16 17 18 19 20 21 multiplicity list of atomic formulas 13 multiplicity list of irreducible factors 13 multiplicity list of terms 14 N DegablOD iiid wr rrr ebbe ig 7 negation normal form 2T network analysis sss 3 34 pm n 27 Index non degeneracy conditions 34 non ordering inequalities 18 normal form 13 24 25 27 28 number of atomic formulas 13 O OFSF 2 3 4 5 8 10 11 1
13. 2h Mala theese tiacccaye die ned 25 rinzden s2 d EE EAE T 9 Ploptis 2nze enna et oe eee eae 36 rlpasfexpand 2 ciens 22 rlpa sfsimnplify 2 2 eas 22 LIposdenu cs o dst aenea Lee te 9 rlqedfS is RIS PE ERES 30 rlqegenct ce duiden ENERE ESA 35 rlqeleu E O EE ok 30 rlqepnf 5g cem eSI ias 31 rlgeq8S6 v ned ee RRISGAd Oe Sees he 30 IlqesdS6ocs sls sueta isTOWpes deas 30 Ilgestu ocenii e Eu nde sm 31 rlrealtime 2 1m X REREAUA 13 rlsiatadv usn deg 19 22 IISXChkE e6enecocleu e pe REI 17 IlsTeXplc si thike tiaan ss 17 IlSIZOXDl ee uae Aer denn 16 PUSTEAC 1 21 tobacco bly 2 Abe os 19 21 rlsij13d8m one tee tori dedaeatd 17 rlssmplocs tat ides hatin Se ee ae 13 EISXpd Pe ete ae are 19 PUSUPO esas 5 lane Sed aa ea 18 UST PW zis 24d cys Be E E e See Bizrate 18 EISISm epee Ma deu nieve t toe 17 ElS1805 2252 p shee ded neris a aa 17 TISPESQSP lois Boe ek Be ee ect 19 IISUSI cies eruere ien UA 28 ELUta8bID toate fede heni pie eie ia 28 rltnft o usquc ee ir EEEE 28 IlverfbosSG o cdd baled tale ode ee 13 T 30 ee 8 Switches and Variables References to Switches and Variables rlanuexdebu g 9n m t bes 33 rlanuexdifferentroots 33 rlanuexgcdnormalize 34 rlanuexpsremseq esses 33 rlanuexsgnopt cs b n 34 rlanuexverbose eese 33 rlcad see t9 ppeR PISIS coheed SS 31 rlcad ptoj si pe basa eed da 33 rlcad proja lways
14. 5 Chapter 7 References 39 Wei97 Volker Weispfenning Quantifier elimination for real algebra the quadratic case and beyond Applicable Algebra in Engi neering Communication and Computing 8 2 85 101 February 1997 Wei97a Volker Weispfenning Simulation and optimization by quantifier elimination Journal of Symbolic Computation 24 2 189 208 August 1997 Wei90 Volker Weispfenning The complexity of almost linear diophan tine problems Journal of Symbolic Computation 10 5 395 403 November 1990 Functions Functions Documentation of Functions All bce tears cea eee ads ma Pe ea aS ee ton Sede T ONG EE E EE EEE T T 88806 EA E E Mees d perit 10 B DpablilieniesseseeBeeesee TUEERREScHes 8 band 295 deep et eee rbuti eps 11 be quiy lex b ev RIDARS IM RUBRI it OX eck Sata heard tenes aes 8 binpl 5eel eei ERR te Se 11 bnOot c o paeRcxpei UTE Gg HR E Pe 11 Lot 11 replys iiaseeswee iraro roinaa cas 11 COUP P E 10 D PIPER 11 diXusiscecn e ag pe Rep RHENO EGG 10 E equal ie sis ci trece a rege 8 10 11 T i ia ta M T SK sth interes E A E shin T F POP cette eoa Red e roe Tu 11 Bed owes inca rage Mead d ertabai 8 10 Ereaterpcs o ge Ida Rr ER es 8 10 I 3mplo onseeeeciei up pu Mp iae T 40 L Length issue escriba de pee hA ER 12 lequcizeieeseertic iei we eg b ree 8 10 L SSP i seteear meee hg ep Eres 8 10 M kand ioe od chsh aid ccce inania ras 11 MKOR dio c Qh dws ie Giang eet
15. 5 16 17 20 26 29 30 31 35 36 optimization 2er eriten 35 36 ordered field luuuuusus 2 8 Ordering eei RR Le ERERSS 8 10 ordering constraint 18 ordering inequality 18 ordering relations 19 P p adie number riip eresi lady ede 2 5 p adic valuation esses sss 5 parametric denominator 9 10 parity decomposition 18 19 partial cylindrical algebraic decomposition p 29 PASE 2 vues ue Dues du S ning sean leaders 5 21 physical problems 34 PNE aiea ie eia esee Ebr Rep R Ei 28 polynomial reduction 24 25 positive head coefficient 17 20 power Of pi ivesies actdoedieedeeeen 20 predicates nse eae eee et 5 prefer orderings 18 prefer weak orderings 18 prenex normal form 28 31 primitive over the integers 17 20 projection order 32 protocol iinssBheseusisvadp emn 13 25 Q quadratic constraint esses 31 quadratic special case 30 quantifier 7 8 14 27 28 quantifier block eese seg oe eres 21 quantifier changes 28 quantifier elimination 8 29 30 31 34 35 quantifier free equivalent 29 31 R radical membership test 24 25 26 48 rational numbers lssu 9 real closed field
16. 9249 b dadeehed euches 35 36 context default 2e caren eR 6 context selection 20065 5 contexts available 0 2 contract atomic formulas 25 convenient relations 18 19 count atomic formulas 13 counterexample 000 30 GU ovg ri deemed Be ree es 27 31 DORSE 21 ceti pit i aki eed ae es 5 decision problem 30 31 decrease degree 26 29 decrease number of clauses 27 deeply nested formula 28 detault context 23d s oce rep 6 default language 6 degreascss ok opp eR ae PERO E 26 degree restriction 26 29 30 denominator pem 9 10 depth first search 30 derivatio 42 mE RR CU mE 11 discretely valued field 2 5 10 disj ncetlon nas rir saree we pedals T dt disjunctive normal form 24 27 28 divislblliby 2 oq es euttepbeR ERE eee 10 Index DNE s Leba mele areik errep ee 24 27 28 DVFSF 2 3 5 10 15 16 17 20 21 23 26 29 30 34 35 E elimination set lesse 29 GpsSilOn ebe p ee See ea 30 equal subformulas 16 17 CQUANION sete ted oe p teisiu IDE 8 10 11 equivalence eeses eese T evaluate atomic formulas 17 20 25 30 evaluate reduced form 25 existential closure 4 8 explode atomic formulas
17. Redlog User Manual A REDUCE Logic Package Edition 3 1 for REDLOG Version 3 06 REDUCE 3 8 24 November 2006 by A Dolzmann A Seidl and T Sturm Copyright 1995 2006 by A Dolzmann A Seidl and T Sturm Quickstart In case you hate long manuals and want to see something within a minute type reduce in the command line REDUCE should start up Type the four commands load redlog rlset ofsf phi ex x a x 2 b x 1 0 rlqe phi and hit return You will get a condition on the parameters a and b such that the quadratic polynomial a x 2 b x 1 has a real root Acknowledgments We acknowledge with pleasure the superb support by Herbert Melenk and Winfried Neun of the Konrad Zuse Zentrum fuer Informationstechnik Berlin Germany during this project Furthermore we wish to mention numerous valuable mathematical ideas contributed by Volker Weispfenning University of Passau Germany Redlog Home Page There is REDLOG home page maintained at http www fmi uni passau de redlog It contains information on REDLOG online versions of publications and a collection of examples that can be computed with REDLOG This site will also be used for providing update versions of REDLOG Support For mathematical and technical support contact redlogOfmi uni passau de Bug Reports and Comments Send bug reports and comments to redlogOfmi uni passau de Any hint or suggestion is welcome In particular we are interested in practic
18. a theory Function Groebner simplifier formula is a quantifier free formula Default for the ory is the empty theory 3 The functions differ in the boolean normal form that is computed at the beginning rlgsc computes a conjunc tive normal form rlgsd computes a disjunctive normal form and rlgsn heuristically decides for either a conjunctive or a disjunctive normal form depending on the structure of formula After computing the correspond ing normal form the formula is simplified using Groebner simplification techniques The returned formula is equivalent to the input formula wrt 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 0Oandz 0 rlgsc x neq O or y neq O or x 242 x y lt 0 and z neq O or x 3 z 0 gt x lt gt 0 orz lt gt 0 The heuristic used by rlgsn is intended to find the smaller boolean nor mal form among CNF an DNF Note that anyway the simplification of the smaller normal form can lead to a larger final result than that of the larger one The Groebner simplifiers use 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 order between the variables are applied The other switches and variables of the Groebner package are not controlled by the Groebner simplifier They can be adjusted by the user In contrast to the standard simplifier rlsimp1 see Section 4 1 Standard
19. ailable on http www fmi uni passau de redlog George E Collins and Hoon Hong Partial cylindrical algebraic decomposition for quantifier elimination Journal of Symbolic Computation 12 3 299 328 September 1991 Andreas Dolzmann Solving Geometric Problems with Real Quantifier Elimination Technical Report MIP 9903 FMI Uni versitaet Passau D 94030 Passau Germany January 1999 Andreas Dolzmann Oliver Gloor and Thomas Sturm Ap proaches to parallel quantifier elimination In Oliver Gloor edi tor Proceedings of the 1998 International Symposium on Sym bolic and Algebraic Computation ISSAC 98 pages 88 95 Ro stock Germany August 1998 ACM ACM Press New York Andreas Dolzmann and Thomas Sturm Simplification of quantifier free formulae over ordered fields Journal of Symbolic Computation 24 2 209 231 August 1997 Andreas Dolzmann and Thomas Sturm Redlog Computer al gebra meets computer logic ACM SIGSAM Bulletin 31 2 2 9 June 1997 Andreas Dolzmann and Thomas Sturm Guarded expressions in practice In Wolfgang W Kuechlin editor Proceedings of the 1997 International Symposium on Symbolic and Algebraic Computation ISSAC 97 pages 376 383 New York July 1997 ACM ACM Press Andreas Dolzmann and Thomas Sturm P adic constraint solv ing Technical Report MIP 9901 FMI Universitaet Passau D 94030 Passau Germany January 1999 To appear in the pro ceedings of the ISSAC 99 Andreas Dolzmann Tho
20. al problems to the solution of which REDLOG has contributed Chapter 1 Introduction 2 1 Introduction 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 This document serves as a user guide describing the usage of REDLOG from the algebraic mode of REDUCE For a detailed description of the system design see DS97a An overview on some of the application areas of REDLOG is given in DSW98 See also Chapter 7 References page 37 for articles on REDLOG applications 1 1 Contexts REDLOG is designed for working with several languages and theories in the sense of first order logic Both a language and a theory make up a context In addition a context determines the internal representation of terms There are the following contexts available OFSF OF stands for ordered fields which is a little imprecise The quantifier elimination actually requires the more restricted class of real closed fields while most of the tool like algorithms are generally correct for ordered fields One usually has in mind real numbers with ordering when using OFSF DVFSF Discretely valued fields This is for computing with formulas over classes of p adic valued extension fields of the rationals usually the fields of p adic numbers for some prime p ACFSF Algebraical
21. aluation of variable free atomic formulas to truth values Make the left hand sides primitive over the integers with positive head coefficient Replace left hand sides of atomic formulas by their squarefree parts switch rlsiatdv see Section 4 1 4 OFSF specific Standard Simplifier Switches page 18 Optionally perform factorization of equations and inequalities switch rlsifac see Section 4 1 4 OFSF specific Standard Simplifier Switches page 18 switches rlsiexpl and rlsiexpla see Section 4 1 2 General Standard Simplifier Switches page 16 For details see the description of the simplification for ordered fields in DS97 This can be easily adapted to algebraically closed fields 4 1 6 ACFSF specific Standard Simplifier Switches The switches rlsiatadv and rlsifac have the same effects as in the OFSF context see Section 4 1 4 OFSF specific Standard Simplifier Switches page 18 4 1 7 DVFSF specific Simplifications In the DVFSF case the atomic formula simplification includes the following Evaluation of variable free atomic formulas to truth values provided that p is known Equations and inequalities can be treated as in ACFSF see Section 4 1 5 ACFSF specific Simplifications page 19 Moreover powers of p can be cancelled With valuation relations the GCD of both sides is cancelled and added appropriately as an equation or inequality Valuation relations involving zero sides can be evaluated or at least tur
22. apnf formula Function Anti prenex normal form Returns a formula equivalent to formula where all quantifiers are moved to the inside as far as possible rlapnf ex x all y x 0 or y 0 and x z ex x x 0 or all y y 0 and ex x x z 0 rltnf formula terml Function Term normal form term is a list of terms This combines DNF computa tion with tableau ideas see Section 4 2 Tableau Simplifier page 23 A typical choice for terml is rlterml formula If the switch rltnft is off then 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 Quantifier Elimination and Variants 29 6 Quantifier Elimination and Variants Quantifier elimination computes quantifier free equivalents for given first order formulas For OFSF there are two methods available 1 Virtual substitution based on elimination set ideas Wei88 This imple mentation is restricted to at most quadratic occurrences of the quanti fied variables but includes numerous heuristic strategies for coping with higher degrees See LW93 Wei97 for details of the method 2 Partial cylindrical algebraic decomposition CAD introduced by Collins and Hong CH91 There are no degree restrictions with CAD For DVFSF we use the virtual substitution method that is also available for OFSF Here the implementation is restricted to linear occur
23. ar ity decompositions switch rlsipd and factorization of equations and inequalities switch rlsifac are enabled rlsitsqspl Switch Simplify split trivial square sum This is on by default It is ignored with rlsiadv off Trivial square sums are split additively depending on rlsiexpl and rlsiexpla see Section 4 1 2 General Standard Simplifier Switches page 16 rlsimpl a 2 b 2 gt 0 gt a lt gt 0 or b lt gt 0 rlsipd Switch Simplify parity decomposition By default this switch is on It is ignored with rlsiatadv off 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 rlsimpl f 3 2 a ta a 1 gt 0 The atomic formula is possibly split into two parts according to the set ting of the switches rlsiexpl and rlsiexpla see Section 4 1 2 General Standard Simplifier Switches page 16 rlsifac Switch Simplify factorization By default this switch is on It is ignored with rlsiatadv off Splits equations and inequalities via factorization of their left hand side terms into a disjunction or a conjunction respectively This is done in dependence on rlsiexpl and rlsiexpla see Section 4 1 2 General Standard Simplifier Switches page 16 4 1 5 ACFSF specific Simplifications In the ACFSF case the atomic formula simplification includes the following Chapter 4 Simplification 20 Ev
24. are eliminated For this outermost block the constructive information obtained by the elimination is saved Chapter 6 Quantifier Elimination and Variants 30 e In case the considered block is existential for each evaluation of the free variables we know the following Whenever a condition holds then 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 condition is false then formula is false and the solution is one possible counterexam ple As an example we show how to find conditions and solutions for a system of two linear constraints rlqea ex x x b1 gt 0 and a2 x b2 lt 0 2 b2 a2 b1 a2 b2 gt 0 and a2 lt gt 0 x a2 a2 lt 0 or a2 0 and b2 lt 0 x infinity1 The answer can contain constants named infinity or epsilon both indexed 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 rlqea is not available in the context ACFSF rlqeqsc Switch rlqesqsc Switch Quantifier elimination super quadratic special case By default these switches are off They are relevant
25. ase of inequalities even more simplification can be done f 3 x 6 y 9 0 rlsimpl f Chapter 4 Simplification 22 gt x 2 y 3 0 f 3 x 6 y 7 lt 0 rlsimpl f gt x 2 y 2 lt 0 f cong 3 x 6 y 3 0 9 rlsimpl f gt x 2 y 157 0 3 e In certain cases we can simplify un equations and in congruences to truth values These simplification rules due to their non triviality are referred to as the advanced simplification rules f 3 k 1 0 rlsimpl f false Beyond atomic formulas simplification was extended to care for bounded quantifiers e PASF provides a simplification procedure for bounds using their special properties e Bounds that can t be satisfied bounds with single satisfaction value and bounds with trivial matrix are transformed into equivalent unbounded formulas reducing the total formula length e Suitable atomic formulas in the matrix of a bounded quantifier that contain the bounded variable are moved inside the bound e Information from the bound is used to expand the implicit theory for the matrix simplification 4 1 10 PASF specific Standard Simplifier Switches rlpasfsimplify Switch Simplifies the output formula after the elimination of each quantifier By default this switch is on rlpasfexpand Switch Expands the output formula with bounded quantifiers after the elimi nation of each quantifier This switch is off by default due to immense overhead of the expansion
26. bles of f The return value is a list 1 f is a formula and 1 is a list v d where v is from varlist and d is an integer f has been obtained from formula by substituting v for v d The sign conditions necessary with the OFSF context are not generated automatically but have to be constructed by hand for the variables v with even degree d in 1 rldecdeg1 m x 4711 b 8 gt 0 b x gt ib mex gt 0 x 4711 b 8 Chapter 5 Normal Forms 27 5 Normal Forms 5 1 Boolean Normal Forms For computing small boolean normal forms see also the documentation of the procedures rlgsc and rlgsd Section 4 3 Groebner Simplifier page 23 rlcnf formula Function Conjunctive normal form formula is a quantifier free formula Returns a conjunctive normal form of formula rlcnf a 0 and b 0 or b 0 and c 0 gt a 0 or c 0 andb 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 gt a 0 and c 0 or b 0 or c 0 0 rlbnfsm Switch Boolean normal form smart By default this switch is off If on simplifier recognized implication DS97 is applied by rlcnf and rldnf This leads to smaller normal forms but is considerably time consuming rlbnfsac Fix Switch Boolean normal forms subsumption and cut By default this switch is on With boolean normal form computation subsumptio
27. bstitution list s1 contains all substitutions 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 v1 x y v2 x v3 y rlifstruct formula kernel Function Irreducible factor structure of a formula kernel is v by default Returns a list 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 substitutions to obtain formula from f rlstruct x y 0 and x 0 or y gt 0 v gt vi v2 0 and vi 0 or v2 gt 0 v1 x v2 y rlmatrix formula Function Matrix computation Drops all leading quantifiers from formula Chapter 4 Simplification 15 4 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 that focus mainly on reducing the size of the given for mula The standard simplifier tableau simplifiers and Groebner simplifiers The OFSF versions of these are described in DS97 The ACFSF versions are the same as the OFSF versions except for tech niques that are particular to ordered fields such as treatment of square sums in connection with ordering relations For DVFSF there is no Groebner simplifier available The parts of the stan dard simplifier that are particular to valued fields are described i
28. c Computation Modelling and Applied Mathematics IMACS 97 pages 727 732 Berlin August 1997 IMACS Wis senschaft amp Technik Verlag Thomas Sturm and Volker Weispfenning Computational ge ometry problems in Redlog In Dongming Wang editor Auto mated Deduction in Geometry volume 1360 of Lecture Notes in Artificial Intelligence Subseries of LNCS pages 58 86 Springer Verlag Berlin Heidelberg 1998 Thomas Sturm and Volker Weispfenning An algebraic approach to offsetting and blending of solids Technical Report MIP 9804 FMI Universitaet Passau D 94030 Passau Germany May 1998 Volker Weispfenning The complexity of linear problems in fields Journal of Symbolic Computation 5 1 3 27 February 1988 Volker Weispfenning Comprehensive Groebner Bases Journal of Symbolic Computation 14 1 29 July 1992 Volker Weispfenning Parametric linear and quadratic optimiza tion by elimination Technical Report MIP 9404 FMI Univer sitaet Passau D 94030 Passau Germany April 1994 Volker Weispfenning Quantifier elimination for real algebra the cubic case In Proceedings 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 In J Fleischer et al editors Computer Algebra in Science and Engineering pages 163 179 World Scientific Singapore 199
29. cce ue 33 rl adbaseonly 2 22 pnia 32 rlcaddebug 4 4o Eden 33 rlcadextonly ii pic 2 re es 32 rlcadfacc eR irei POSS sertis 32 rlcadfulldimonly 2 Re 32 rlcadguessauto ss 32 rlcadhongpr e ovr ea 33 rlcadisoallroOtsS eri or 33 rl adparti alzni z iiv we JG edere 32 rl adpordeE 2262 5 38 94 Deas 32 rl adpr jonly 4 iersmelftewfBensdes 32 rlcadrawformula 32 39 rlcadte ii b as baled Pees 32 rlcadtrimtre6 eg e 32 rlcadyerbo8Se 2i need Eres 33 rldeflangl iili IRE eed 6 IlgSprOd ve cae Fie ekes bae 24 rlgsrad ee rere b EES annis 26 DU PSL is onde Gi shia dees PRESE g 24 44 PIGSSUD i erini bites ead tabs hoe a 24 Ilgsutord cezsrelsreredo kae due 26 flhqessenieseiorceednnsiienb er pns 34 r lnzden conber ku eg ut RP nh Es 9 flposden o bee Peete nied 9 10 rlqedfs ede I ERE RER AS 30 rlqeheu ek ism Rr Rx 30 rlqepnf z ell 9 e rr Ret 31 rldeq86 c hd RR ae EIE UE 29 rlqe8d86 ii s Rd RP 29 IlSiadv voee ern 19 rlsSiat dv is ekoi aitete 19 20 21 rlsiatdv 6 gees este Saves ees ee 18 20 rlsSichDk op ecg bois aa nd adde rens 16 IlSiexpl eererens 15 18 19 20 21 rlsiexpla 15 16 17 18 19 20 21 IlSifaC 4 03 ae eats eects 18 19 20 21 rlsiide e oiei ern nrakane ix dae dg ave 16 TISIMP 3c 2 oi pha dac sane Gels eder ens 15 TISXYDd c ee odes de eran as 16 17 18 19 PUSASM 2 4 5 aya ce s deserts uno
30. dard Simplifier page 15 to certain REDLOG procedures Optionally the system can be forced to add them to the formula at the input stage rladdcond Switch Add condition This is off by default With rladdcond on non zeroness and positivity assumptions made due to the switches rlnzden and rlposden are added to the formula at the input stage With rladdcond and rlposden on we get for instance a b c 0 and a d c gt 0 b lt gt 0 and a b c 0 and d gt O and a c d gt 0 Chapter 3 Format and Handling of Formulas 10 3 4 DVFSF Operators Discretely valued fields are implemented as a one sorted language using the operators and which encode lt and in the value group respectively For details see Wei88 Stu00 or DS99 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 l and respectively Integer reciprocals in the input are resolved correctly DVFSF allows the input of chains in analogy to OFSF See Section 3 3 OFSF Operators page 8 for details With the DVFSF operators there is no treatment of parametric denomi nators available 3 5 ACFSF Operators equal Binary Infix operator neq Binary Infix operator The above operators may also be written as lt gt As for OFSF it i
31. ding REDLOG and selecting a context see Chapter 2 Loading and Context Selection page 5 there are first order formulas available as an additional type of symbolic expressions That is formulas are now subject to symbolic manipulation in the same way as say polynomials or matrices in conventional systems There is nothing changed in the behavior of the builtin facilities and of other packages 3 1 First order Operators Though the operators and or and not are already sufficient for representing 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 See Section 3 9 Extended Built in Commands page 11 for the descrip tion of extended for loop actions that allow to comfortably input large sys tematic conjunctions and disjunctions REDUCE expects the user to know about the precedence of and over or In analogy to and there are thus no parentheses output around conjunctions within disjunctions The following switch causes such subformulas to be bracketed anyway See Section 1 3 Conventions page 4 for the notion of a fix switch rlbrop Fix Switch Bracket all operators By default this switch is on wh
32. e 34 6 3 Local Quantifier Elimination 000 c cece eee eee 35 6 4 Linear Optimization 0 00 0 0 cece ehh 35 7 References 04 6 oSb os oe hs EE EUER oe Se aT PURCHIONS a sectes 1369 dann D Ud e ERE ADR R COR be es ea 40 Documentation of Functions 00 000 c cece cece ee eee eens 40 References to Functions 0 0000 cece cece e 41 Switches and Variables 2492 RR mn 43 Documentation of Switches and Variables lssss ess 43 References to Switches and Variables 0 00000 cece eeeeee 44 Data Structures s id rue IRIGRe4A ER 3 YER 45 Documentation of Data Structures 00 0 c eee cee eee ees 45 References to Data Structures lile 45
33. e ned cwn 15 D Normal PORUSaa 9 see ess P AUGE ord iene oe RP Y x des 27 6 Quantifier Elimination and Variants 200 00 n 29 T R fere c s eses diners we d oe Ws ee a ae Bw wie we E a 37 F nctionS c Pr D PT 40 Switches and Variables uuu o ad menada oc e ERU oe hoe 43 BOUT NIRE TIS ER S E ES T ILI EI i 111 151 45 ii Table of Contents Lh JIHPOXOHGl O los essea a ota E n a eE a OE m 2 l l Contexts costes ree be ee Reg Erw us e E RR EE Ea RE 2 II ENS uc DEPT TrIDLC 2 1 9 Conventions ien eise op e repaired doe i ete 4 2 Loading and Context Selection 9 2 1 Loading Redlog 0 cece omini iE tte eee 5 2 2 Context Selection ele ds nee ge tee ones eei eee Ree das 5 3 Format and Handling of Formulas 7 3 1 First order Operators ese dead aeea ge ada ieseee Phos EE 7 3 2 ClOSUreS 4 5 leere eR re eee ae dae CREER Renee eas 8 3 3 OFSF Operators cse segete into Rote doe Ri c ei eee eee 8 3 4 DVFSF Operators sesseeeeesee mn 10 3 0 ACESSE Operators 322 uin mel a te EEG RES Pa ORE d 10 3 0 PASE Operators 4s eee gd aod ed ea Eb Po nb e ee 10 3 7 IBALP Operators sooie niao aiiai a ie ehh 11 3 8 DCESF Oper8tOrs i222mc 4e raiat eb eb EA er E e A 11 3 9 Extended Built in Commands 0 0c eee eee eee i 3 10 Global Switches 4i ese sersa Sandee Reb ep wees gg 12 3 11 Basic Functions on Formulas 0 0 000 e eee eee 13 4 Sim
34. ft hand sides of equiations in suggestedpoint For restrictions and options compare rlge see Section 6 1 Quantifier Elim ination page 29 6 4 Linear Optimization In the context OFSF there is a linear optimization method implemented which uses quantifier elimination see Section 6 1 Quantifier Elimination page 29 encoding the target function by an additional constraint includ ing a dummy variable This optimization technique has been described in Wei94a rlopt constraints target Function Linear optimization rlopt is available only in OFSF constraints is a list of parameter free atomic formulas built with lt or gt target is a Chapter 6 Quantifier Elimination and Variants 36 polynomial over the rationals target is minimized subject to constraints 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 takes this value The point list does however not contain all such points For unbound problems the result is infinity rloptis Switch Optimization one solution This is off by default rloptis is relevant only for OFSF If on rlopt returns at most one solution point Chapter 7 References 37 7 References CH91 Dol99 DGS98 DS97 DS97a DS97b DS99 DSW98 DSW98a DW00 Most of the references listed here are av
35. g 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 Turning on rlsipw will instead yield the following rlsimpl a lt gt 0 and a gt 0 or b 0 a lt gt 0 and a gt 0 or b 0 Here we meet the simplification goal of convenient relations when strict orderings are considered inconvenient rlsipo Switch Simplification prefer orderings Prefers orderings in contrast to inequal ities with implicit 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 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 4 Simplification 19 Here we meet the simplification goal of convenient relations when order ings are considered inconvenient rlsiatadv Switch Simplify atomic formulas advanced By default this switch is on En ables sophisticated atomic formula simplifications based on squarefree part computations and recognition of 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 Furthermore splitting of trivial square sums switch rlsitsqspl p
36. hapter 4 Simplification 18 e Evaluation of trivial square sums to truth values switch rlsisqf see Section 4 1 4 OFSF specific Standard Simplifier Switches page 18 Additive splitting of trivial square sums switch rlsitsqspl see Sec tion 4 1 4 OFSF specific Standard Simplifier Switches page 18 e In ordering inequalities perform parity decomposition similar to squarefree decomposition of terms switch rlsipd see Section 4 1 4 OFSF specific Standard Simplifier Switches page 18 with the option to split an atomic formula multiplicatively into two simpler ones switches rlsiexpl and rlsiexpla see Section 4 1 2 General Standard Simplifier Switches page 16 e In equations and non ordering inequalities replace left hand sides by their squarefree parts switch rlsiatdv see Section 4 1 4 OFSF specific Standard Simplifier Switches page 18 Optionally per form factorization of equations and inequalities switch rlsifac see Section 4 1 4 OFSF specific Standard Simplifier Switches page 18 switches rlsiexpl and rlsiexpla see Section 4 1 2 General Standard Simplifier Switches page 16 For further details on the simplification in ordered fields see the article DS97 4 1 4 OFSF specific Standard Simplifier Switches rlsipw Switch Simplification prefer weak orderings Prefers weak orderings in contrast to strict orderings with implicit theory simplification rlsipw is off by default which leads to the followin
37. ich causes some private printing routines to be called for formulas All subformulas are bracketed completely making the output more readable Besides the boolean operators introduced above first order logic includes the well known existential quantifiers and universal quantifiers 3 and V 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 list is expanded into several nested quantifiers Chapter 3 Format and Handling of Formulas 8 See Section 3 2 Closures page 8 for automatically quantifying all vari ables except for an exclusion list bex Binary Operator ball Binary Operator These are the bounded quantifiers The first argument is the quantified variable the second one is the bound and the third one is the matrix formula A bound is a quantifier free formula which contains only one variable and defines a finite set Formulas with bounded quantifiers are only available in PASF For convenience we also have boolean constants for the truth values true Variable false Variable These algebraic mode variables are reserved They serve as truth values 3 2 Closures rlall formula exceptionlist Function Universal closure exceptionlist is a list of variables empty by default Returns formula with all free variables universally quant
38. ified except for those in exceptionlist 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 3 3 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 such as division in the language of ordered fields Note that the OFSF quantifier elimination pro cedures see Chapter 6 Quantifier Elimination and Variants page 29 for non linear formulas actually operate over real closed fields See Section 1 1 Contexts page 2 and Section 2 2 Context Selection page 5 for details on contexts equal Binary Infix operator neq Binary Infix operator leq Binary Infix operator lessp Binary Infix operator greaterp Binary Infix operator 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 geq sed Infix T Chapter 3 Format and Handling of Formulas 9 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 0 and b c
39. ion Automatic tableau method Tableau steps wrt a case distinction over the signs of all terms occurring in formula are computed 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 corresponding next tableau step is not applied to the last tableau result but independently to each single branch The iteration stops when the obtained formula is not smaller than the corresponding input 4 3 Groebner Simplifier The Groebner simplifier is not available in the DVFSF context It consid ers order theoretical and algebraic simplification rules between the atomic formulas of the input formula Currently the Groebner simplifier is not Chapter 4 Simplification 24 idempotent The name is derived from the main mathematical tool 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 formula theory Function rlgsd formula theory Function rlgsn formul
40. is simplified with rldnf rlcadisoallroots Advanced Switch Isolate all roots This is off by default Turning this switch on allows to find out how much time is consumed more without incremental root isolation rlcadaproj Advanced Switch rlcadaprojalways Advanced Switch Augmented projection always By default rlcadaproj is turned on and rlcadaprojalways is turned off If rlcadaproj is turned off no augmented projection is performed Otherwerwise if turned on aug mented projection is performed always if rlcadaprojalways is turned on or just for the free variable space rlcadaprojalways turned off rlcadhongproj Switch Hong projection This is on by default If turned on Hong s improvement for the projection operator is used rlcadverbose Switch Verbose This is off by default With rladverbose on additional verbose information is displayed rlcaddebug Switch Debug This is turned off by default Performes a self test at several places if turned on rlanuexverbose Advanced Switch Verbose This is off by default With ranuexverbose on additional verbose information is displayed Not of much importance any more rlanuexdifferentroots Advanced Switch Different roots Unused for the moment and maybe redundant soon rlanuexdebug Switch Debug This is off by default Performes a self test at several places if turned on rlanuexpsremseq Switch Pseudo remainder sequences This is turned off by defaul
41. ity list of atomic formulas Returns the atomic formulas con tained 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 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 3 Format and Handling of Formulas 14 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 rlvarl formula Function Variable lists Returns both the list of variables occurring freely and that of the variables occurring boundly in formula in a two element list Notice that the two member lists are not necessarily disjoint rlfvarl formula Function Free variable list Returns the variables occurring freely in formula as a list rlbvarl formula Function Bound variable list Returns the variables occurring boundly in formula as a list rlstruct formula kernel Function Structure of a formula kernel is v by default Returns a list f s1 f is constructed from formula by replacing each occurrence of a term with a kernel constructed by concatenating a number to kernel The su
42. la by iteratively making formula anti prenex see Section 5 2 Miscellaneous Normal Forms page 27 and elim inating one quantifier rlqews formula theory Function Quantifier elimination by virtual substitution 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 innermost block moving it inside as far as possible and then eliminating it rlqews is not available in ACFSF 6 1 2 Cylindrical Algebraic Decomposition rlcad formula Function Cylindrical algebraic decomposition Returns a quantifier free equivalent of formula Works only in context OFSF There are no degree restrictions on formula Chapter 6 Quantifier Elimination and Variants 32 rlcadporder formula Function Efficient projection order Returns a list of variables The first variable is eliminated first rlcadguessauto formula Function Guess the size of a full CAD wrt the projection order the system would actually choose The resulting value gives quickly an idea on how big the order of magnitude of the size of a full CAD is rlcadfac Advanced Switch Factorisation This is on by default rlcadbaseonly Switch Base phase only Turned off by default rlcadprojonly Switch Projection phase only Turned off by default rlcadextonly Switch Extension phase only Turned off by default rlcadpartial Switch Partial CAD This is turned on by defa
43. le contexts 0 00000 2 B Boolean and ror ea 11 boolean constant sseeessss 8 Boolean equivalence ss 11 Boolean implication 11 boolean normal form 24 25 27 Boolean not 0 eee esse eens 11 boolean operator 0000 7 Boolean OF s ose sc dsedie ene a e reati aaki oe 11 Boolean replication 11 bound variables lusus 14 bounded quantifers 22 bounded quantifier 8 loctd c C PRI EE 1 branch wise tableau iteration 23 breadth first search 0 30 DUE TOpOTU xut eEbRSEREF IH e ERIS 1 C QAD d b e pbePRArab PR PT 29 cancel COD oi RehLinbeivh i eda ean 20 46 cancel powers of p 00005 20 canonical ordering 16 case distinction 0 00 25 oci m P EE EET 3 29 chains of binary relations 9 10 chains of binary relations in the input Em Li change boolean structure 28 clos reiiilccSteeerie Bp ReesteP e ees 8 ONE P 24 27 complex numbers lesse 2 complex theory ss esses 35 complexity of terms 25 35 comprehensive Groebner basis 29 comprehensive Groebner Basis 3 29 condition solution pairs 29 CONGTUENCC Rs rs ie hese EVE 10 congunction ied ERR REESE Tu conjunctive normal form 24 27 consiraint o 2
44. lqepnf Advanced Switch Quantifier elimination compute prenex normal form By default this switch is on which causes that rlpnf see Section 5 2 Miscellaneous Nor mal Forms page 27 is applied to formula before starting the elimination process If the argument formula to rlqe rlqea or rlgqe rlggea see Section 6 2 Generic Quantifier Elimination page 34 is already prenex this switch can be turned off This may be useful with formulas con taining equiv since rlpnf applies rlnnf see Section 5 2 Miscellaneous Normal Forms page 27 and resolving equivalences can double the size of a formula rlqepnf is ignored in ACFSF since NNF is necessary for elimination there rlqesr Fix Switch Quantifier elimination separate roots This is off by default It is relevant only in OFSF for rlge rlgqe and for all but the outermost quantifier block in rlqea rlgqea For rlqea and rlgqea see Section 6 2 Generic Quantifier Elimination page 34 It affects the technique for substituting the 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 method rlge has turned out superior rlqeipo formula theory Function Quantifier elimination by virtual substitution in position Returns a quantifier free equivalent to formu
45. lt 0 and c d gt O and d f 0 Here only adjacent terms are related to each other Though we use the language of ordered rings the input of integer re ciprocals is allowed and treated correctly interpreting them as constants for rational numbers There are two switches that allow to input arbitrary re ciprocals which are then resolved into proper formulas in various reasonable ways The user is welcome to experiment with switches like the following which are not marked as fiz switches See Section 1 3 Conventions page 4 for the classification of REDLOG switches rlnzden Switch rlposden Switch Non zero positive denominators Both switches are off by default If both rlnzden and rlposden are on the latter is active Activating one of them allows the input of reciprocal terms With rlnzden on these terms are assumed to be non zero and resolved by multiplication When occurring with ordering relations the reciprocals are resolved by multiplication with their square preserving the sign a b c 0 and a d c gt 0 2 a b c 0 and a d ctd gt 0 Turning rlposden on guarantees the reciprocals to be strictly positive which allows simple i e non square multiplication also with ordering relations a b c 0 and a d c gt 0 gt at b c 0 and a c d gt 0 The non zeroness or positivity assumptions made by using the above switches can be stored in a variable and then later be passed as a theory see Section 4 1 Stan
46. ly closed fields such as the complex numbers PASF Presburger Arithmetic i e the linear theory of integers with congruences modulo m for m gt 1 IBALP Initial Boolean algebras basically quantified propositional logic DCFSF Differentially closed fields according to Robinson There is no natural example The quantifier elimination is an optimized version of the procedure by Seidenberg 1956 The trailing sF stands for standard form which is the representation chosen for the terms within the implementation Accordingly LP stands for Lisp prefix See Section 2 2 Context Selection page 5 for details on selecting REDLOG contexts 1 2 Overview REDLOG origins from the implementation of quantifier elimination proce dures Successfully applying such methods to both academic and real world Chapter 1 Introduction 3 problems the authors have developed over the time a large set of formula manipulating tools many of which are meanwhile interesting in their own right e Numerous tools for comfortably inputing decomposing and analyzing formulas This includes for instance the construction of systematic formulas via for loops and the extension of built in commands such as sub or part See Chapter 3 Format and Handling of Formulas page 7 e Several techniques for the simplification of formulas The simplifiers do not only operate on the boolean structure of the formulas but also discover algebraic relationships For thi
47. mas Sturm and Volker Weispfenning A new approach for automatic theorem proving in real geome try Journal of Automated Reasoning 21 3 357 380 December 1998 Andreas Dolzmann Thomas Sturm and Volker Weispfenning Real quantifier elimination in practice In B H Matzat G M Greuel and G Hiss editors Algorithmic Algebra and Number Theory pages 221 248 Springer Berlin 1998 Andreas Dolzmann and Volker Weispfenning Local Quantifier Elimination In Carlo Traverso editor Proceedings of the 2000 Chapter 7 LW93 Stu97 Stu00 SW97al SW98 SW98a Wei88 Wei92 Wei94a Wei94b Wei95 References 38 International Symposium on Symbolic and Algebraic Compu tation ISSAC 00 pages 86 94 St Andrews Scotland August 2000 ACM ACM Press New York 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 Reasoning over networks by symbolic methods Technical Report MIP 9719 FMI Universitaet Passau D 94030 Passau Germany December 1997 To appear in AAECC Thomas Sturm Linear problems in valued fields Journal of Symbolic Computation 30 2 207 219 August 2000 Thomas Sturm and Volker Weispfenning Rounding and blend ing of solids by a real elimination method In Achim Sydow editor Proceedings of the 15th IMACS World Congress on Scientifi
48. ment For passing a variable list to torder note that rlgsradmemv is used as the tag variable for radical membership tests Chapter 4 Simplification 26 rlgsradmemv Fluid Radical membership test variable This fluid contains the tag variable used for the radical membership test with switch rlgsrad on It can be used to pass the variable explicitly to torder with switch rlgsutord on 4 4 Degree Decreaser The quantifier elimination procedures of REDLOG see Section 6 1 Quan tifier Elimination page 29 obey certain degree restrictions on the bound variables For this reason there are degree decreasing simplifiers available which are automatically applied by the corresponding quantifier elimination procedures There is no degree decreaser for the DVFSF context available rldecdeg formula Function Decrease degrees Returns a formula equivalent to formula hopefully decreasing the degrees of the bound variables In the OFSF context there are in general some sign conditions on the variables added which slightly increases the number of contained atomic formulas rldecdeg ex b x m x 4711 b 8 gt 0 ex b b gt 0 and ex x b mtx gt 0 rldecdeg1 formula varlist Function Decrease degrees subroutine This provides a low level entry point to the degree decreaser The variables to be decreased are not determined by regarding quantifiers but are explicitly given by varlist where the empty varlist selects all free varia
49. ment of atomic subformulas by simpler equivalents These equivalents are not necessarily atomic switches rlsiexpl rlsiexpla see Section 4 1 2 General Standard Simplifier Switches page 16 Chapter 4 Simplification 16 For details on the simplification on the atomic formula level see Section 4 1 3 OFSF specific Simplifications page 17 Section 4 1 5 ACFSF specific Simplifications page 19 and Section 4 1 7 DVFSF specific Simplifications page 20 e Proper treatment of truth values e Flattening nested n ary operator levels and resolving involutive appli cations of not e Dropping not operator with atomic formula arguments by changing the relation of the atomic formula appropriately The languages of all contexts allow to do so e Changing repl to impl e Producing a canonical ordering among the atomic formulas on a given level switch rlsisort see Section 4 1 2 General Standard Simplifier Switches page 16 e Recognizing equal subformulas on a given level switch rlsichk see Section 4 1 2 General Standard Simplifier Switches page 16 e Passing down information that is collected during recursion switches rlsism rlsiidem see Section 4 1 2 General Standard Simplifier Switches page 16 The technique of implicit theories used for this is described in detail in DS97 for orsF ACFSF and in DS99 for pvrsF e Considering interaction of atomic formulas on the same level and in teraction with information inhe
50. n DS99 The tableau simplification is straightforwardly derived from the smart sim plifications described there In PASF only the standard simplifier is available Besides reducing the size of formulas it is a reasonable simplification goal to reduce the degree of the quantified variables Our method of de creasing the degree of quantified variables is described for OFSF in DSW98 A suitable variant is available also in ACFSF but not in DVFSF 4 1 Standard Simplifier The Standard Simplifier is a fast simplification algorithm that is frequently called internally by other REDLOG algorithms It can be applied automat ically at the expression evaluation stage by turning on the switch rlsimpl see Section 3 10 Global Switches page 12 theory Data Structure A list of atomic formulas assumed to hold rlsimpl formula theory Function Simplify formula is simplified recursively such that the result is equiva lent under the assumption that theory holds Default for theory is the empty theory Theory inconsistency may but need not be detected by rlsimpl If theory is detected to be inconsistent a corresponding error is raised Note that under an inconsistent theory any formula is equivalent to the input i e the result is meaningless theory should thus be chosen carefully 4 1 1 General Features of the Standard Simplifier The standard simplifier rlsimp1 includes the following features common to all contexts e Replace
51. n and cut strategies are applied by rlcnf and rldnf to decrease the number of clauses We give an example rldnf x 0 and y 0 or x 0 and y 0 or x 0 and y lt gt 0 and z 0 gt x 0 and y lt gt 0 5 2 Miscellaneous Normal Forms rlnnf formula Function Negation normal form Returns a negation normal form of formula This is an and or combination of atomic formulas Note that in all contexts we use languages such that all negations can be encoded by relations see Chapter 3 Format and Handling of Formulas page 7 We give an example rinnf a 0 equiv b gt 0 a 0 and b gt 0 or a lt gt O0 and b lt 0 rlnnf accepts formulas containing quantifiers but it does not eliminate quantifiers Chapter 5 Normal Forms 28 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 quanti fiers to the outside When formula contains two quantifiers with the same variable such as in Je s D A sees 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 xi lt gt 0 rl
52. ned into equations or inequalities For concrete p integer coefficients with valuation relations can be re placed by a power of p on one side of the relation For unspecified p polynomials in p can often be replaced by one mono mial For unspecified p valuation relations containing a monomial in p on one side and an integer on the other side can be transformed into z 1 or z 1 where z is an integer For details on simplification in p adic fields see the article DS99 Atomic formulas of the form z 1 or z 1 where z is an integer can be split into several ones via integer factorization This simplification is often reasonable on final results It explicitly discovers those primes p for which the formula holds There is a special function for this simplification Chapter 4 Simplification 21 rlexplats formula Function Explode atomic formulas Factorize atomic formulas of the form z 1 or z 1 where z is an integer rlexplats obeys the switches rlsiexpla and rlsiexpl see Section 4 1 2 General Standard Simplifier Switches page 16 but not rlsifac see Section 4 1 8 DVFSF specific Standard Simplifier Switches page 21 4 1 8 DVFSF specific Standard Simplifier Switches The context DVFSF knows no special simplifier switches and ignores the gen eral switches rlsiexpla and rlsiexpl see Section 4 1 2 General Standard Simplifier Switches page 16 It behaves like rlsiexpla on The simplifier contains numerous
53. of theory adding only inequali ties and f is a quantifier free formula equivalent to formula assuming th The added inequalities contain neither bound variables nor variables from exceptionlist For restrictions and options compare rlge see Section 6 1 Quantifier Elimination page 29 rlgqea formula theory exceptionlist Function Generic quantifier elimination with answer rlgqea is not available in ACFSF and DVFSF exceptionlist is a list of variables empty by default Returns a list consisting of an extended theory and an elimination answer Compare rlqea rlgqe see Section 6 1 Quantifier Elimination page 29 After applying generic quantifier elimination the user might feel that the result is still too large while the theory is still quite weak The following function rlgentheo simplifies a formula by making further assumptions rlgentheo theory formula exceptionlist Function Generate theory rlgentheo is not available in DVFSF formula is a quantifier free formula exceptionlist is a list of variables empty by default Chapter 6 Quantifier Elimination and Variants 35 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 simplified formula rlqegenct Switch Quantifier elimination generate complex theory This is on by default which allows rlgentheo to assume inequalities
54. only in OFSF If turned on alter native elimination sets are used for certain special cases by rlqe rlqea and rlgqe rlgqea see Section 6 2 Generic Quantifier Elimination page 34 They will possibly avoid violations of the degree restrictions but lead to larger results in general Former versions of REDLOG without these switches behaved as if rlqeqsc was on and rlqesqsc was off rlqedfs Advanced Switch Quantifier elimination depth first search By default this switch is off It is also ignored in the ACFSF context It is ignored with the switch rlqeheu on which is the default for oFsF Turning rlqedfs on makes rlqe rlqea and rlgqe rlgqea see Section 6 2 Generic Quantifier Elim ination page 34 work in a depth first search manner instead of breadth first search This saves space and with decision problems where variable free atomic formulas can be evaluated to truth values it might save time In general it leads to larger results rlqeheu Advanced Switch Quantifier elimination search heuristic By default this switch is on in OFSF and off in DVFSF It is ignored in ACFSF Turning rlqeheu on causes the switch rlqedfs to be ignored rlqe rlqea and rlgqge rlgqea see Chapter 6 Quantifier Elimination and Variants 31 Section 6 2 Generic Quantifier Elimination page 34 will then decide between breadth first search and depth first search for each quantifier block where DFs is chosen when the problem is a decision problem r
55. ontexts page 2 for a summary of the available contexts OFSF DVFSF ACFSF PASF IBALP and DCFSF A context can be selected by the rlset command rlset context arguments Function rlset argument list Function Set current context Valid choices for context are OFSF ordered fields standard form bvFsF discretely valued fields standard form ACFSF algebraically closed fields standard form PASF Presburger arithmetic standard form IBALP initial Boolean algebra Lisp prefix and DCFSF With OFSF ACFSF PASF IBALP and DCFSF there are no further argu ments With DVFSF an optional dvf class specification can be passed which defaults to 0 rlset returns the old setting as a list that can be saved to be passed to rlset later When called with no arguments or the empty list rlset returns the current setting dvf class specification Data Structure Zero or a possibly negative prime q For q 0 all computations are uniformly correct for all p adic valuations 39 pnd Both input and output then possibly involve a symbolic constant p which is being reserved Chapter 2 Loading and Context Selection 6 For positive q all computations take place wrt the corresponding q adic valuation For negative q the can be read as up to i e all computations are performed in such a way that they are correct for all p adic valuations with p lt q In this case the knowledge of an upper bound for p support
56. op Bh RE 16 17 TLSISOTT i Coina eri tiea hd a E du 16 rlsisdf kids Rer UR 18 rlsitsdspl 2i 9 eee aes 18 19 rlt bib s cada peri oie 23 PIXtnft oiolligsio dk doeet anb Rd 28 IlV rfb6S6 dde ett e 25 rounded sadi dua verd doe dace wis 30 T I8 ccc we eis ates ese eS 13 oq LE 30 Data Structures 45 Data Structures Documentation of Data Structures COM nr 23 multiplicity list 13 dvf cl If i1Catioh 232 MUN a E tect substitution list 12 elimination answer 29 UlBOEy eios ee ted 15 RNC TEE 23 multiplicity list 13 14 dvf class specification 5 substitution Heb eins 12 14 36 elimination answer 29 34 Index Index reducerc profile 0 6 A ACFSF 2 3 5 10 15 16 19 20 29 30 31 34 35 additively split atomic formula 16 17 19 advanced atomic formula simplification LL 19 advanced Switch 0 4 algebraic simplification 23 algebraically closed field 2 ANSWE e iict rhea etiedewtrneeas 3 29 34 anti prenex normal form 28 31 atomic formula list I3 atomic formula multiplicity list 13 atomic formula simplification 17 19 20 21 atomic formulas 000 13 automatic simplification 13 automatic tableau 28 availab
57. over non monomial terms with the generic quantifier elimination rlgcad formula Function Generic cylindrical algebraic decomposition rlgcad is available only for OFSF Compare rlcad see Section 6 1 Quantifier Elimination page 29 and rlgqe see Section 6 2 Generic Quantifier Elimination page 34 rlghqe formula Function Generic Hermitian quantifier elimination rlghqe is available only for OFSF Compare rlhge see Section 6 1 Quantifier Elimination page 29 and rlgqe see Section 6 2 Generic Quantifier Elimination page 34 6 3 Local Quantifier Elimination In contrast to the generic quantifier elimination see Section 6 2 Generic Quantifier Elimination page 34 the following variant of rlqe see Sec tion 6 1 Quantifier Elimination page 29 enlarges the theory by arbitrary atomic formulas wherever this supports the quantifier elimination process This is done in such a way that the theory holds for the suggested point specified by the user The method has been described in detail in DW00 rllqe formula theory suggestedpoint Function Local quantifier elimination rllqe is not available in ACFSF and DVFSF suggestedpoint is a list of equations var value where var is a free vari able and value is a rational number Returns a list th such that th is a superset of theory and f is a quantifier free formula equivalent to formula assuming th The added inequalities contains exclusively vari ables occuring on the le
58. pecific Standard Simplifier Switches page 18 else rlsiexpl is not used in the DVFSF context The DVFSF simplifier behaves like rlsiexpla on The user is not supposed to alter the settings of the following fix switches see Section 1 3 Conventions page 4 rlsism Fix Switch Simplify smart By default this switch is on See the description of the function rlsimpl see Section 4 1 Standard Simplifier page 15 for its effects rlsimpl x gt 0 and x 1 lt 0 gt false rlsichk Fix Switch Simplify check By default this switch is on enabling checking for equal sibling subformulas rlsimpl x 0 and x 1 0 or x gt 0 and x 1 0 x50 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 see Section 4 1 Standard Simplifier page 15 is idempotent in the very most cases i e an ap plication 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 0 and b 0 4 1 3 OFSF specific Simplifications In the OFSF context the atomic formula simplification includes the following e Evaluation of variable free atomic formulas to truth values e Make the left hand sides primitive over the integers with positive head coefficient C
59. plification 25 RR b2604e09 5 15 4 1 Standard Simplifier 0 0 06 cece ee eee eens 15 4 1 1 General Features of the Standard Simplifier 15 4 1 2 General Standard Simplifier Switches 16 4 1 8 OFSF specific Simplifications 0 0000000 17 4 1 4 OFSF specific Standard Simplifier Switches 18 4 1 5 ACFSF specific Simplifications 00000005 19 4 1 6 ACFSF specific Standard Simplifier Switches 20 4 1 7 DVFSF specific Simplifications ssse sese 20 4 1 8 DVFSF specific Standard Simplifier Switches 21 4 1 9 PASF specific Simplifications 00 000 eee 21 4 1 10 PASF specific Standard Simplifier Switches 22 4 2 Tableau Simplifier 0000 0 cece eee eens 23 4 3 Groebner Simplifier cc 2tc4e ehderdeae ee EE nh n 29 4 4 Degree Decreaser 0 00 ccc cee cee hh 26 5 Normal FPorms 2x m a A REESE 27 5 1 Boolean Normal Forms 000 c cece eee e tenet eee 27 5 2 Miscellaneous Normal Forms lesse eee 27 6 Quantifier Elimination and Variants 29 6 1 Quantifier Elimination 0 eee eee eee 29 6 1 1 Virtual Substitution 0 00 0 cece cee eee ee 29 6 1 2 Cylindrical Algebraic Decomposition 31 6 1 3 Hermitian Quantifier Elimination 34 6 2 Generic Quantifier Elimination 0 0000 e ee ee
60. r documentation Switch This is an ordinary switch which usually selects strategies ap propriate for a particular input or determines the required trade off between computation speed and quality of the result Advanced Switch They are used like ordinary switches You need however a good knowledge about the underlying algorithms for making use of it Fix Switch You do not want to change it Chapter 2 Loading and Context Selection 5 2 Loading and Context Selection 2 1 Loading Redlog At the beginning of each session REDLOG has to be loaded explicitly This is done by inputing the command load_package redlog from within a REDUCE session 2 2 Context Selection Fixing a context reflects the mathematical fact that first order formulas are defined over fixed languages specifying e g valid function symbols and relation symbols predicates After selecting a language fixing a theory such as the theory of ordered fields allows to assign a semantics to the formulas Both language and theory make up a REDLOG context In addition a context determines the internal representation of terms As first order formulas are not defined unless the language is known and meaningless unless the theory is known it is impossible to enter a first order formula into REDLOG without specifying a context REDUCE 3 6 15 Jul 95 patched to 30 Aug 98 1 load_package redlog 2 f a 0 and b 0 kkKK Select a context See Section 1 1 C
61. rences of the quantified variables There are also heuristic strategies for coping with higher degrees included The method is described in detail in Stu00 The ACFSF quantifier elimination is based on comprehensive Groebner basis computation there are no degree restrictions for this context Wei92 In PASF context the quantifier elimination is based on the fast method similar to elimination by virtual substitution introduced by Weispfenning For more details see Wei90 6 1 Quantifier Elimination 6 1 1 Virtual Substitution rlge formula theory Function Quantifier elimination by virtual substitution Returns a quantifier free equivalent of formula wrt theory In the contexts OFSF and DVFSF formula has to obey certain degree restrictions There are various tech niques 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 is not quantifier free but still equivalent For degree decreasing heuristics see e g Section 4 4 Degree Decreaser page 26 or the switches rlqeqsc rlqesqsc 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 answer Returns an elimination answer ob tained the following way formula is wlog prenex All quantifier blocks but the outermost one
62. rited from higher levels switch rlsism see Section 4 1 2 General Standard Simplifier Switches page 16 The smart simplification techniques used for this are beyond the scope of this manual They are described in detail in DS97 for OFSF ACFSF and in DS99 for DvFSF 4 1 2 General Standard Simplifier Switches rlsiexpla Switch Simplify explode always By default this switch is on It is relevant with simplifications that allow to split one atomic formula into several simpler ones Consider e g the following simplification toggled by the switch rlsipd see Section 4 1 4 OFSF specific Standard Simplifier Switches page 18 With rlsiexpla on we obtain f a 1 3 x a 1 4 gt 0 7 6 5 4 3 2 gt a ta 3 a 3 a 3ta 3ta a 1 gt 0 rlsimpl f gt a i1 gt O0orat ti 0 With rlsiexpla off f will simplify as in the description of the switch rlsipd rlsiexpla is not used in the DvFSF context The DVFSF simpli fier behaves like rlsiexpla on Chapter 4 Simplification 17 rlsiexpl Switch Simplify explode By default this switch is on Its role is very similar to that of rlsiexpla but it considers the operator the scope of which the atomic formula occurs in With rlsiexpl on T 6 5 4 3 2 a ta 3 a 3 a 3a 34a 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 see Section 4 1 4 OFSF s
63. rs which considerably speeds up the elimination For geometric theorem proving it has turned out that these assump tions correspond to reasonable geometric non degeneracy conditions DSW98 Generic quantifier elimination has turned out useful also for physical applications such as network analysis Stu97 There is no generic quantifier elimination available for DVFSF See Section 6 2 Generic Quantifier Elimination page 34 e The contexts OFSF and DVFSF provide variants of generic quantifier elimination that additionally compute answers such as satisfying sample points for existentially quantified formulas l his has been referred to as Chapter 1 Introduction 4 the extended quantifier elimination problem Wei97a See Section 6 1 Quantifier Elimination page 29 e OFSF includes linear optimization techniques based on quantifier elimi nation Wei94a See Section 6 4 Linear Optimization page 35 1 3 Conventions To avoid ambiguities with other packages all REDLOG functions and switches are prefixed by rl The remaining part of the name is explained by the first sentence of the documentation of the single functions and switches Some of the numerous switches of REDLOG have been introduced only for finding the right fine tuning of the functions or for internal experiments They should not be changed anymore except for in very special situations For an easier orientation the switches are divided into three categories fo
64. s specified that all right hand sides must be zero In analogy to OFSF ACFSF allows also the input of chains and an appropriate treatment of parametric denominators in the input See Section 3 3 OFSF Operators page 8 for details Note that the switch rlposden see Section 3 3 OFSF Operators page 8 makes no sense for algebraically closed fields 3 6 PASF Operators equal Binary Infix operator neq Binary Infix operator leq Binary Infix operator geq Binary Infix operator lessp Binary Infix operator greaterp Binary Infix operator The above operators may also be written as lt gt lt gt lt and gt respectively cong Ternary Prefix operator ncong Ternary Prefix operator The operators cong and ncong represent congruences with nonparametric modulus given by the third argument The example below defines the set of even integers Chapter 3 Format and Handling of Formulas 11 f cong x 0 2 gt x 727 0 As for OFSF it is specified that all right hand sides are transformed to be zero In analogy to OFSF PASF allows also the input of chains See Section 3 3 OFSF Operators page 8 for details 3 7 IBALP Operators bnot Unary operator band n ary Infix operator bor n ary Infix operator bimpl Binary Infix operator brepl Binary Infix operator bequiv Binary Infix operator The operator bnot may also be written as The operators band and bor may also be written as amp and
65. s the quantifier elimination rlqe rlqea Stu00 See Section 6 1 Quantifier Elimination page 29 The user will probably have a favorite context reflecting their particular field of interest To save the explicit declaration of the context with each session REDLOG provides a global variable rldeflang which contains a default context This variable can be set already before loading redlog This is typically done within the reducerc profile lisp rldeflang ofsf Notice that the Lisp list representation has to be used here rldeflang Fluid Default language This can be bound to a default context before loading redlog More precisely rldeflang contains the arguments of rlset as a Lisp list If rldeflang is non nil rlset is automatically executed on rldeflang when loading redlog In addition REDLOG evaluates an environment variable RLDEFLANG This allows to fix a default context within the shell already before starting RE DUCE The syntax for setting environment variables depends on the shell For instance in the GNU Bash or in the csh shell one would say export RLDEFLANG ofsf or setenv RLDEFLANG ofsf respectively RLDEFLANG Environment Variable Default language This may be bound to a context in the sense of the first argument of rlset With RLDEFLANG set any rldeflang binding is overloaded Chapter 3 Format and Handling of Formulas 7 3 Format and Handling of Formulas After loa
66. s is never increased Mind that by reduc tion the terms can become more complicated rlgsvb Advanced 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 see Section 3 10 Global Switches page 12 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 con tracted multiplicatively to one atomic formula This reduces the number of atomic formulas but in most cases it raises the complexity of the terms Most simplifications recognized by considering products are detected also with rlgsprod off rlgserf Advanced Switch Groebner simplifier evaluate reduced form By default this switch is on It controls the evaluation of the atomic formulas to truth values If this switch is on the standard simplifier see Section 4 1 Standard Simplifier page 15 is used to evaluate atomic formulas Otherwise atomic formulas are evaluated only 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 reductions 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 state
67. s purpose we make use of ad vanced algebraic concepts such as Groebner basis computations For the notion of simplification and a detailed description of the implemented techniques for the contexts OFSF and ACFSF see DS97 For the DVFSF context see DS99 See Chapter 4 Simplification page 15 e Various normal form computations The CNF DNF computation includes both boolean and algebraic simplification strategies DS97 The prenez normal form computation minimizes the number of quantifier changes See Chapter 5 Normal Forms page 27 e Quantifier elimination computes quantifier free equivalents for given first order formulas For OFSF and DVFSF we use a technique based on elimination set ideas Wei88 The OFSF implementation is restricted to at most quadratic occurrences of the quantified variables but includes numerous heuristic strategies for coping with higher degrees See LW93 Wei97 for details on the method The DvFSF implementation is restricted to formulas that are linear in the quantified variables The method is described in detail in Stu00 The ACFSF quantifier elimination is based on comprehensive Groebner basis computation There are no degree restrictions for this context Wei92 See Section 6 1 Quantifier Elimination page 29 e The contexts OFSF and ACFSF allow a variant of quantifier elimination called generic quantifier elimination DSW98 There are certain non degeneracy assumptions made on the paramete
68. sSi icem qedpresed ten nate poets 31 PlSebDuicssieileXng gung qubd 5 TEMS DM eset carne wei wget 15 bel os UC ae ea ee deo 14 LE AD ab crazed teas tae eeu grew re utn c 23 GO rTM Jose 2204 bc Eea 14 bl Dy 91s hing eae 14 PUGH fenced 23 b MUR hee eas ada Need 28 bl t ol ee en P EH EE 14 S SOI 21241 e3Reiegp bep e bed IRE 10 SUD ose eo sens pef veas dues 12 Functions References to Functions A ends EE EE EE T EE 12 E equiv scie eme RIGEN UV Rn 31 F POR 20 xr ata a elses EUR dle n RC i I implet cute ee Hha d e IE Ib AR 16 L load package I teed ee Hed 5 N NOG eid ae ee Hehehe edhe eae eb 16 O OE Bo ee deceat rc puede qoe p dE ee 212 P partoese zenteeette ehOERERRIGS RS ER 3 12 42 R dE 16 flatab L 55 j0gda gata eeentva dennis 23 ppl or oe a ea Rd 27 pl Co i ah ae 27 rlgentbeOo 22 d perei karis 34 35 rlgges c Er RAE Des 30 31 35 Ilgd 8 sede eR urpita E RU Ras 30 31 IlES C secs teehee EORR Rd Seed 24 27 PIGS peed deese ed ginisi 24 27 PIGS six cdnDDe ue pu PD er ME 24 Plitab o eese FRE Re mee 23 rl dtrix Hilde es tose eeu 12 Iln ficseriseer e reeerie jv ENEN 31 IlOpbicolesijsesserkee ave YR 36 Ilpnf zc s iere hr niii eE hag e 31 PIGS i sve hepa ems 6 30 31 34 35 rlq68 m Rs Ra er ie ens 6 30 31 Ilqe6lpO0 ce ende p bI peus 31 Ilqews D bu sci e tentes erae 31 IIlS6tU L n6 I tebe dares ede REDE 6 rlsimpl 13 16 17 18 19 21 22 24 rlternl lee 9 eere E e eas 28
69. t This switch decides whether division or pseudo division is used for sturm chains Chapter 6 Quantifier Elimination and Variants 34 rlanuexgcdnormalize Advanced Switch GCD normalize This is turned on by default If turned on the GCD is normalized to 1 if it is a constant polynomial rlanuexsgnopt Advanced Switch Sign optimization This is turned off by default If turned on it is tried to determine the sign of a constant polynomial by calculating a containment 6 1 3 Hermitian Quantifier Elimination rlhqe formula Function Hermitian quantifier elimination Returns a quantifier free equivalent of formula Works only in context OFSF There are no degree restrictions on formula 6 2 Generic Quantifier Elimination The following variant of rlqe see Section 6 1 Quantifier Elimination page 29 enlarges the theory by inequalities i e lt gt atomic formulas wher ever this supports the quantifier elimination process For geometric prob lems it has turned out that in most cases the additional assumptions made are actually geometric non degeneracy conditions The method has been described in detail in DSW98 It has also turned out useful for physical problems such as network analysis Stu97 rlgqe formula theory exceptionlist Function Generic quantifier elimination rlgqe is not available in ACFSF and DVFSF exceptionlist is a list of variables empty by default Returns a list th such that th is a superset
70. ult rlcadte Switch Trial evaluation the first improvement to partial CAD This is turned on by default rlcadpbfvs Switch Propagation below free variable space the second improvement to partial CAD This is turned on by default rlcadfulldimonly Advanced Switch Full dimensional cells only This is turned off by default Only stacks over full dimensional cells are built Such cells have rational sample points To do this ist sound only in special cases as consistency problems existenially quantified strict inequalities rlcadtrimtree Switch Trim tree This is turned on by default Frees unused part of the con structed partial CAD tree and hence saves space However afterwards it is not possible anymore to find out how many cells were calculated beyond free variable space rlcadrawformula Advanced Switch Raw formula Turned off by default If turned on a variable free DNF is returned if simple solution formula construction succeeds Otherwise the raw result is simplified with rldnf Chapter 6 Quantifier Elimination and Variants 33 rlcadisoallroots Advanced Switch Isolate all roots This is off by default Turning this switch on allows to find out how much time is consumed more without incremental root isolation rlcadrawformula Advanced Switch Raw formula Turned off by default If turned on a variable free DNF is returned if simple solution formula construction succeeds Otherwise the raw result

Redlog User Manual

Contents

Download Pdf Manuals

Related Search

Related Contents