senooken JP Social
  • FAQ
  • Login
senooken JP Socialはsenookenの専用分散SNSです。
  • Public

    • Public
    • Network
    • Groups
    • Popular
    • People

Conversation

Notices

  1. きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Saturday, 23-Jan-2021 08:50:40 JST きゅーけー きゅーけー

    このチュートリアルめっちゃ重要だった。thm と verify コマンドと expand ヒントの使い方を覚えたぞ。https://www.cs.utexas.edu/users/kaufmann/tutorial/rev3.html#top

    #ACL2

    In conversation Saturday, 23-Jan-2021 08:50:40 JST from mastodon.tojo.tokyo permalink
    • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Saturday, 23-Jan-2021 09:27:12 JST きゅーけー きゅーけー
      in reply to

      expand のヒントの使い方を覚えたことで、11 以下のときは安全にヒットできることを示す定理がかけた。

      https://gitlab.com/tojoqk/blackjack/-/commit/12733bfa51f3cc6c98d2b067bf3217f4e2a76145

      In conversation Saturday, 23-Jan-2021 09:27:12 JST permalink
    • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Saturday, 23-Jan-2021 09:28:16 JST きゅーけー きゅーけー
      in reply to

      総当たりで解決しちゃっている感はある

      In conversation Saturday, 23-Jan-2021 09:28:16 JST permalink
    • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Sunday, 24-Jan-2021 03:32:18 JST きゅーけー きゅーけー
      in reply to

      https://mastodon.tojo.tokyo/@tojoqk/105606459763642932

      In conversation Sunday, 24-Jan-2021 03:32:18 JST permalink

      Attachments

      1. Domain not in remote thumbnail source whitelist: media.mastodon.tojo.tokyo
        きゅーけー (@tojoqk@mastodon.tojo.tokyo)
        from きゅーけー
        ACL2 で書いたブラックジャック、任意の枚数のカードで、score が 11 以下のときにもう一回カードを引いても BUST しない定理の証明に成功したのでだいたい満足した。 https://gitlab.com/tojoqk/blackjack/-/commit/60143c0e574d00a1571bd0750ca7186cdc4d04dc

Feeds

  • Activity Streams
  • RSS 2.0
  • Atom
  • Help
  • About
  • FAQ
  • TOS
  • Privacy
  • Source
  • Version
  • Contact

senooken JP Social is a social network, courtesy of senooken. It runs on GNU social, version 2.0.2-beta0, available under the GNU Affero General Public License.

Creative Commons Attribution 3.0 All senooken JP Social content and data are available under the Creative Commons Attribution 3.0 license.