Conversation

Notices

1. きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Saturday, 04-Sep-2021 19:54:04 JST きゅーけー

   ACL2 を使ってると古典論理に支配されてしまう感じがする。特に p -> q で p が偽のとき真という異常な感覚が養われつつある。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Saturday, 04-Sep-2021 19:57:26 JST きゅーけー

     in reply to

     ACL2 が式変形した結果、仮定が偽になっているやつが見つかり、全体を真にするために仮定が偽であることを証明するということがたまによくある。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Saturday, 04-Sep-2021 20:02:23 JST きゅーけー

     in reply to

     1=2 ならば全ての猫は爬虫類に属する(古典論理では真)