|
\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 <v3.8h> 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 <tvz>)))
(/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 <krisrose@ens-lyon.fr>
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.
|