Mercurial > hg > Papers > 2018 > nozomi-master
diff presentation/slide.html @ 124:7ab9767dc9f9 presentation
Update slide
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 14 Feb 2017 16:18:28 +0900 |
parents | 81978a9122f0 |
children |
line wrap: on
line diff
--- a/presentation/slide.html Tue Feb 14 16:09:01 2017 +0900 +++ b/presentation/slide.html Tue Feb 14 16:18:28 2017 +0900 @@ -86,7 +86,7 @@ <!-- === begin markdown block === generated by markdown/1.2.0 on Ruby 2.3.3 (2016-11-21) [x86_64-darwin16] - on 2017-02-14 16:08:41 +0900 with Markdown engine kramdown (1.13.0) + on 2017-02-14 16:17:51 +0900 with Markdown engine kramdown (1.13.0) using options {} --> @@ -443,11 +443,6 @@ <!-- _S9SLIDE_ --> <h1 id="agda-">Agda における証明</h1> <ul> - <li>Curry-Howard Isomorphism による型付きラムダ計算と自然演繹の対応 - <ul> - <li>自然演繹: 命題、ならば、かつ、または、で構成される証明システム</li> - </ul> - </li> <li>論理式は型に相当して、証明はその値の導出</li> <li>三段論法の証明は以下のようになる <ul>