[討論] mathematica的量詞太神了吧？

[alfadick (悟道修行者)]

我讀virtual book的時候，看到量詞、Reduce、Resolve這些函數，

我看了幾個範例，真的有嚇到，

並且我反應很快，馬上想到：真那麼神，那費馬定理不就可以輕鬆推出來嗎？

但因為我才剛學，寫起來超卡，就沒去實驗了。

結果剛才逛到官網範例，還真的有耶：(最最下面的那個箭頭，巧妙範例點進去)

http://reference.wolfram.com/mathematica/ref/FullSimplify.html

這到底是怎麼做到的？它背後的機制是真的用迴圈瘋狂去test嗎？

因為我看官網Reduce/Resolve的範例，真的蠻強大的...

並且ForAll, Exist是巢狀量詞，這些直接跟高等微積分的精髓有關

如果那麼有效，我不敢想像在高等微積分會多麼神威...


--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 220.136.214.71
→ biglion:tutorial/SomeNotesOnInternalImplementation 文件中
→ biglion: Simplification(中文為"化簡")部分 有演算法的說明
→ biglion:大多數指令的演算法都有提到
→ alfadick:原來如此，一切其來有自。集人類智力文明顛峰於此軟體
→ alfadick:大開眼界了
推 ToMoveJizz:是識別而已吧?
感謝大家回應。剛才實驗了一下


FullSimplify[
 ForAll[\[Epsilon], \[Epsilon] > 0,
  Exists[\[Delta], \[Delta] > 0,
   ForAll[x, 0 < Abs[x - 2] < \[Delta], Abs[x^2 - 4] < \[Epsilon]]]]]

結果是 True。

其中的 x^2-4 改成 x^2-6 啊那些，結果出的來，是False。


換掉函數，x^2-4改成x^3-8，或者Sqrt[x]-Sqrt[2]、Sin[x]-0，

都跑超超超超超超久還跑不出來。


Mathematica在高微果然還是沒那麼神XDD

倒是

FullSimplify[
 ForAll[\[Epsilon], \[Epsilon] > 0,
  Exists[\[Delta], \[Delta] > 0,
   ForAll[x, 0 < Abs[x - 0] < \[Delta],
    Abs[Sin[1/x] - 0] < \[Epsilon]]]]]


他直接放棄判斷T/F，而是給出一整串的符號邏輯格式，這我有點不明白為什麼
※ 編輯: alfadick        來自: 220.136.214.71       (02/16 13:33)