Mercurial > hg > Papers > 2017 > atton-master
changeset 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 | c1cc5407cefe |
| files | presentation/slide.html presentation/slide.md presentation/slide.pdf.html |
| diffstat | 3 files changed, 2 insertions(+), 14 deletions(-) [+] |
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>
--- a/presentation/slide.md Tue Feb 14 16:09:01 2017 +0900 +++ b/presentation/slide.md Tue Feb 14 16:18:28 2017 +0900 @@ -189,8 +189,6 @@ * Agda 上に CbC を定義することで形式的な定義を得る # Agda における証明 -* Curry-Howard Isomorphism による型付きラムダ計算と自然演繹の対応 - * 自然演繹: 命題、ならば、かつ、または、で構成される証明システム * 論理式は型に相当して、証明はその値の導出 * 三段論法の証明は以下のようになる * 「((A ならば B) かつ (B ならば C)) ならば (A ならば C)
--- a/presentation/slide.pdf.html Tue Feb 14 16:09:01 2017 +0900 +++ b/presentation/slide.pdf.html Tue Feb 14 16:18:28 2017 +0900 @@ -70,7 +70,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 {} --> @@ -427,11 +427,6 @@ <!-- _S9SLIDE_ --> <h1 id="agda-">Agda における証明</h1> <ul> - <li>Curry-Howard Isomorphism による型付きラムダ計算と自然演繹の対応 - <ul> - <li>自然演繹: 命題、ならば、かつ、または、で構成される証明システム</li> - </ul> - </li> <li>論理式は型に相当して、証明はその値の導出</li> <li>三段論法の証明は以下のようになる <ul>