Conversation

Notices

1. きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Saturday, 29-Jun-2024 14:17:17 JST きゅーけー

   値がないとすると間数が全域じゃなくなって困る。間数が全部全域で必ず値がある前提で定理証明をしてるから。
   ACL2 でもゼロ除算の結果は 0 だけど、ガードという機能でゼロ除算をしないことを証明できる形になってる。
   https://www.cs.utexas.edu/~moore/acl2/v8-5/combined-manual/?topic=ACL2____UNARY-_F2

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Saturday, 29-Jun-2024 14:20:28 JST きゅーけー

     in reply to

     定理証明手習いに間数が全域じゃない場合には矛盾を証明できるという話があったはず。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Saturday, 29-Jun-2024 14:59:46 JST きゅーけー

     in reply to

     いや、ガードよりも矛盾した証明ができないことが重要か。矛盾した定理を導く公理や定理がないから大丈夫という話か。