login  home  contents  what's new  discussion  bug reports help  links  subscribe  changes  refresh  edit
 Topics FrontPage SandBox SandBoxProp <-- You are here. \begin{spad} )abbrev domain INEQTY InEquality ++ Author: kfp ++ Date Created: Sun Oct 26 02:21:23 CEST 2014 ++ License: BSD (same as Axiom) ++ Date Last Updated: ++ Basic Operations: ++ Related Domains: ++ Also See: ++ AMS Classifications: ++ Keywords: ++ Examples: ++ References: ++ ++ Description: ++ ++ InEquality(S:Comparable) : Exports == Implementation where OF ==> OutputForm Exports == Join(Comparable , CoercibleTo OutputForm) with "<" : (S,S) -> % ++ < means lesser than "<=" : (S,S) -> % ++ <= means lesser than or equal ">" : (S,S) -> % ++ > means greater than ">=" : (S,S) -> % ++ >= means greater than or equal eql : (S,S) -> % ++ = means equal neq : (S,S) -> % ++ neq means not equal. lhs : % -> S ++ lhs returns the left hand side of the inequality rhs : % -> S ++ rhs returns the right hand side of the inequality rel : % -> Symbol ++ rel returns the inequality (relation) symbol converse : % -> % ++ converse inequality coerce : % -> OF ++ coerce to output form Implementation == add Rep := Record(rel:Symbol , lhs : S, rhs : S) s:List(Symbol):=['<,'<=,'>,'>=,'=,'~=] l:S < r:S == [s.1, l, r]$Rep l:S <= r:S == [s.2, l, r]$Rep l:S > r:S == [s.3, l, r]$Rep l:S >= r:S == [s.4, l, r]$Rep eql(l:S,r:S) == [s.5, l, r]$Rep neq(l:S,r:S) == [s.6, l, r]$Rep lhs x == x.lhs rhs x == x.rhs rel x == x.rel converse x == x.rel = s.1 => [s.3, x.rhs, x.lhs]$Rep x.rel = s.2 => [s.4, x.rhs, x.lhs]$Rep x.rel = s.3 => [s.1, x.rhs, x.lhs]$Rep x.rel = s.4 => [s.2, x.rhs, x.lhs]$Rep x.rel = s.5 => [s.5, x.rhs, x.lhs]$Rep x.rel = s.6 => [s.6, x.rhs, x.lhs]$Rep coerce(x:%):OF == hconcat [x.lhs::OF," ", x.rel::OF, " ", x.rhs::OF] )abbrev domain PROP Prop ++ Prop is the domain of Propositions over a type T Prop(T:Comparable) : Exports == Implementation where S ==> Symbol PI ==> PositiveInteger EQT ==> InEquality(T) TT ==> Union(S,T,PI,EQT) Exports == with assert : InEquality(T) -> % ++ assert an equation of type InEquality(T) assert : Equation(T) -> % ++ assert an equation of type Equation(T) (convenience) And : (%,%) -> % ++ And means the logical connective and Or : (%,%) -> % ++ Or means the logical connective or Imp : (%,%) -> % ++ Imp means the logical connective implies Eqv : (%,%) -> % ++ Eqv means the logical connective equivalent Not : % -> % ++ Not means negation not All : (Symbol,%) -> % ++ All means the universal quantifier forall Ex : (Symbol,%) -> % ++ Ex means the existential quantifier exists coerce : % -> OutputForm ++ coerce to output form qvars : % -> List(TT) ++ qvars lists all quantifier variables nnf : % -> % ++ nnf means negation normal form nnf Implementation == add BinaryTree(TT) add Rep := BinaryTree(TT) -- map x in TT to Rep iD(x:TT):% == binaryTree(x)$Rep rs:List(Symbol):=['<,'<=,'>,'>=,'=,'~=] ----------------------- Op id's -- 1 ..... and -- 2 ..... or -- 3 ..... implies -- 4 ..... equivalent -- 5 ..... not -- 6 ..... forall -- 7 ..... exists -- 8,9 .... reserved -- 10 ..... equality -- 11 ..... neq -- 12 ..... lt -- 13 ..... leq -- 14 ..... gt -- 15 ..... geq ----------------------- -- assert an element of type Equation(T) assert(s:Equation(T)):% == binaryTree(iD lhs s,10,iD rhs s)$Rep assert(s:EQT):% == rel s = rs.1 => binaryTree(iD lhs s,12,iD rhs s)$Rep rel s = rs.2 => binaryTree(iD lhs s,13,iD rhs s)$Rep rel s = rs.3 => binaryTree(iD lhs s,14,iD rhs s)$Rep rel s = rs.4 => binaryTree(iD lhs s,15,iD rhs s)$Rep rel s = rs.5 => binaryTree(iD lhs s,10,iD rhs s)$Rep rel s = rs.6 => binaryTree(iD lhs s,11,iD rhs s)$Rep -- variable, the only nodes without left/right var(x:S):% == binaryTree(x)$Rep And(p:%,q:%):% == binaryTree(p,1,q)$Rep Or (p:%,q:%):% == binaryTree(p,2,q)$Rep Imp(p:%,q:%):% == binaryTree(p,3,q)$Rep Eqv(p:%,q:%):% == binaryTree(p,4,q)$Rep Not(p:%):% == binaryTree(p,5,empty())$Rep All(x:S,p:%):% == binaryTree(var x,6,p)$Rep Ex (x:S,p:%):% == binaryTree(var x,7,p)$Rep coerce(p) == OF ==> OutputForm lp:OF:="(" rp:OF:=")" lb:OF:="{" rb:OF:="}" lk:OF:="[" rk:OF:="]" of:OF:="" s0:OF:="." s1:OF:=" & " s2:OF:=" | " s3:OF:=" => " s4:OF:=" <=> " s5:OF:="~" s6:OF:="\" s7:OF:="?" s10:OF:=" = " s11:OF:=" ~= " s12:OF:=" < " s13:OF:=" <= " s14:OF:=" > " s15:OF:=" >= " empty? p => of val:= value p val=1 => of:=hconcat [of,lp,coerce(left p),s1,coerce(right p),rp] val=2 => of:=hconcat [of,lp,coerce(left p),s2,coerce(right p),rp] val=3 => of:=hconcat [of,lp,coerce(left p),s3,coerce(right p),rp] val=4 => of:=hconcat [of,lp,coerce(left p),s4,coerce(right p),rp] val=5 => of:=hconcat [of,s5,lp,coerce(left p),rp] val=6 => of:=hconcat [of,s6,coerce(left p),s0,lk,coerce(right p),rk] val=7 => of:=hconcat [of,s7,coerce(left p),s0,lk,coerce(right p),rk] val=10=> of:=hconcat [of,lb,coerce(left p),s10,coerce(right p),rb] val=11=> of:=hconcat [of,lb,coerce(left p),s11,coerce(right p),rb] val=12=> of:=hconcat [of,lb,coerce(left p),s12,coerce(right p),rb] val=13=> of:=hconcat [of,lb,coerce(left p),s13,coerce(right p),rb] val=14=> of:=hconcat [of,lb,coerce(left p),s14,coerce(right p),rb] val=15=> of:=hconcat [of,lb,coerce(left p),s15,coerce(right p),rb] of:=hconcat[of,val::OF] of --local mvNot(p:%):% == val := value p val=1 => Or(Not(left p),Not(right p))::Rep val=2 => And(Not(left p),Not(right p))::Rep val=3 => And(left p, Not(right p))::Rep val=4 => Not(Or(And(left p,right p),And(Not(left p),Not(right p)))) val=5 => (left p)::Rep val=6 => Ex(value(left p)::S, Not(right p))::Rep val=7 => All(value(left p)::S, Not(right p))::Rep val=10 => binaryTree(left p,11,right p)$Rep val=11 => binaryTree(left p,10,right p)$Rep val=12 => binaryTree(left p,15,right p)$Rep val=13 => binaryTree(left p,14,right p)$Rep val=14 => binaryTree(left p,13,right p)$Rep val=15 => binaryTree(left p,12,right p)$Rep p::Rep nnf(p:%):% == empty? p => p::Rep val := value p val=1 => And(nnf(left p),nnf(right p)) val=2 => Or(nnf(left p),nnf(right p)) val=3 => nnf(Or(Not(left p),right p)) val=4 => nnf(And(Or(left p,Not(right p)),Or(Not(left p),right p))) val=5 => nnf(mvNot(left p)) val=6 => All(value(left p)::S, nnf(right p)) val=7 => Ex(value(left p)::S, nnf(right p)) p::Rep qvars(p:%):List(TT) == L:List(TT):=[] empty? p => []::List(TT) val := value p if (val case S) then L:=append(L,[val]) else L:=append(L,qvars(left p)) L:=append(L,qvars(right p)) L )abbrev domain SUBSET SubsetOf ++ Author: kfp ++ Date Created: Mon Nov 03 20:41:24 CET 2014 ++ License: BSD (same as Axiom) ++ Date Last Updated: ++ Basic Operations: ++ Related Domains: ++ Also See: ++ AMS Classifications: ++ Keywords: ++ Examples: ++ References: ++ ++ Description: ++ ++ SubsetOf(T:Comparable) : Exports == Implementation where OF ==> OutputForm Exports == Join(Comparable , CoercibleTo OutputForm) with setOfAll : (List Symbol, Prop T ) -> % member? : (List T,%) -> Boolean coerce : % -> OutputForm Implementation == Prop(T) add Rep := Record(s:List Symbol, p:Prop T) setOfAll(ls,P) == [ls,P]::Rep member?(t,ss) == false coerce(ss:%):OF == r:=ss::Rep sym:OF:=(r.s)::OF prop:OF:=(r.p)::OF hconcat [Set of all , sym, such that , prop] \end{spad} InEq \begin{axiom} )set output tex off )set output algebra on x>0 x^2+y^2<1 a+b<=2 sin(x)+y>=1+y eql(x,y) neq(x,y) P1:=sin(x)+y>=1+y lhs P1 rhs P1 rel P1 converse P1 \end{axiom} Propositions \begin{axiom} assert(P1) R ==> EXPR INT A:=assert(x::R + y + z >=1) B:=assert(z::R<1/2) C:=assert(x+y=4::R) And(A,B) Or(A,B) Imp(A,C) Eqv(B,C) Not(A) Not(C) All(x,A) All(y,Ex(z,A)) All(x,All(y,Imp(assert(x=y),assert(y=x)))) \end{axiom} NNF \begin{axiom} m1:=assert(m>1::R) m2:=assert(m SUBSETS \begin{axiom} setOfAll([x,y,z],assert(x^2+y^2+z^2<=1)) setOfAll([x,y],And(assert(x^2c))) \end{axiom} -- continue with NatDed/Solve/RSPACE/Cell/Interval/Surface(k) , requires: CAD Some or all expressions may not have rendered properly, because Axiom returned the following error:Error: export FRICAS=/usr/local/lib/fricas/target/x86_64-unknown-linux; export ALDORROOT=/usr/local/aldor/linux/1.1.0; export PATH=$ALDORROOT/bin:$PATH; export HOME=/var/zope2/var/LatexWiki; ulimit -t 600; export LD_LIBRARY_PATH=/usr/local/lib/fricas/target/x86_64-unknown-linux/lib; LANG=en_US.UTF-8 \$FRICAS/bin/FRICASsys < /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/8659343403449756850-25px.axm /bin/sh: /usr/local/lib/fricas/target/x86_64-unknown-linux/bin/FRICASsys: not found  Some or all expressions may not have rendered properly, because Latex returned the following error:This is pdfTeXk, Version 3.141592-1.40.3 (Web2C 7.5.6) \write18 enabled. %&-line parsing enabled. entering extended mode (./2008420880488702843-16.0px.tex LaTeX2e <2005/12/01> Babel and hyphenation patterns for english, usenglishmax, dumylang, noh yphenation, arabic, farsi, croatian, ukrainian, russian, bulgarian, czech, slov ak, danish, dutch, finnish, basque, french, german, ngerman, ibycus, greek, mon ogreek, ancientgreek, hungarian, italian, latin, mongolian, norsk, icelandic, i nterlingua, turkish, coptic, romanian, welsh, serbian, slovenian, estonian, esp eranto, uppersorbian, indonesian, polish, portuguese, spanish, catalan, galicia n, swedish, ukenglish, pinyin, loaded. (/usr/share/texmf-texlive/tex/latex/base/article.cls Document Class: article 2005/09/16 v1.4f Standard LaTeX document class (/usr/share/texmf-texlive/tex/latex/base/size12.clo)) (/usr/share/texmf-texlive/tex/latex/ucs/ucs.sty (/usr/share/texmf-texlive/tex/latex/ucs/data/uni-global.def)) (/usr/share/texmf-texlive/tex/latex/base/inputenc.sty (/usr/share/texmf-texlive/tex/latex/ucs/utf8x.def)) (/usr/share/texmf-texlive/tex/latex/bbm/bbm.sty) (/usr/share/texmf-texlive/tex/latex/jknapltx/mathrsfs.sty) (/usr/share/texmf-texlive/tex/latex/base/fontenc.sty (/usr/share/texmf-texlive/tex/latex/base/t1enc.def)) (/usr/share/texmf-texlive/tex/latex/pstricks/pstricks.sty (/usr/share/texmf-texlive/tex/generic/pstricks/pstricks.tex PSTricks' v1.15 <2006/12/22> (tvz) (/usr/share/texmf-texlive/tex/generic/pstricks/pstricks.con)) (/usr/share/texmf/tex/latex/xcolor/xcolor.sty (/etc/texmf/tex/latex/config/color.cfg) (/usr/share/texmf-texlive/tex/latex/graphics/dvips.def) (/usr/share/texmf-texlive/tex/latex/graphics/dvipsnam.def))) (/usr/share/texmf-texlive/tex/latex/graphics/epsfig.sty (/usr/share/texmf-texlive/tex/latex/graphics/graphicx.sty (/usr/share/texmf-texlive/tex/latex/graphics/keyval.sty) (/usr/share/texmf-texlive/tex/latex/graphics/graphics.sty (/usr/share/texmf-texlive/tex/latex/graphics/trig.sty) (/etc/texmf/tex/latex/config/graphics.cfg)))) (/usr/share/texmf-texlive/tex/latex/pst-grad/pst-grad.sty (/usr/share/texmf-texlive/tex/generic/pst-grad/pst-grad.tex (/usr/share/texmf-texlive/tex/latex/xkeyval/pst-xkey.tex (/usr/share/texmf-texlive/tex/latex/xkeyval/xkeyval.sty (/usr/share/texmf-texlive/tex/latex/xkeyval/xkeyval.tex))) pst-plot' v1.05, 2006/11/04 (tvz,dg,hv))) (/usr/share/texmf-texlive/tex/latex/pstricks/pst-plot.sty (/usr/share/texmf-texlive/tex/generic/pstricks/pst-plot.tex v97 patch 2, 1999/12/12 (/usr/share/texmf-texlive/tex/generic/multido/multido.tex v1.41, 2004/05/18 ))) (/usr/share/texmf-texlive/tex/latex/geometry/geometry.sty (/usr/share/texmf-texlive/tex/xelatex/xetexconfig/geometry.cfg) Package geometry Warning: lmargin' and rmargin' result in NEGATIVE (-108.405p t). width' should be shortened in length. ) (/usr/share/texmf-texlive/tex/latex/amsmath/amsmath.sty For additional information on amsmath, use the ? option. (/usr/share/texmf-texlive/tex/latex/amsmath/amstext.sty (/usr/share/texmf-texlive/tex/latex/amsmath/amsgen.sty)) (/usr/share/texmf-texlive/tex/latex/amsmath/amsbsy.sty) (/usr/share/texmf-texlive/tex/latex/amsmath/amsopn.sty)) (/usr/share/texmf-texlive/tex/latex/amsfonts/amsfonts.sty) (/usr/share/texmf-texlive/tex/latex/amsfonts/amssymb.sty) (/usr/share/texmf-texlive/tex/latex/amscls/amsthm.sty) (/usr/share/texmf-texlive/tex/latex/setspace/setspace.sty Package: setspace 6.7 <2000/12/01> ) (/usr/share/texmf-texlive/tex/generic/xypic/xy.sty (/usr/share/texmf-texlive/tex/generic/xypic/xy.tex Bootstrap'ing: catcodes, docmode, (/usr/share/texmf-texlive/tex/generic/xypic/xyrecat.tex) (/usr/share/texmf-texlive/tex/generic/xypic/xyidioms.tex) Xy-pic version 3.7 <1999/02/16> Copyright (c) 1991-1998 by Kristoffer H. Rose Xy-pic is free software: see the User's Guide for details. Loading kernel: messages; fonts; allocations: state, direction, utility macros; pictures: \xy, positions, objects, decorations; kernel objects: directionals, circles, text; options; algorithms: directions, edges, connections; Xy-pic loaded)) (/usr/share/texmf-texlive/tex/generic/xypic/xyall.tex Xy-pic option: All features v.3.3 (/usr/share/texmf-texlive/tex/generic/xypic/xycurve.tex Xy-pic option: Curve and Spline extension v.3.7 curve, circles, loaded) (/usr/share/texmf-texlive/tex/generic/xypic/xyframe.tex Xy-pic option: Frame and Bracket extension v.3.7 loaded) (/usr/share/texmf-texlive/tex/generic/xypic/xycmtip.tex Xy-pic option: Computer Modern tip extension v.3.3 (/usr/share/texmf-texlive/tex/generic/xypic/xytips.tex Xy-pic option: More Tips extension v.3.3 loaded) loaded) (/usr/share/texmf-texlive/tex/generic/xypic/xyline.tex Xy-pic option: Line styles extension v.3.6 loaded) (/usr/share/texmf-texlive/tex/generic/xypic/xyrotate.tex Xy-pic option: Rotate and Scale extension v.3.3 loaded) (/usr/share/texmf-texlive/tex/generic/xypic/xycolor.tex Xy-pic option: Colour extension v.3.3 loaded) (/usr/share/texmf-texlive/tex/generic/xypic/xymatrix.tex Xy-pic option: Matrix feature v.3.4 loaded) (/usr/share/texmf-texlive/tex/generic/xypic/xyarrow.tex Xy-pic option: Arrow and Path feature v.3.5 path, \ar, loaded) (/usr/share/texmf-texlive/tex/generic/xypic/xygraph.tex Xy-pic option: Graph feature v.3.7 loaded) loaded) (/usr/share/texmf-texlive/tex/latex/tools/verbatim.sty) (/usr/share/texmf/tex/latex/graphviz/graphviz.sty (/usr/share/texmf-texlive/tex/latex/psfrag/psfrag.sty)) (/usr/share/texmf/tex/latex/sagetex.sty Writing sage input file 2008420880488702843-16.0px.sage ) (/usr/share/texmf-texlive/tex/latex/gnuplottex/gnuplottex.sty (/usr/share/texmf-texlive/tex/latex/base/latexsym.sty) (/usr/share/texmf-texlive/tex/latex/moreverb/moreverb.sty) (/usr/share/texmf-texlive/tex/latex/base/ifthen.sty)) (./2008420880488702843-16.0px.aux) (/usr/share/texmf-texlive/tex/latex/ucs/ucsencs.def) (/usr/share/texmf-texlive/tex/latex/jknapltx/ursfs.fd) (/usr/share/texmf-texlive/tex/latex/amsfonts/umsa.fd) (/usr/share/texmf-texlive/tex/latex/amsfonts/umsb.fd) (/usr/share/texmf-texlive/tex/latex/base/ulasy.fd) [1] Misplaced alignment tab character &. l.308 s1:OF:=" & " Overfull \hbox (38.1871pt too wide) in paragraph at lines 298--338 \T1/cmr/m/n/12 [of,s6,coerce(left p),s0,lk,coerce(right p),rk] val=7 => of:=hco ncat [of,s7,coerce(left p),s0,lk,coerce(right p),rk] val=10=> of:=hconcat [of,l b,coerce(left Overfull \hbox (39.7535pt too wide) in paragraph at lines 298--338 \T1/cmr/m/n/12 p),s10,coerce(right p),rb] val=11=> of:=hconcat [of,lb,coerce(le ft p),s11,coerce(right p),rb] val=12=> of:=hconcat [of,lb,coerce(left p),s12,co erce(right [2] [3] (/usr/share/texmf-texlive/tex/latex/base/t1cmtt.fd) LaTeX Warning: Characters dropped after \end{axiom}' on input line 439. LaTeX Warning: Characters dropped after \end{axiom}' on input line 455. LaTeX Warning: Characters dropped after \end{axiom}' on input line 465. LaTeX Warning: Characters dropped after \end{axiom}' on input line 469. [4] [5] (./2008420880488702843-16.0px.aux) ) (see the transcript file for additional information) Output written on 2008420880488702843-16.0px.dvi (5 pages, 10784 bytes). Transcript written on 2008420880488702843-16.0px.log. `

 Subject:   Be Bold !! ( 15 subscribers )