isabelleの検索結果1 - 2 件 / 2件

• あとで読む

  Isabelle ゆるリファレンス（apply-scriptスタイル） - 若くない何かの悩み

  • 4 users
  • blog.kuniwak.com
  • テクノロジー
  • 2020/12/19

  最近は本業の自動テストマンより定理証明支援系に力を入れている Kuniwak です（経緯は過去記事参照）。 orgachem.hatenablog.com 定理証明支援系はいいぞ、ということで本記事では 私がよく使う Isabelle の便利機能の紹介とごく個人的に感じている使い所などを書いています。 そのため全機能を網羅するものではなくかなり漏れがあります。もし「これめっちゃ便利だけど書いてない！」みたいな気づきがありましたらご指摘いただけると嬉しいです！ 本記事の対象読者 対象読者は Isabelle の apply-script スタイルを学びたい方で、かつ「Tutorial on Isabelle/HOL 2020 の 1, 2, 3, 5 章を読んでなんとなくわかったけど…」な方です。もし定理証明支援系を使ったことがなく、Tutorial もまだ読んでいない方は 1, 2, 3,

  
• あとで読む

  Isabelle/Isar勉強会を社内で開催しました - DeNA Testing Blog

  • 3 users
  • swet.dena.com
  • テクノロジー
  • 2022/08/04

  こんにちは、SWETグループの鈴木穂高（@hoddy3190）です。 SWETグループのメンバー向けにIsabelle/Isar勉強会を開催しました。本記事では、勉強会の概要の紹介と、勉強会の資料の公開をします。 もしよろしければご活用ください。 Isabelleとは Isabelleは、定理証明支援ツールの1つです。 数学の授業で証明を解く時、暗記した定義や定義を引き出して仮定や結論をみて試行錯誤しながら適用して解いていっていたと思います。Isabelleを使うと、利用できる定理を提示してくれたり、自動で定理を適用して証明を進めてくれたり、誤った証明を指摘してくれたりします。 Isabelleの大きな特徴として強力な自動証明が挙げられます。自動証明機能の典型例であるSledgehammerは、証明したい論理式を与えれば自動で定理を適用して証明を解き進めてくれます。 公理系も選択可能です。