InforLorV4, Istex, Corpus, bibRecord, 002662

Prefixed Tableau Systems for Logic of Proofs and Provability

Identifieur interne : 002662 ( Istex/Corpus ); précédent : 002661; suivant : 002663

Prefixed Tableau Systems for Logic of Proofs and Provability

Source :

Lecture Notes in Computer Science [ 0302-9743 ]

RBID : ISTEX:A3CA0681C9B628C718B6068A1CDF0792C81ABC1C

Abstract

Abstract: In this paper, we introduce prefixed tableau systems for logics combining Artemov’s logic of proofs, which is introduced in order to explore combinatorial structure of proofs, and the logic of provability (strong provability), which has been studied as a logic of formal provability (provability and truth) in arithmetic for decades. Such joint logics have already been studied, but no cut-free tableau systems for these logics have been available in the literature so far. We show the admissibility of cut for these systems via semantic completeness for cut-free prefixed tableau systems for these logics.

Url:

https://api.istex.fr/ark:/67375/HCB-VBMH15HS-4/fulltext.pdf

DOI: 10.1007/978-3-642-40537-2_18

Links to Exploration step

ISTEX:A3CA0681C9B628C718B6068A1CDF0792C81ABC1C

Le document en format XML

<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Prefixed Tableau Systems for Logic of Proofs and Provability</title>
<author><name sortKey="Kurokawa, Hidenori" sort="Kurokawa, Hidenori" uniqKey="Kurokawa H" first="Hidenori" last="Kurokawa">Hidenori Kurokawa</name>
<affiliation><mods:affiliation>Department of Information Science, Kobe University, Japan</mods:affiliation>
</affiliation>
<affiliation><mods:affiliation>E-mail: hidenori.kurokawa@gmail.com</mods:affiliation>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:A3CA0681C9B628C718B6068A1CDF0792C81ABC1C</idno>
<date when="2013" year="2013">2013</date>
<idno type="doi">10.1007/978-3-642-40537-2_18</idno>
<idno type="url">https://api.istex.fr/ark:/67375/HCB-VBMH15HS-4/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">002662</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002662</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Prefixed Tableau Systems for Logic of Proofs and Provability</title>
<author><name sortKey="Kurokawa, Hidenori" sort="Kurokawa, Hidenori" uniqKey="Kurokawa H" first="Hidenori" last="Kurokawa">Hidenori Kurokawa</name>
<affiliation><mods:affiliation>Department of Information Science, Kobe University, Japan</mods:affiliation>
</affiliation>
<affiliation><mods:affiliation>E-mail: hidenori.kurokawa@gmail.com</mods:affiliation>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title>
<idno type="ISSN">0302-9743</idno>
<idno type="eISSN">1611-3349</idno>
<idno type="ISSN">0302-9743</idno>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><idno type="ISSN">0302-9743</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass></textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Abstract: In this paper, we introduce prefixed tableau systems for logics combining Artemov’s logic of proofs, which is introduced in order to explore combinatorial structure of proofs, and the logic of provability (strong provability), which has been studied as a logic of formal provability (provability and truth) in arithmetic for decades. Such joint logics have already been studied, but no cut-free tableau systems for these logics have been available in the literature so far. We show the admissibility of cut for these systems via semantic completeness for cut-free prefixed tableau systems for these logics.</div>
</front>
</TEI>
<istex><corpusName>springer-ebooks</corpusName>
<author><json:item><name>Hidenori Kurokawa</name>
<affiliations><json:string>Department of Information Science, Kobe University, Japan</json:string>
<json:string>E-mail: hidenori.kurokawa@gmail.com</json:string>
</affiliations>
</json:item>
</author>
<subject><json:item><lang><json:string>eng</json:string>
</lang>
<value>prefixed tableau system</value>
</json:item>
<json:item><lang><json:string>eng</json:string>
</lang>
<value>logic of proofs</value>
</json:item>
<json:item><lang><json:string>eng</json:string>
</lang>
<value>provability logic</value>
</json:item>
</subject>
<arkIstex>ark:/67375/HCB-VBMH15HS-4</arkIstex>
<language><json:string>eng</json:string>
</language>
<originalGenre><json:string>OriginalPaper</json:string>
</originalGenre>
<abstract>Abstract: In this paper, we introduce prefixed tableau systems for logics combining Artemov’s logic of proofs, which is introduced in order to explore combinatorial structure of proofs, and the logic of provability (strong provability), which has been studied as a logic of formal provability (provability and truth) in arithmetic for decades. Such joint logics have already been studied, but no cut-free tableau systems for these logics have been available in the literature so far. We show the admissibility of cut for these systems via semantic completeness for cut-free prefixed tableau systems for these logics.</abstract>
<qualityIndicators><refBibsNative>false</refBibsNative>
<abstractWordCount>94</abstractWordCount>
<abstractCharCount>616</abstractCharCount>
<keywordCount>3</keywordCount>
<score>8.128</score>
<pdfWordCount>8361</pdfWordCount>
<pdfCharCount>34236</pdfCharCount>
<pdfVersion>1.6</pdfVersion>
<pdfPageCount>16</pdfPageCount>
<pdfPageSize>439.363 x 666.131 pts</pdfPageSize>
</qualityIndicators>
<title>Prefixed Tableau Systems for Logic of Proofs and Provability</title>
<chapterId><json:string>18</json:string>
<json:string>Chap18</json:string>
</chapterId>
<genre><json:string>conference</json:string>
</genre>
<serie><title>Lecture Notes in Computer Science</title>
<language><json:string>unknown</json:string>
</language>
<copyrightDate>2013</copyrightDate>
<issn><json:string>0302-9743</json:string>
</issn>
<eissn><json:string>1611-3349</json:string>
</eissn>
<editor><json:item><name>David Hutchison</name>
<affiliations><json:string>Lancaster University, Lancaster, UK</json:string>
</affiliations>
</json:item>
<json:item><name>Takeo Kanade</name>
<affiliations><json:string>Carnegie Mellon University, Pittsburgh, PA, USA</json:string>
</affiliations>
</json:item>
<json:item><name>Josef Kittler</name>
<affiliations><json:string>University of Surrey, Guildford, UK</json:string>
</affiliations>
</json:item>
<json:item><name>Jon M. Kleinberg</name>
<affiliations><json:string>Cornell University, Ithaca, NY, USA</json:string>
</affiliations>
</json:item>
<json:item><name>Friedemann Mattern</name>
<affiliations><json:string>ETH Zurich, Zurich, Switzerland</json:string>
</affiliations>
</json:item>
<json:item><name>John C. Mitchell</name>
<affiliations><json:string>Stanford University, Stanford, CA, USA</json:string>
</affiliations>
</json:item>
<json:item><name>Moni Naor</name>
<affiliations><json:string>Weizmann Institute of Science, Rehovot, Israel</json:string>
</affiliations>
</json:item>
<json:item><name>Oscar Nierstrasz</name>
<affiliations><json:string>University of Bern, Bern, Switzerland</json:string>
</affiliations>
</json:item>
<json:item><name>C. Pandu Rangan</name>
<affiliations><json:string>Indian Institute of Technology, Madras, India</json:string>
</affiliations>
</json:item>
<json:item><name>Bernhard Steffen</name>
<affiliations><json:string>University of Dortmund, Dortmund, Germany</json:string>
</affiliations>
</json:item>
<json:item><name>Madhu Sudan</name>
<affiliations><json:string>Massachusetts Institute of Technology, MA, USA</json:string>
</affiliations>
</json:item>
<json:item><name>Demetri Terzopoulos</name>
<affiliations><json:string>University of California, Los Angeles, CA, USA</json:string>
</affiliations>
</json:item>
<json:item><name>Doug Tygar</name>
<affiliations><json:string>University of California, Berkeley, CA, USA</json:string>
</affiliations>
</json:item>
<json:item><name>Moshe Y. Vardi</name>
<affiliations><json:string>Rice University, Houston, TX, USA</json:string>
</affiliations>
</json:item>
<json:item><name>Gerhard Weikum</name>
<affiliations><json:string>Max-Planck Institute of Computer Science, Saarbrücken, Germany</json:string>
</affiliations>
</json:item>
</editor>
</serie>
<host><title>Automated Reasoning with Analytic Tableaux and Related Methods</title>
<language><json:string>unknown</json:string>
</language>
<copyrightDate>2013</copyrightDate>
<doi><json:string>10.1007/978-3-642-40537-2</json:string>
</doi>
<issn><json:string>0302-9743</json:string>
</issn>
<eissn><json:string>1611-3349</json:string>
</eissn>
<eisbn><json:string>978-3-642-40537-2</json:string>
</eisbn>
<bookId><json:string>978-3-642-40537-2</json:string>
</bookId>
<isbn><json:string>978-3-642-40536-5</json:string>
</isbn>
<volume>8123</volume>
<pages><first>203</first>
<last>218</last>
</pages>
<genre><json:string>book-series</json:string>
</genre>
<editor><json:item><name>Didier Galmiche</name>
<affiliations><json:string>LORIA UMR CNRS 7503, Université de Lorraine, Campus Scientifique, BP 239, 54506, Vandœuvre-lès-Nancy, France</json:string>
<json:string>E-mail: didier.galmiche@loria.fr</json:string>
</affiliations>
</json:item>
<json:item><name>Dominique Larchey-Wendling</name>
<affiliations><json:string>LORIA – CNRS, UHP Nancy, Campus Scientifique, BP 239, 54 506, Vandœuvre-lès-Nancy, France</json:string>
<json:string>E-mail: dominique.larchey-wendling@loria.fr</json:string>
</affiliations>
</json:item>
</editor>
<subject><json:item><value>Computer Science</value>
</json:item>
<json:item><value>Computer Science</value>
</json:item>
<json:item><value>Artificial Intelligence (incl. Robotics)</value>
</json:item>
<json:item><value>Mathematical Logic and Formal Languages</value>
</json:item>
<json:item><value>Programming Techniques</value>
</json:item>
<json:item><value>Software Engineering</value>
</json:item>
<json:item><value>Discrete Mathematics in Computer Science</value>
</json:item>
<json:item><value>Logics and Meanings of Programs</value>
</json:item>
</subject>
</host>
<ark><json:string>ark:/67375/HCB-VBMH15HS-4</json:string>
</ark>
<publicationDate>2013</publicationDate>
<copyrightDate>2013</copyrightDate>
<doi><json:string>10.1007/978-3-642-40537-2_18</json:string>
</doi>
<id>A3CA0681C9B628C718B6068A1CDF0792C81ABC1C</id>
<score>1</score>
<fulltext><json:item><extension>pdf</extension>
<original>true</original>
<mimetype>application/pdf</mimetype>
<uri>https://api.istex.fr/ark:/67375/HCB-VBMH15HS-4/fulltext.pdf</uri>
</json:item>
<json:item><extension>zip</extension>
<original>false</original>
<mimetype>application/zip</mimetype>
<uri>https://api.istex.fr/ark:/67375/HCB-VBMH15HS-4/bundle.zip</uri>
</json:item>
<istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/HCB-VBMH15HS-4/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Prefixed Tableau Systems for Logic of Proofs and Provability</title>
</titleStmt>
<publicationStmt><authority>ISTEX</authority>
<availability><licence>Springer-Verlag Berlin Heidelberg</licence>
</availability>
<date when="2013">2013</date>
</publicationStmt>
<notesStmt><note type="conference" source="proceedings" scheme="https://content-type.data.istex.fr/ark:/67375/XTP-BFHXPBJJ-3">conference</note>
<note type="publication-type" subtype="book-series" scheme="https://publication-type.data.istex.fr/ark:/67375/JMC-0G6R5W5T-Z">book-series</note>
</notesStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Prefixed Tableau Systems for Logic of Proofs and Provability</title>
<author><persName><forename type="first">Hidenori</forename>
<surname>Kurokawa</surname>
</persName>
<email>hidenori.kurokawa@gmail.com</email>
<affiliation><idno type="GRID" subtype="Institution">grid.31432.37</idno>
<idno type="ISNI" subtype="Institution">0000000110923077</idno>
<orgName type="department">Department of Information Science</orgName>
<orgName type="institution">Kobe University</orgName>
<address><country key="JP">JAPAN</country>
</address>
</affiliation>
</author>
<idno type="istex">A3CA0681C9B628C718B6068A1CDF0792C81ABC1C</idno>
<idno type="ark">ark:/67375/HCB-VBMH15HS-4</idno>
<idno type="DOI">10.1007/978-3-642-40537-2_18</idno>
</analytic>
<monogr><title level="m" type="main">Automated Reasoning with Analytic Tableaux and Related Methods</title>
<title level="m" type="sub">22nd International Conference, TABLEAUX 2013, Nancy, France, September 16-19, 2013, Proceedings</title>
<title level="m" type="part">Research Papers</title>
<idno type="DOI">10.1007/978-3-642-40537-2</idno>
<idno type="book-id">978-3-642-40537-2</idno>
<idno type="ISBN">978-3-642-40536-5</idno>
<idno type="eISBN">978-3-642-40537-2</idno>
<idno type="chapter-id">Chap18</idno>
<idno type="part-id">Part2</idno>
<editor><persName><forename type="first">Didier</forename>
<surname>Galmiche</surname>
</persName>
<email>didier.galmiche@loria.fr</email>
<affiliation><idno type="GRID" subtype="Institution">grid.29172.3f</idno>
<idno type="ISNI" subtype="Institution">0000000121946418</idno>
<orgName type="department">LORIA UMR CNRS 7503</orgName>
<orgName type="institution">Université de Lorraine</orgName>
<address><street>Campus Scientifique</street>
<postBox>BP 239</postBox>
<postCode>54506</postCode>
<settlement>Vandœuvre-lès-Nancy</settlement>
<country key="FR">FRANCE</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">Dominique</forename>
<surname>Larchey-Wendling</surname>
</persName>
<email>dominique.larchey-wendling@loria.fr</email>
<affiliation><orgName type="department">LORIA – CNRS</orgName>
<orgName type="institution">UHP Nancy</orgName>
<address><street>Campus Scientifique</street>
<postBox>BP 239</postBox>
<postCode>54 506</postCode>
<settlement>Vandœuvre-lès-Nancy</settlement>
<country key="FR">FRANCE</country>
</address>
</affiliation>
</editor>
<meeting><title type="name">International Conference on Automated Reasoning with Analytic Tableaux and Related Methods</title>
<title type="abbr">TABLEAUX</title>
<idno type="conf-number">22</idno>
<idno type="Springer">tableaux</idno>
<idno type="DBLP">tableaux</idno>
<idno type="conf-ID">tableaux2013</idno>
<settlement>Nancy</settlement>
<country>France</country>
<date from="20130916" to="20130919"></date>
</meeting>
<imprint><biblScope unit="vol">8123</biblScope>
<biblScope unit="page" from="203">203</biblScope>
<biblScope unit="page" to="218">218</biblScope>
<biblScope unit="chapter-count">23</biblScope>
<biblScope unit="part-chapter-count">20</biblScope>
</imprint>
</monogr>
<series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title>
<editor><persName><forename type="first">David</forename>
<surname>Hutchison</surname>
</persName>
<affiliation><idno type="GRID" subtype="Institution">grid.9835.7</idno>
<idno type="ISNI" subtype="Institution">0000000081906402</idno>
<orgName type="institution">Lancaster University</orgName>
<address><settlement>Lancaster</settlement>
<country key="GB">UNITED KINGDOM</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">Takeo</forename>
<surname>Kanade</surname>
</persName>
<affiliation><idno type="GRID" subtype="Institution">grid.147455.6</idno>
<idno type="ISNI" subtype="Institution">0000000120970344</idno>
<orgName type="institution">Carnegie Mellon University</orgName>
<address><settlement>Pittsburgh</settlement>
<region>PA</region>
<country key="US">UNITED STATES</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">Josef</forename>
<surname>Kittler</surname>
</persName>
<affiliation><idno type="GRID" subtype="Institution">grid.5475.3</idno>
<idno type="ISNI" subtype="Institution">0000000404074824</idno>
<orgName type="institution">University of Surrey</orgName>
<address><settlement>Guildford</settlement>
<country key="GB">UNITED KINGDOM</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">Jon</forename>
<forename type="first">M.</forename>
<surname>Kleinberg</surname>
</persName>
<affiliation><idno type="GRID" subtype="Institution">grid.5386.8</idno>
<idno type="ISNI" subtype="Institution">000000041936877X</idno>
<orgName type="institution">Cornell University</orgName>
<address><settlement>Ithaca</settlement>
<region>NY</region>
<country key="US">UNITED STATES</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">Friedemann</forename>
<surname>Mattern</surname>
</persName>
<affiliation><idno type="GRID" subtype="Institution">grid.5801.c</idno>
<idno type="ISNI" subtype="Institution">0000000121562780</idno>
<orgName type="institution">ETH Zurich</orgName>
<address><settlement>Zurich</settlement>
<country key="CH">SWITZERLAND</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">John</forename>
<forename type="first">C.</forename>
<surname>Mitchell</surname>
</persName>
<affiliation><idno type="GRID" subtype="Institution">grid.168010.e</idno>
<idno type="ISNI" subtype="Institution">0000000419368956</idno>
<orgName type="institution">Stanford University</orgName>
<address><settlement>Stanford</settlement>
<region>CA</region>
<country key="US">UNITED STATES</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">Moni</forename>
<surname>Naor</surname>
</persName>
<affiliation><idno type="GRID" subtype="Institution">grid.13992.30</idno>
<idno type="ISNI" subtype="Institution">0000000406047563</idno>
<orgName type="institution">Weizmann Institute of Science</orgName>
<address><settlement>Rehovot</settlement>
<country key="IL">ISRAEL</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">Oscar</forename>
<surname>Nierstrasz</surname>
</persName>
<affiliation><idno type="GRID" subtype="Institution">grid.5734.5</idno>
<idno type="ISNI" subtype="Institution">0000000107265157</idno>
<orgName type="institution">University of Bern</orgName>
<address><settlement>Bern</settlement>
<country key="CH">SWITZERLAND</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">C.</forename>
<surname>Pandu Rangan</surname>
</persName>
<affiliation><idno type="GRID" subtype="Institution">grid.417969.4</idno>
<idno type="ISNI" subtype="Institution">0000000123151926</idno>
<orgName type="institution">Indian Institute of Technology</orgName>
<address><settlement>Madras</settlement>
<country key="IN">INDIA</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">Bernhard</forename>
<surname>Steffen</surname>
</persName>
<affiliation><idno type="GRID" subtype="Institution">grid.5675.1</idno>
<idno type="ISNI" subtype="Institution">0000000104169637</idno>
<orgName type="institution">University of Dortmund</orgName>
<address><settlement>Dortmund</settlement>
<country key="DE">GERMANY</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">Madhu</forename>
<surname>Sudan</surname>
</persName>
<affiliation><idno type="GRID" subtype="Institution">grid.116068.8</idno>
<idno type="ISNI" subtype="Institution">0000000123412786</idno>
<orgName type="institution">Massachusetts Institute of Technology</orgName>
<address><region>MA</region>
<country key="US">UNITED STATES</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">Demetri</forename>
<surname>Terzopoulos</surname>
</persName>
<affiliation><idno type="GRID" subtype="Institution">grid.19006.3e</idno>
<idno type="ISNI" subtype="Institution">0000000096326718</idno>
<orgName type="institution">University of California</orgName>
<address><settlement>Los Angeles</settlement>
<region>CA</region>
<country key="US">UNITED STATES</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">Doug</forename>
<surname>Tygar</surname>
</persName>
<affiliation><idno type="GRID" subtype="Institution">grid.47840.3f</idno>
<idno type="ISNI" subtype="Institution">0000000121817878</idno>
<orgName type="institution">University of California</orgName>
<address><settlement>Berkeley</settlement>
<region>CA</region>
<country key="US">UNITED STATES</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">Moshe</forename>
<forename type="first">Y.</forename>
<surname>Vardi</surname>
</persName>
<affiliation><idno type="GRID" subtype="Institution">grid.21940.3e</idno>
<idno type="ISNI" subtype="Institution">	0000000419368278</idno>
<orgName type="institution">Rice University</orgName>
<address><settlement>Houston</settlement>
<region>TX</region>
<country key="US">UNITED STATES</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">Gerhard</forename>
<surname>Weikum</surname>
</persName>
<affiliation><idno type="GRID" subtype="Institution">grid.419607.d</idno>
<idno type="ISNI" subtype="Institution">0000000120969941</idno>
<orgName type="institution">Max-Planck Institute of Computer Science</orgName>
<address><settlement>Saarbrücken</settlement>
<country key="DE">GERMANY</country>
</address>
</affiliation>
</editor>
<idno type="pISSN">0302-9743</idno>
<idno type="eISSN">1611-3349</idno>
<idno type="seriesID">558</idno>
</series>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><abstract xml:lang="en"><head>Abstract</head>
<p>In this paper, we introduce prefixed tableau systems for logics combining Artemov’s logic of proofs, which is introduced in order to explore combinatorial structure of proofs, and the logic of provability (strong provability), which has been studied as a logic of formal provability (provability and truth) in arithmetic for decades. Such joint logics have already been studied, but no cut-free tableau systems for these logics have been available in the literature so far. We show the admissibility of cut for these systems via semantic completeness for cut-free prefixed tableau systems for these logics.</p>
</abstract>
<textClass ana="keyword"><keywords xml:lang="en"><term>prefixed tableau system</term>
<term>logic of proofs</term>
<term>provability logic</term>
</keywords>
</textClass>
<textClass ana="subject"><keywords scheme="book-subject-collection"><list><label>SUCO11645</label>
<item><term>Computer Science</term>
</item>
</list>
</keywords>
</textClass>
<textClass ana="subject"><keywords scheme="book-subject"><list><label>SCI</label>
<item><term type="Primary">Computer Science</term>
</item>
<label>SCI21017</label>
<item><term type="Secondary" subtype="priority-1">Artificial Intelligence (incl. Robotics)</term>
</item>
<label>SCI16048</label>
<item><term type="Secondary" subtype="priority-2">Mathematical Logic and Formal Languages</term>
</item>
<label>SCI14010</label>
<item><term type="Secondary" subtype="priority-3">Programming Techniques</term>
</item>
<label>SCI14029</label>
<item><term type="Secondary" subtype="priority-4">Software Engineering</term>
</item>
<label>SCI17028</label>
<item><term type="Secondary" subtype="priority-5">Discrete Mathematics in Computer Science</term>
</item>
<label>SCI1603X</label>
<item><term type="Secondary" subtype="priority-6">Logics and Meanings of Programs</term>
</item>
</list>
</keywords>
</textClass>
<langUsage><language ident="EN"></language>
</langUsage>
</profileDesc>
</teiHeader>
</istex:fulltextTEI>
<json:item><extension>txt</extension>
<original>false</original>
<mimetype>text/plain</mimetype>
<uri>https://api.istex.fr/ark:/67375/HCB-VBMH15HS-4/fulltext.txt</uri>
</json:item>
</fulltext>
<metadata><istex:metadataXml wicri:clean="corpus springer-ebooks not found" wicri:toSee="no header"><istex:xmlDeclaration>version="1.0" encoding="UTF-8"</istex:xmlDeclaration>
<istex:docType PUBLIC="-//Springer-Verlag//DTD A++ V2.4//EN" URI="http://devel.springer.de/A++/V2.4/DTD/A++V2.4.dtd" name="istex:docType"></istex:docType>
<istex:document><Publisher><PublisherInfo><PublisherName>Springer Berlin Heidelberg</PublisherName>
<PublisherLocation>Berlin, Heidelberg</PublisherLocation>
<PublisherImprintName>Springer</PublisherImprintName>
</PublisherInfo>
<Series><SeriesInfo ID="Series558" SeriesType="Series" TocLevels="0"><SeriesID>558</SeriesID>
<SeriesPrintISSN>0302-9743</SeriesPrintISSN>
<SeriesElectronicISSN>1611-3349</SeriesElectronicISSN>
<SeriesTitle Language="En">Lecture Notes in Computer Science</SeriesTitle>
</SeriesInfo>
<SeriesHeader><EditorGroup><Editor AffiliationIDS="Aff1"><EditorName DisplayOrder="Western"><GivenName>David</GivenName>
<FamilyName>Hutchison</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff2"><EditorName DisplayOrder="Western"><GivenName>Takeo</GivenName>
<FamilyName>Kanade</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff3"><EditorName DisplayOrder="Western"><GivenName>Josef</GivenName>
<FamilyName>Kittler</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff4"><EditorName DisplayOrder="Western"><GivenName>Jon</GivenName>
<GivenName>M.</GivenName>
<FamilyName>Kleinberg</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff5"><EditorName DisplayOrder="Western"><GivenName>Friedemann</GivenName>
<FamilyName>Mattern</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff6"><EditorName DisplayOrder="Western"><GivenName>John</GivenName>
<GivenName>C.</GivenName>
<FamilyName>Mitchell</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff7"><EditorName DisplayOrder="Western"><GivenName>Moni</GivenName>
<FamilyName>Naor</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff8"><EditorName DisplayOrder="Western"><GivenName>Oscar</GivenName>
<FamilyName>Nierstrasz</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff9"><EditorName DisplayOrder="Western"><GivenName>C.</GivenName>
<FamilyName>Pandu Rangan</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff10"><EditorName DisplayOrder="Western"><GivenName>Bernhard</GivenName>
<FamilyName>Steffen</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff11"><EditorName DisplayOrder="Western"><GivenName>Madhu</GivenName>
<FamilyName>Sudan</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff12"><EditorName DisplayOrder="Western"><GivenName>Demetri</GivenName>
<FamilyName>Terzopoulos</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff13"><EditorName DisplayOrder="Western"><GivenName>Doug</GivenName>
<FamilyName>Tygar</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff14"><EditorName DisplayOrder="Western"><GivenName>Moshe</GivenName>
<GivenName>Y.</GivenName>
<FamilyName>Vardi</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff15"><EditorName DisplayOrder="Western"><GivenName>Gerhard</GivenName>
<FamilyName>Weikum</FamilyName>
</EditorName>
</Editor>
<Affiliation ID="Aff1"><OrgID Level="Institution" Type="GRID">grid.9835.7</OrgID>
<OrgID Level="Institution" Type="ISNI">0000000081906402</OrgID>
<OrgName>Lancaster University</OrgName>
<OrgAddress><City>Lancaster</City>
<Country>UK</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff2"><OrgID Level="Institution" Type="GRID">grid.147455.6</OrgID>
<OrgID Level="Institution" Type="ISNI">0000000120970344</OrgID>
<OrgName>Carnegie Mellon University</OrgName>
<OrgAddress><City>Pittsburgh</City>
<State>PA</State>
<Country>USA</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff3"><OrgID Level="Institution" Type="GRID">grid.5475.3</OrgID>
<OrgID Level="Institution" Type="ISNI">0000000404074824</OrgID>
<OrgName>University of Surrey</OrgName>
<OrgAddress><City>Guildford</City>
<Country>UK</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff4"><OrgID Level="Institution" Type="GRID">grid.5386.8</OrgID>
<OrgID Level="Institution" Type="ISNI">000000041936877X</OrgID>
<OrgName>Cornell University</OrgName>
<OrgAddress><City>Ithaca</City>
<State>NY</State>
<Country>USA</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff5"><OrgID Level="Institution" Type="GRID">grid.5801.c</OrgID>
<OrgID Level="Institution" Type="ISNI">0000000121562780</OrgID>
<OrgName>ETH Zurich</OrgName>
<OrgAddress><City>Zurich</City>
<Country>Switzerland</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff6"><OrgID Level="Institution" Type="GRID">grid.168010.e</OrgID>
<OrgID Level="Institution" Type="ISNI">0000000419368956</OrgID>
<OrgName>Stanford University</OrgName>
<OrgAddress><City>Stanford</City>
<State>CA</State>
<Country>USA</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff7"><OrgID Level="Institution" Type="GRID">grid.13992.30</OrgID>
<OrgID Level="Institution" Type="ISNI">0000000406047563</OrgID>
<OrgName>Weizmann Institute of Science</OrgName>
<OrgAddress><City>Rehovot</City>
<Country>Israel</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff8"><OrgID Level="Institution" Type="GRID">grid.5734.5</OrgID>
<OrgID Level="Institution" Type="ISNI">0000000107265157</OrgID>
<OrgName>University of Bern</OrgName>
<OrgAddress><City>Bern</City>
<Country>Switzerland</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff9"><OrgID Level="Institution" Type="GRID">grid.417969.4</OrgID>
<OrgID Level="Institution" Type="ISNI">0000000123151926</OrgID>
<OrgName>Indian Institute of Technology</OrgName>
<OrgAddress><City>Madras</City>
<Country>India</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff10"><OrgID Level="Institution" Type="GRID">grid.5675.1</OrgID>
<OrgID Level="Institution" Type="ISNI">0000000104169637</OrgID>
<OrgName>University of Dortmund</OrgName>
<OrgAddress><City>Dortmund</City>
<Country>Germany</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff11"><OrgID Level="Institution" Type="GRID">grid.116068.8</OrgID>
<OrgID Level="Institution" Type="ISNI">0000000123412786</OrgID>
<OrgName>Massachusetts Institute of Technology</OrgName>
<OrgAddress><State>MA</State>
<Country>USA</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff12"><OrgID Level="Institution" Type="GRID">grid.19006.3e</OrgID>
<OrgID Level="Institution" Type="ISNI">0000000096326718</OrgID>
<OrgName>University of California</OrgName>
<OrgAddress><City>Los Angeles</City>
<State>CA</State>
<Country>USA</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff13"><OrgID Level="Institution" Type="GRID">grid.47840.3f</OrgID>
<OrgID Level="Institution" Type="ISNI">0000000121817878</OrgID>
<OrgName>University of California</OrgName>
<OrgAddress><City>Berkeley</City>
<State>CA</State>
<Country>USA</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff14"><OrgID Level="Institution" Type="GRID">grid.21940.3e</OrgID>
<OrgID Level="Institution" Type="ISNI">	0000000419368278</OrgID>
<OrgName>Rice University</OrgName>
<OrgAddress><City>Houston</City>
<State>TX</State>
<Country>USA</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff15"><OrgID Level="Institution" Type="GRID">grid.419607.d</OrgID>
<OrgID Level="Institution" Type="ISNI">0000000120969941</OrgID>
<OrgName>Max-Planck Institute of Computer Science</OrgName>
<OrgAddress><City>Saarbrücken</City>
<Country>Germany</Country>
</OrgAddress>
</Affiliation>
</EditorGroup>
</SeriesHeader>
<SubSeries><SubSeriesInfo><SubSeriesID>1244</SubSeriesID>
<SubSeriesPrintISSN>0302-9743</SubSeriesPrintISSN>
<SubSeriesElectronicISSN>1611-3349</SubSeriesElectronicISSN>
<SubSeriesTitle Language="En">Lecture Notes in Artificial Intelligence</SubSeriesTitle>
</SubSeriesInfo>
<SubSeriesHeader><EditorGroup><Editor AffiliationIDS="Aff16"><EditorName DisplayOrder="Western"><GivenName>Randy</GivenName>
<FamilyName>Goebel</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff17"><EditorName DisplayOrder="Western"><GivenName>Jörg</GivenName>
<FamilyName>Siekmann</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff18"><EditorName DisplayOrder="Western"><GivenName>Wolfgang</GivenName>
<FamilyName>Wahlster</FamilyName>
</EditorName>
</Editor>
<Affiliation ID="Aff16"><OrgID Level="Institution" Type="GRID">grid.17089.37</OrgID>
<OrgName>University of Alberta</OrgName>
<OrgAddress><City>Edmonton</City>
<Country>Canada</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff17"><OrgID Level="Institution" Type="GRID">grid.11749.3a</OrgID>
<OrgID Level="Institution" Type="ISNI">0000000121677588</OrgID>
<OrgName>University of Saarland</OrgName>
<OrgAddress><City>Saarbrücken</City>
<Country>Germany</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff18"><OrgID Level="Institution" Type="GRID">grid.11749.3a</OrgID>
<OrgID Level="Institution" Type="ISNI">0000000121677588</OrgID>
<OrgName>DFKI and University of Saarland</OrgName>
<OrgAddress><City>Saarbrücken</City>
<Country>Germany</Country>
</OrgAddress>
</Affiliation>
</EditorGroup>
</SubSeriesHeader>
</SubSeries>
<Book Language="En"><BookInfo BookProductType="Proceedings" ContainsESM="No" Language="En" MediaType="eBook" NumberingDepth="2" NumberingStyle="ContentOnly" OutputMedium="All" TocLevels="0"><BookID>978-3-642-40537-2</BookID>
<BookTitle>Automated Reasoning with Analytic Tableaux and Related Methods</BookTitle>
<BookSubTitle>22nd International Conference, TABLEAUX 2013, Nancy, France, September 16-19, 2013, Proceedings</BookSubTitle>
<BookVolumeNumber>8123</BookVolumeNumber>
<BookSequenceNumber>8123</BookSequenceNumber>
<BookDOI>10.1007/978-3-642-40537-2</BookDOI>
<BookTitleID>318556</BookTitleID>
<BookPrintISBN>978-3-642-40536-5</BookPrintISBN>
<BookElectronicISBN>978-3-642-40537-2</BookElectronicISBN>
<BookChapterCount>23</BookChapterCount>
<BookCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName>
<CopyrightYear>2013</CopyrightYear>
</BookCopyright>
<BookSubjectGroup><BookSubject Code="SCI" Type="Primary">Computer Science</BookSubject>
<BookSubject Code="SCI21017" Priority="1" Type="Secondary">Artificial Intelligence (incl. Robotics)</BookSubject>
<BookSubject Code="SCI16048" Priority="2" Type="Secondary">Mathematical Logic and Formal Languages</BookSubject>
<BookSubject Code="SCI14010" Priority="3" Type="Secondary">Programming Techniques</BookSubject>
<BookSubject Code="SCI14029" Priority="4" Type="Secondary">Software Engineering</BookSubject>
<BookSubject Code="SCI17028" Priority="5" Type="Secondary">Discrete Mathematics in Computer Science</BookSubject>
<BookSubject Code="SCI1603X" Priority="6" Type="Secondary">Logics and Meanings of Programs</BookSubject>
<SubjectCollection Code="SUCO11645">Computer Science</SubjectCollection>
</BookSubjectGroup>
<BookContext><SeriesID>558</SeriesID>
<SubSeriesID>1244</SubSeriesID>
</BookContext>
<ConferenceInfo><ConfSeriesName>International Conference on Automated Reasoning with Analytic Tableaux and Related Methods</ConfSeriesName>
<ConfSeriesID Type="Springer">tableaux</ConfSeriesID>
<ConfSeriesID Type="DBLP">tableaux</ConfSeriesID>
<ConfEventID Type="Springer">tableaux2013</ConfEventID>
<ConfEventAbbreviation>TABLEAUX</ConfEventAbbreviation>
<ConfNumber>22</ConfNumber>
<ConfEventLocation><City>Nancy</City>
<Country>France</Country>
</ConfEventLocation>
<ConfEventDateStart><Year>2013</Year>
<Month>9</Month>
<Day>16</Day>
</ConfEventDateStart>
<ConfEventDateEnd><Year>2013</Year>
<Month>9</Month>
<Day>19</Day>
</ConfEventDateEnd>
</ConferenceInfo>
</BookInfo>
<BookHeader><EditorGroup><Editor AffiliationIDS="Aff19"><EditorName DisplayOrder="Western"><GivenName>Didier</GivenName>
<FamilyName>Galmiche</FamilyName>
</EditorName>
<Contact><Email>didier.galmiche@loria.fr</Email>
</Contact>
</Editor>
<Editor AffiliationIDS="Aff20"><EditorName DisplayOrder="Western"><GivenName>Dominique</GivenName>
<FamilyName>Larchey-Wendling</FamilyName>
</EditorName>
<Contact><Email>dominique.larchey-wendling@loria.fr</Email>
</Contact>
</Editor>
<Affiliation ID="Aff19"><OrgID Level="Institution" Type="GRID">grid.29172.3f</OrgID>
<OrgID Level="Institution" Type="ISNI">0000000121946418</OrgID>
<OrgDivision>LORIA UMR CNRS 7503</OrgDivision>
<OrgName>Université de Lorraine</OrgName>
<OrgAddress><Street>Campus Scientifique</Street>
<Postbox>BP 239</Postbox>
<Postcode>54506</Postcode>
<City>Vandœuvre-lès-Nancy</City>
<Country>France</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff20"><OrgDivision>LORIA – CNRS</OrgDivision>
<OrgName>UHP Nancy</OrgName>
<OrgAddress><Street>Campus Scientifique</Street>
<Postbox>BP 239</Postbox>
<Postcode>54 506</Postcode>
<City>Vandœuvre-lès-Nancy</City>
<Country>France</Country>
</OrgAddress>
</Affiliation>
</EditorGroup>
</BookHeader>
<Part ID="Part2"><PartInfo OutputMedium="All" TocLevels="0"><PartID>2</PartID>
<PartSequenceNumber>2</PartSequenceNumber>
<PartTitle>Research Papers</PartTitle>
<PartChapterCount>20</PartChapterCount>
<PartContext><SeriesID>558</SeriesID>
<BookID>978-3-642-40537-2</BookID>
<BookTitle>Automated Reasoning with Analytic Tableaux and Related Methods</BookTitle>
</PartContext>
</PartInfo>
<Chapter ID="Chap18" Language="En"><ChapterInfo ChapterType="OriginalPaper" ContainsESM="No" NumberingDepth="2" NumberingStyle="ContentOnly" TocLevels="0"><ChapterID>18</ChapterID>
<ChapterDOI>10.1007/978-3-642-40537-2_18</ChapterDOI>
<ChapterSequenceNumber>18</ChapterSequenceNumber>
<ChapterTitle Language="En">Prefixed Tableau Systems for Logic of Proofs and Provability</ChapterTitle>
<ChapterFirstPage>203</ChapterFirstPage>
<ChapterLastPage>218</ChapterLastPage>
<ChapterCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName>
<CopyrightYear>2013</CopyrightYear>
</ChapterCopyright>
<ChapterGrants Type="Regular"><MetadataGrant Grant="OpenAccess"></MetadataGrant>
<AbstractGrant Grant="OpenAccess"></AbstractGrant>
<BodyPDFGrant Grant="Restricted"></BodyPDFGrant>
<BodyHTMLGrant Grant="Restricted"></BodyHTMLGrant>
<BibliographyGrant Grant="Restricted"></BibliographyGrant>
<ESMGrant Grant="Restricted"></ESMGrant>
</ChapterGrants>
<ChapterContext><SeriesID>558</SeriesID>
<PartID>2</PartID>
<BookID>978-3-642-40537-2</BookID>
<BookTitle>Automated Reasoning with Analytic Tableaux and Related Methods</BookTitle>
</ChapterContext>
</ChapterInfo>
<ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff21"><AuthorName DisplayOrder="Western"><GivenName>Hidenori</GivenName>
<FamilyName>Kurokawa</FamilyName>
</AuthorName>
<Contact><Email>hidenori.kurokawa@gmail.com</Email>
</Contact>
</Author>
<Affiliation ID="Aff21"><OrgID Level="Institution" Type="GRID">grid.31432.37</OrgID>
<OrgID Level="Institution" Type="ISNI">0000000110923077</OrgID>
<OrgDivision>Department of Information Science</OrgDivision>
<OrgName>Kobe University</OrgName>
<OrgAddress><Country>Japan</Country>
</OrgAddress>
</Affiliation>
</AuthorGroup>
<Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading>
<Para>In this paper, we introduce prefixed tableau systems for logics combining Artemov’s logic of proofs, which is introduced in order to explore combinatorial structure of proofs, and the logic of provability (strong provability), which has been studied as a logic of formal provability (provability and truth) in arithmetic for decades. Such joint logics have already been studied, but no cut-free tableau systems for these logics have been available in the literature so far. We show the admissibility of cut for these systems via semantic completeness for cut-free prefixed tableau systems for these logics.</Para>
</Abstract>
<KeywordGroup Language="En"><Heading>Keywords</Heading>
<Keyword>prefixed tableau system</Keyword>
<Keyword>logic of proofs</Keyword>
<Keyword>provability logic</Keyword>
</KeywordGroup>
</ChapterHeader>
<NoBody></NoBody>
</Chapter>
</Part>
</Book>
</Series>
</Publisher>
<!-- Converted from LaTeX with LaTeX2A++ V3.1.52 --></istex:document>
</istex:metadataXml>
<mods version="3.6"><titleInfo lang="en"><title>Prefixed Tableau Systems for Logic of Proofs and Provability</title>
</titleInfo>
<titleInfo type="alternative" contentType="CDATA"><title>Prefixed Tableau Systems for Logic of Proofs and Provability</title>
</titleInfo>
<name type="personal"><namePart type="given">Hidenori</namePart>
<namePart type="family">Kurokawa</namePart>
<affiliation>Department of Information Science, Kobe University, Japan</affiliation>
<affiliation>E-mail: hidenori.kurokawa@gmail.com</affiliation>
<role><roleTerm type="text">author</roleTerm>
</role>
</name>
<typeOfResource>text</typeOfResource>
<genre displayLabel="OriginalPaper" authority="ISTEX" authorityURI="https://content-type.data.istex.fr" type="conference" valueURI="https://content-type.data.istex.fr/ark:/67375/XTP-BFHXPBJJ-3">conference</genre>
<originInfo><publisher>Springer Berlin Heidelberg</publisher>
<place><placeTerm type="text">Berlin, Heidelberg</placeTerm>
</place>
<dateIssued encoding="w3cdtf">2013</dateIssued>
<copyrightDate encoding="w3cdtf">2013</copyrightDate>
</originInfo>
<language><languageTerm type="code" authority="rfc3066">en</languageTerm>
<languageTerm type="code" authority="iso639-2b">eng</languageTerm>
</language>
<abstract lang="en">Abstract: In this paper, we introduce prefixed tableau systems for logics combining Artemov’s logic of proofs, which is introduced in order to explore combinatorial structure of proofs, and the logic of provability (strong provability), which has been studied as a logic of formal provability (provability and truth) in arithmetic for decades. Such joint logics have already been studied, but no cut-free tableau systems for these logics have been available in the literature so far. We show the admissibility of cut for these systems via semantic completeness for cut-free prefixed tableau systems for these logics.</abstract>
<subject lang="en"><genre>Keywords</genre>
<topic>prefixed tableau system</topic>
<topic>logic of proofs</topic>
<topic>provability logic</topic>
</subject>
<relatedItem type="host"><titleInfo><title>Automated Reasoning with Analytic Tableaux and Related Methods</title>
<subTitle>22nd International Conference, TABLEAUX 2013, Nancy, France, September 16-19, 2013, Proceedings</subTitle>
</titleInfo>
<name type="personal"><namePart type="given">Didier</namePart>
<namePart type="family">Galmiche</namePart>
<affiliation>LORIA UMR CNRS 7503, Université de Lorraine, Campus Scientifique, BP 239, 54506, Vandœuvre-lès-Nancy, France</affiliation>
<affiliation>E-mail: didier.galmiche@loria.fr</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Dominique</namePart>
<namePart type="family">Larchey-Wendling</namePart>
<affiliation>LORIA – CNRS, UHP Nancy, Campus Scientifique, BP 239, 54 506, Vandœuvre-lès-Nancy, France</affiliation>
<affiliation>E-mail: dominique.larchey-wendling@loria.fr</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<genre type="book-series" authority="ISTEX" authorityURI="https://publication-type.data.istex.fr" valueURI="https://publication-type.data.istex.fr/ark:/67375/JMC-0G6R5W5T-Z">book-series</genre>
<originInfo><publisher>Springer</publisher>
<copyrightDate encoding="w3cdtf">2013</copyrightDate>
<issuance>monographic</issuance>
</originInfo>
<subject><genre>Book-Subject-Collection</genre>
<topic authority="SpringerSubjectCodes" authorityURI="SUCO11645">Computer Science</topic>
</subject>
<subject><genre>Book-Subject-Group</genre>
<topic authority="SpringerSubjectCodes" authorityURI="SCI">Computer Science</topic>
<topic authority="SpringerSubjectCodes" authorityURI="SCI21017">Artificial Intelligence (incl. Robotics)</topic>
<topic authority="SpringerSubjectCodes" authorityURI="SCI16048">Mathematical Logic and Formal Languages</topic>
<topic authority="SpringerSubjectCodes" authorityURI="SCI14010">Programming Techniques</topic>
<topic authority="SpringerSubjectCodes" authorityURI="SCI14029">Software Engineering</topic>
<topic authority="SpringerSubjectCodes" authorityURI="SCI17028">Discrete Mathematics in Computer Science</topic>
<topic authority="SpringerSubjectCodes" authorityURI="SCI1603X">Logics and Meanings of Programs</topic>
</subject>
<identifier type="DOI">10.1007/978-3-642-40537-2</identifier>
<identifier type="ISBN">978-3-642-40536-5</identifier>
<identifier type="eISBN">978-3-642-40537-2</identifier>
<identifier type="ISSN">0302-9743</identifier>
<identifier type="eISSN">1611-3349</identifier>
<identifier type="BookTitleID">318556</identifier>
<identifier type="BookID">978-3-642-40537-2</identifier>
<identifier type="BookChapterCount">23</identifier>
<identifier type="BookVolumeNumber">8123</identifier>
<identifier type="BookSequenceNumber">8123</identifier>
<identifier type="PartChapterCount">20</identifier>
<part><date>2013</date>
<detail type="part"><title>Research Papers</title>
</detail>
<detail type="volume"><number>8123</number>
<caption>vol.</caption>
</detail>
<extent unit="pages"><start>203</start>
<end>218</end>
</extent>
</part>
<recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2013</recordOrigin>
</recordInfo>
</relatedItem>
<relatedItem type="series"><titleInfo><title>Lecture Notes in Computer Science</title>
</titleInfo>
<name type="personal"><namePart type="given">David</namePart>
<namePart type="family">Hutchison</namePart>
<affiliation>Lancaster University, Lancaster, UK</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Takeo</namePart>
<namePart type="family">Kanade</namePart>
<affiliation>Carnegie Mellon University, Pittsburgh, PA, USA</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Josef</namePart>
<namePart type="family">Kittler</namePart>
<affiliation>University of Surrey, Guildford, UK</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Jon</namePart>
<namePart type="given">M.</namePart>
<namePart type="family">Kleinberg</namePart>
<affiliation>Cornell University, Ithaca, NY, USA</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Friedemann</namePart>
<namePart type="family">Mattern</namePart>
<affiliation>ETH Zurich, Zurich, Switzerland</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">John</namePart>
<namePart type="given">C.</namePart>
<namePart type="family">Mitchell</namePart>
<affiliation>Stanford University, Stanford, CA, USA</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Moni</namePart>
<namePart type="family">Naor</namePart>
<affiliation>Weizmann Institute of Science, Rehovot, Israel</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Oscar</namePart>
<namePart type="family">Nierstrasz</namePart>
<affiliation>University of Bern, Bern, Switzerland</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">C.</namePart>
<namePart type="family">Pandu Rangan</namePart>
<affiliation>Indian Institute of Technology, Madras, India</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Bernhard</namePart>
<namePart type="family">Steffen</namePart>
<affiliation>University of Dortmund, Dortmund, Germany</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Madhu</namePart>
<namePart type="family">Sudan</namePart>
<affiliation>Massachusetts Institute of Technology, MA, USA</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Demetri</namePart>
<namePart type="family">Terzopoulos</namePart>
<affiliation>University of California, Los Angeles, CA, USA</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Doug</namePart>
<namePart type="family">Tygar</namePart>
<affiliation>University of California, Berkeley, CA, USA</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Moshe</namePart>
<namePart type="given">Y.</namePart>
<namePart type="family">Vardi</namePart>
<affiliation>Rice University, Houston, TX, USA</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Gerhard</namePart>
<namePart type="family">Weikum</namePart>
<affiliation>Max-Planck Institute of Computer Science, Saarbrücken, Germany</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<originInfo><publisher>Springer</publisher>
<copyrightDate encoding="w3cdtf">2013</copyrightDate>
<issuance>serial</issuance>
</originInfo>
<relatedItem type="constituent"><titleInfo><title>Lecture Notes in Artificial Intelligence</title>
</titleInfo>
<name type="personal"><namePart type="given">David</namePart>
<namePart type="family">Hutchison</namePart>
<affiliation>Lancaster University, Lancaster, UK</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Takeo</namePart>
<namePart type="family">Kanade</namePart>
<affiliation>Carnegie Mellon University, Pittsburgh, PA, USA</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Josef</namePart>
<namePart type="family">Kittler</namePart>
<affiliation>University of Surrey, Guildford, UK</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Jon</namePart>
<namePart type="given">M.</namePart>
<namePart type="family">Kleinberg</namePart>
<affiliation>Cornell University, Ithaca, NY, USA</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Friedemann</namePart>
<namePart type="family">Mattern</namePart>
<affiliation>ETH Zurich, Zurich, Switzerland</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">John</namePart>
<namePart type="given">C.</namePart>
<namePart type="family">Mitchell</namePart>
<affiliation>Stanford University, Stanford, CA, USA</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Moni</namePart>
<namePart type="family">Naor</namePart>
<affiliation>Weizmann Institute of Science, Rehovot, Israel</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Oscar</namePart>
<namePart type="family">Nierstrasz</namePart>
<affiliation>University of Bern, Bern, Switzerland</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">C.</namePart>
<namePart type="family">Pandu Rangan</namePart>
<affiliation>Indian Institute of Technology, Madras, India</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Bernhard</namePart>
<namePart type="family">Steffen</namePart>
<affiliation>University of Dortmund, Dortmund, Germany</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Madhu</namePart>
<namePart type="family">Sudan</namePart>
<affiliation>Massachusetts Institute of Technology, MA, USA</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Demetri</namePart>
<namePart type="family">Terzopoulos</namePart>
<affiliation>University of California, Los Angeles, CA, USA</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Doug</namePart>
<namePart type="family">Tygar</namePart>
<affiliation>University of California, Berkeley, CA, USA</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Moshe</namePart>
<namePart type="given">Y.</namePart>
<namePart type="family">Vardi</namePart>
<affiliation>Rice University, Houston, TX, USA</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Gerhard</namePart>
<namePart type="family">Weikum</namePart>
<affiliation>Max-Planck Institute of Computer Science, Saarbrücken, Germany</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Randy</namePart>
<namePart type="family">Goebel</namePart>
<affiliation>University of Alberta, Edmonton, Canada</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Jörg</namePart>
<namePart type="family">Siekmann</namePart>
<affiliation>University of Saarland, Saarbrücken, Germany</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Wolfgang</namePart>
<namePart type="family">Wahlster</namePart>
<affiliation>DFKI and University of Saarland, Saarbrücken, Germany</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Didier</namePart>
<namePart type="family">Galmiche</namePart>
<affiliation>LORIA UMR CNRS 7503, Université de Lorraine, Campus Scientifique, BP 239, 54506, Vandœuvre-lès-Nancy, France</affiliation>
<affiliation>E-mail: didier.galmiche@loria.fr</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Dominique</namePart>
<namePart type="family">Larchey-Wendling</namePart>
<affiliation>LORIA – CNRS, UHP Nancy, Campus Scientifique, BP 239, 54 506, Vandœuvre-lès-Nancy, France</affiliation>
<affiliation>E-mail: dominique.larchey-wendling@loria.fr</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<genre type="sub-series"></genre>
<identifier type="ISSN">0302-9743</identifier>
<identifier type="eISSN">1611-3349</identifier>
<identifier type="SubSeriesID">1244</identifier>
</relatedItem>
<identifier type="ISSN">0302-9743</identifier>
<identifier type="eISSN">1611-3349</identifier>
<identifier type="SeriesID">558</identifier>
<recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2013</recordOrigin>
</recordInfo>
</relatedItem>
<identifier type="istex">A3CA0681C9B628C718B6068A1CDF0792C81ABC1C</identifier>
<identifier type="ark">ark:/67375/HCB-VBMH15HS-4</identifier>
<identifier type="DOI">10.1007/978-3-642-40537-2_18</identifier>
<identifier type="ChapterID">18</identifier>
<identifier type="ChapterID">Chap18</identifier>
<accessCondition type="use and reproduction" contentType="copyright">Springer-Verlag Berlin Heidelberg, 2013</accessCondition>
<recordInfo><recordContentSource authority="ISTEX" authorityURI="https://loaded-corpus.data.istex.fr" valueURI="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-RLRX46XW-4">springer</recordContentSource>
<recordOrigin>Springer-Verlag Berlin Heidelberg, 2013</recordOrigin>
</recordInfo>
</mods>
<json:item><extension>json</extension>
<original>false</original>
<mimetype>application/json</mimetype>
<uri>https://api.istex.fr/ark:/67375/HCB-VBMH15HS-4/record.json</uri>
</json:item>
</metadata>
<annexes><json:item><extension>xml</extension>
<original>true</original>
<mimetype>application/xml</mimetype>
<uri>https://api.istex.fr/ark:/67375/HCB-VBMH15HS-4/annexes.xml</uri>
</json:item>
</annexes>
</istex>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Corpus

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002662 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 002662 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Istex
   |étape=   Corpus
   |type=    RBID
   |clé=     ISTEX:A3CA0681C9B628C718B6068A1CDF0792C81ABC1C
   |texte=   Prefixed Tableau Systems for Logic of Proofs and Provability
}}

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022

	Serveur d'exploration sur la recherche en informatique en Lorraine
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration sur la recherche en informatique en Lorraine

Prefixed Tableau Systems for Logic of Proofs and Provability

Prefixed Tableau Systems for Logic of Proofs and Provability

Source :

Abstract

Links to Exploration step

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri