計算の例（４）

「xを0に近づけたときのsin(x)/xの極限値がyである」という式の入力と出力です．RedLog

rlqe(rlcnf(rlpnf( all(p,p>0 impl ex(q,q>0 and all({x,s,c},(0<x<q and 0<s<x and 0<c*x<s and c^2+s^2=1) impl (y-p)*x<s<(y+p)*x))) )));
8*y**2 + 8*y + 1 > 0 and 8*y**2 - 8*y + 1 > 0 and 8*y**2 - 8*y - 1 < 0 and 2*y**2 - 1 > 0 and 2*y**2 - 3 < 0 and y - 1 = 0

そして

rlqe(ex(y,8*y**2 + 8*y + 1 > 0 and 8*y**2 - 8*y + 1 > 0 and 8*y**2 - 8*y - 1 < 0 and 2*y**2 - 1 > 0 and 2*y**2 - 3 < 0 and y - 1 = 0));
true

なので，結果はy=1ということです．
　ここで用いたrlpnfは与えられた式をprenex formula（冠頭標準形 - Wikipedia）に直す関数で，何もいわなくてもQEの前処理として内部で実行されているのですが，これをまず行って標準形にしてから渡すとrlqeの処理時間が短くなります．なお，rlcnf，rldnfなどは量化子の外からでも作用してくれます．