Mercurial > hg > Papers > 2018 > nozomi-master

comparison presentation/slide.html @ 124:7ab9767dc9f9 presentation

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update slide
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Tue, 14 Feb 2017 16:18:28 +0900
parents 81978a9122f0
children
comparison
equal deleted inserted replaced
123:81978a9122f0 124:7ab9767dc9f9
84 84
85 <div class='slide '> 85 <div class='slide '>
86 <!-- === begin markdown block === 86 <!-- === begin markdown block ===
87 87
88 generated by markdown/1.2.0 on Ruby 2.3.3 (2016-11-21) [x86_64-darwin16] 88 generated by markdown/1.2.0 on Ruby 2.3.3 (2016-11-21) [x86_64-darwin16]
89 on 2017-02-14 16:08:41 +0900 with Markdown engine kramdown (1.13.0) 89 on 2017-02-14 16:17:51 +0900 with Markdown engine kramdown (1.13.0)
90 using options {} 90 using options {}
91 --> 91 -->
92 92
93 <!-- _S9SLIDE_ --> 93 <!-- _S9SLIDE_ -->
94 <h1 id="section">プログラミング言語とソフトウェアの信頼性</h1> 94 <h1 id="section">プログラミング言語とソフトウェアの信頼性</h1>
441 </div> 441 </div>
442 <div class='slide '> 442 <div class='slide '>
443 <!-- _S9SLIDE_ --> 443 <!-- _S9SLIDE_ -->
444 <h1 id="agda-">Agda における証明</h1> 444 <h1 id="agda-">Agda における証明</h1>
445 <ul> 445 <ul>
446 <li>Curry-Howard Isomorphism による型付きラムダ計算と自然演繹の対応
447 <ul>
448 <li>自然演繹: 命題、ならば、かつ、または、で構成される証明システム</li>
449 </ul>
450 </li>
451 <li>論理式は型に相当して、証明はその値の導出</li> 446 <li>論理式は型に相当して、証明はその値の導出</li>
452 <li>三段論法の証明は以下のようになる 447 <li>三段論法の証明は以下のようになる
453 <ul> 448 <ul>
454 <li>「((A ならば B) かつ (B ならば C)) ならば (A ならば C)</li> 449 <li>「((A ならば B) かつ (B ならば C)) ならば (A ならば C)</li>
455 </ul> 450 </ul>