DC Field | Value | Language |
---|---|---|
dc.contributor.author | Park, S | - |
dc.contributor.author | Im, H | - |
dc.date.accessioned | 2016-03-31T09:23:22Z | - |
dc.date.available | 2016-03-31T09:23:22Z | - |
dc.date.created | 2011-10-09 | - |
dc.date.issued | 2011-12 | - |
dc.identifier.issn | 0890-5401 | - |
dc.identifier.other | 2011-OAK-0000024199 | - |
dc.identifier.uri | https://oasis.postech.ac.kr/handle/2014.oak/17114 | - |
dc.description.abstract | In the proof-theoretic study of logic, the notion of normal proof has been understood and investigated as a metalogical property. Usually we formulate a system of logic, identify a class of proofs as normal proofs, and show that every proof in the system reduces to a corresponding normal proof. This paper develops a system of modal logic that is capable of expressing the notion of normal proof within the system itself, thereby making normal proofs an inherent property of the logic. Using a modality Delta to express the existence of a normal proof, the system provides a means for both recognizing and manipulating its own normal proofs. We develop the system as a sequent calculus with the implication connective superset of and the modality Delta, and prove the cut elimination theorem. From the sequent calculus, we derive two equivalent natural deduction systems. (C) 2011 Elsevier Inc. All rights reserved. | - |
dc.description.statementofresponsibility | X | - |
dc.language | English | - |
dc.publisher | Elsevier | - |
dc.relation.isPartOf | INFORMATION AND COMPUTATION | - |
dc.subject | Normal proof | - |
dc.subject | Modal logic | - |
dc.subject | Sequent calculus | - |
dc.subject | Natural deduction system | - |
dc.subject | Reflective system | - |
dc.title | A Modal Logic Internalizing Normal Proofs | - |
dc.type | Article | - |
dc.contributor.college | 컴퓨터공학과 | - |
dc.identifier.doi | 10.1016/J.IC.2010.09.010 | - |
dc.author.google | Park, S | - |
dc.author.google | Im, H | - |
dc.relation.volume | 209 | - |
dc.relation.issue | 12 | - |
dc.relation.startpage | 1519 | - |
dc.relation.lastpage | 1535 | - |
dc.contributor.id | 10165554 | - |
dc.relation.journal | INFORMATION AND COMPUTATION | - |
dc.relation.index | SCI급, SCOPUS 등재논문 | - |
dc.relation.sci | SCI | - |
dc.collections.name | Journal Papers | - |
dc.type.rims | ART | - |
dc.identifier.bibliographicCitation | INFORMATION AND COMPUTATION, v.209, no.12, pp.1519 - 1535 | - |
dc.identifier.wosid | 000297531300007 | - |
dc.date.tcdate | 2018-03-23 | - |
dc.citation.endPage | 1535 | - |
dc.citation.number | 12 | - |
dc.citation.startPage | 1519 | - |
dc.citation.title | INFORMATION AND COMPUTATION | - |
dc.citation.volume | 209 | - |
dc.contributor.affiliatedAuthor | Park, S | - |
dc.identifier.scopusid | 2-s2.0-81155148137 | - |
dc.description.journalClass | 1 | - |
dc.description.journalClass | 1 | - |
dc.description.scptc | 0 | * |
dc.date.scptcdate | 2018-05-121 | * |
dc.type.docType | Article | - |
dc.subject.keywordAuthor | Normal proof | - |
dc.subject.keywordAuthor | Modal logic | - |
dc.subject.keywordAuthor | Sequent calculus | - |
dc.subject.keywordAuthor | Natural deduction system | - |
dc.subject.keywordAuthor | Reflective system | - |
dc.relation.journalWebOfScienceCategory | Computer Science, Theory & Methods | - |
dc.relation.journalWebOfScienceCategory | Mathematics, Applied | - |
dc.description.journalRegisteredClass | scie | - |
dc.description.journalRegisteredClass | scopus | - |
dc.relation.journalResearchArea | Computer Science | - |
dc.relation.journalResearchArea | Mathematics | - |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.
library@postech.ac.kr Tel: 054-279-2548
Copyrights © by 2017 Pohang University of Science ad Technology All right reserved.