と言えば，やはり不等式の成立です．すなわち 変数が仮定を満たすならば，結論の不等式が成り立つ という論理式を QE すれば，その式と同値で量化子を含まない式（とくに，成り立つときは true，成り立たないときは false）が得られる（RedLog ではtrue，fal…

今回は極限のお話です． よく知られた CAS（計算機代数システム）には極限を求めるコマンドが実装されており，例えば を得るには，Reduce では limit( 1/x , x , a ) ; Mathematica では Limit[ 1/x , x -> a ] Maple では limit( 1/x , x = a ) ; maxima で…