Mercurial > hg > Papers > 2018 > nozomi-master

comparison presentation/slide.pdf.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
68 68
69 <div class='slide '> 69 <div class='slide '>
70 <!-- === begin markdown block === 70 <!-- === begin markdown block ===
71 71
72 generated by markdown/1.2.0 on Ruby 2.3.3 (2016-11-21) [x86_64-darwin16] 72 generated by markdown/1.2.0 on Ruby 2.3.3 (2016-11-21) [x86_64-darwin16]
73 on 2017-02-14 16:08:41 +0900 with Markdown engine kramdown (1.13.0) 73 on 2017-02-14 16:17:51 +0900 with Markdown engine kramdown (1.13.0)
74 using options {} 74 using options {}
75 --> 75 -->
76 76
77 <!-- _S9SLIDE_ --> 77 <!-- _S9SLIDE_ -->
78 <h1 id="section">プログラミング言語とソフトウェアの信頼性</h1> 78 <h1 id="section">プログラミング言語とソフトウェアの信頼性</h1>
425 </div> 425 </div>
426 <div class='slide '> 426 <div class='slide '>
427 <!-- _S9SLIDE_ --> 427 <!-- _S9SLIDE_ -->
428 <h1 id="agda-">Agda における証明</h1> 428 <h1 id="agda-">Agda における証明</h1>
429 <ul> 429 <ul>
430 <li>Curry-Howard Isomorphism による型付きラムダ計算と自然演繹の対応
431 <ul>
432 <li>自然演繹: 命題、ならば、かつ、または、で構成される証明システム</li>
433 </ul>
434 </li>
435 <li>論理式は型に相当して、証明はその値の導出</li> 430 <li>論理式は型に相当して、証明はその値の導出</li>
436 <li>三段論法の証明は以下のようになる 431 <li>三段論法の証明は以下のようになる
437 <ul> 432 <ul>
438 <li>「((A ならば B) かつ (B ならば C)) ならば (A ならば C)</li> 433 <li>「((A ならば B) かつ (B ならば C)) ならば (A ならば C)</li>
439 </ul> 434 </ul>