![[PukiWiki]](image/knxmpen.png "[PukiWiki]")
Redlog is an integral part of the interactive computer algebra system Reduce. It supplements Reduce's comprehensive collection of powerful methods from symbolic computation by supplying more than 100 functions on first-order formulas. Redlog has been publicly available since 1995 and is constantly being improved. The name Redlog stands for Reduce Logic System.
Redlog は MathLibre にも収録されている数式処理ソフト REDUCE の一階述語論理パッケージです．
作動原理の異なる Quantifier Elimination (QE，量化子消去) 関数 rlqe (Virtual Substitution)，rlcad (Cylindrical Algebraic Decomposition)，rlhqe (Hermitian Quantifier Elimination) を軸に，ユーザーが新たな関数を書くに十分なコマンド群を実装しています．
端末，白黒で起動
reduce -w -b
パッケージのロードとコンテキストをR，分数関数も使えるように設定
load redlog;rlset r$on rlnzden,rladdcond;
高々2次の判別式
rlqe ex(x,x^2+b*x+c=0);
rlqe ex(x,a*x^2+b*x+c=0);
rlqe (ex(x,a*x^2+b*x+c=0), {a<>0});
rlqe (ex(x,a*x^2+b*x+c=0), {a=0});
「1/xは区間0<xで一様連続である」は偽
rlqe all(e,e>0 impl ex(d,d>0 and all({x,y},and(0<x,0<y,-d<=x-y<=d) impl -e<1/x-1/y<e)));
「a>0ならば1/xは区間a<xで一様連続である」は真
rlqe all({a,e},and(0<a,e>0) impl ex(d,d>0 and all({x,y},and(a<x,a<y,-d<=x-y<=d) impl -e<1/x-1/y<e)));
「1/xは区間a<xで一様連続である」は「a>0」と等価
rlqe all(e,e>0 impl ex(d,d>0 and all({x,y},and(a<x,a<y,-d<=x-y<=d) impl -e<1/x-1/y<e)));showtime;
終了
quit;
