XU, Chuangjie \uff08\u535a\u58eb\u7814\u7a76\u54e1, Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen\uff09
\n\u5c71\ufa11 \u7d17\u7d00\u5b50\u3000 \uff08\u535a\u58eb\u8ab2\u7a0b, \u9996\u90fd\u5927\u5b66\u6771\u4eac\uff09<\/p>\n
\u8b1b\u6f14\u304a\u3088\u3073\u8cea\u7591\u5fdc\u7b54 (1)<\/b>\u300013:20\uff5e14:20
\n\u8b1b\u6f14\u8005\uff1a<\/b>XU, Chuangjie<\/p>\n
\u30bf\u30a4\u30c8\u30eb\uff1a<\/b> The computer as referee in mathematics
\n\u30a2\u30d6\u30b9\u30c8\u30e9\u30af\u30c8\uff1a<\/b> Proofs in modern mathematics now cover hundreds and soon thousands) of pages, with additional computer calculations worth gigabytes of data. Given that no referee (or even team of referees) can reliably judge the correctness of such a proof, how should mathematics as a field proceed? I will discuss one way forward, namely the use of Martin-Loef’s constructive type theory and the associated proof assistants (like Agda and Coq) to formalise and verify the correctness of proofs, and to execute proofs as computer programs. During the talk I will use the Agda proof assistant for demonstration.<\/p>\n
\u8b1b\u6f14\u304a\u3088\u3073\u8cea\u7591\u5fdc\u7b54 (2)<\/b>\u300014:30\uff5e15:30
\n\u8b1b\u6f14\u8005\uff1a<\/b>\u5c71\ufa11 \u7d17\u7d00\u5b50 (YAMASAKI, Sakiko)<\/p>\n
\u30bf\u30a4\u30c8\u30eb\uff1a<\/b>An attempt at a new embedding of intuitionistic logic into linear logic\uff0dvia multi-succedent G3-style sequent calculus for intuitionistic logic\uff0d References\uff1a<\/b>
\n\u30a2\u30d6\u30b9\u30c8\u30e9\u30af\u30c8\uff1a<\/b>In this presentation, I will examine the relationship between linear logic and G3-style sequent calculus for intuitionistic logic. It is well known that intuitionistic logic can be embedded into linear logic (Girard embedding). It is natural to do so, because intuitionistic logic can be embedded into modal logic S4 (G\u00f6del embedding), and the behavior of exponentials for linear logic (! and?) is similar to that of the modal operators for S4 (\u25a1<\/span> and \u25c7). Here, it is important for us (1) which system of intuitionistic logic is to be adopted, and (2) that the proof of the embedding is properly proof-theoretic one. For this purpose, we would like to employ the multi-succedent cut-free G3-style sequent calculus for intuitionistic logic: G3Int. I have already shown that we can establish the proof-theoretic proof for G\u00f6del embedding via G3Int. Now, how about Girard embedding? In this presentation, I will propose a new translation. And I shall investigate this matter. Furthermore, as far as I can, I will examine the relationship between G\u00f6del embedding and Girard embedding.<\/p>\n
\nA.S. Troelstra. Lectures on Linear Logic, CSLI-Lecture Notes 29, Center for the Study of Language and Information, Stanford, California, 1992.
\nA.S. Troelstra and H. Schwichtenberg. Basic Proof Theory. 2nd edn. Cambridge University Press, 2000.<\/p>\n\u4f1a\u3000\u5834 \/ Venue<\/h5>\n