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>