AustralieFrV1, Istex, Corpus, bibRecord, 001613

Display Calculi for Nominal Tense Logics

Identifieur interne : 001613 ( Istex/Corpus ); précédent : 001612; suivant : 001614

Display Calculi for Nominal Tense Logics

Auteurs : Ste Phane Demri ; Rajeev Gore

Source :

Journal of Logic and Computation [ 0955-792X ] ; 2002-12.

RBID : ISTEX:75571AC51C40CB62AF55950D87DC4F9248EE95B1

English descriptors

KwdEn :
- Antecedent, Arbitrary sequents, Axiom, Axiom schema, Base cases, Calculus, Completeness, Completeness proof, Computer science, Demri, Derivable, Derivation, Difference operator, Disjoint, Disjoint unions, Display calculi, Display calculus, Display logic, Display postulates, Expressive power, Heorem, Inequality, Isomorphic copies, Last rule, Lecture notes, Logic, Modal, Modal frames, Modal logic, Modal logics, Modality, Natural translation, Nite, Nite sequence, Nominal, Nominal tense logics; display logic; cut elimination theorem; strong normalisation; Sahlqvist tense formulae, Philosophical logic, Primitive axioms, Primitive extensions, Proof systems, Propositional, Propositional variables, Resp, Sahlqvist, Sequent, Sequent calculi, Sequents, Slight variant, Soundness, Structural connectives, Structural rules, Substructural logics, Succedent, Symbolic logic, Technical report, Tense logic, Tense logics, Universal modality, Weak theorem.
Teeft :
- Antecedent, Arbitrary sequents, Axiom, Axiom schema, Base cases, Calculus, Completeness, Completeness proof, Computer science, Demri, Derivable, Derivation, Difference operator, Disjoint, Disjoint unions, Display calculi, Display calculus, Display logic, Display postulates, Expressive power, Heorem, Inequality, Isomorphic copies, Last rule, Lecture notes, Logic, Modal, Modal frames, Modal logic, Modal logics, Modality, Natural translation, Nite, Nite sequence, Nominal, Philosophical logic, Primitive axioms, Primitive extensions, Proof systems, Propositional, Propositional variables, Resp, Sahlqvist, Sequent, Sequent calculi, Sequents, Slight variant, Soundness, Structural connectives, Structural rules, Substructural logics, Succedent, Symbolic logic, Technical report, Tense logic, Tense logics, Universal modality, Weak theorem.

Abstract

We define display calculi for nominal tense logics extending the minimal nominal tense logic (MNTL) by addition of primitive axioms. To do so, we use the natural translation ofMNTL into the minimal tense logic of inequality (L≠) which is known to be properly displayable by application of Kracht's results. The rules of the display calculus δMNTL for MNTL mimic those of the display calculus δL≠ for L≠. We show that every MNTL‐valid formula admits a cut‐free derivation in δMNTL. We also show that a restricted display calculus δ−MNTL, is not only complete for MNTL, but that it enjoys cut‐elimination for arbitrary sequents. Finally, we give a weak Sahlqvist‐type theorem for two semantically defined extensions of MNTL. Using Kracht's techniques we obtain sound and complete display calculi for these two extensions based upon δMNTL and δ−MNTL respectively. The display calculi based upon δMNTL enjoy cut‐elimination for valid formulae only, but those based upon δ−MNTL enjoy cut‐elimination for arbitrary sequents.

Url:

https://api.istex.fr/document/75571AC51C40CB62AF55950D87DC4F9248EE95B1/fulltext/pdf

DOI: 10.1093/logcom/12.6.993

Links to Exploration step

ISTEX:75571AC51C40CB62AF55950D87DC4F9248EE95B1

Le document en format XML

<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Display Calculi for Nominal Tense Logics</title>
<author><name sortKey="Demri, Ste Phane" sort="Demri, Ste Phane" uniqKey="Demri S" first="Ste Phane" last="Demri">Ste Phane Demri</name>
<affiliation><mods:affiliation>Lab. Spécification et Vérification, CNRS, UMR 8643, ENS de Cachan, 61, av. du Pdt Wilson, 94235 Cachan Cedex, France. E-mail:</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Gore, Rajeev" sort="Gore, Rajeev" uniqKey="Gore R" first="Rajeev" last="Gore">Rajeev Gore</name>
<affiliation><mods:affiliation>Automated Reasoning Group and Department of Computer Science, Australian National University, Canberra ACT 0200, Australia. E-mail:</mods:affiliation>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:75571AC51C40CB62AF55950D87DC4F9248EE95B1</idno>
<date when="2002" year="2002">2002</date>
<idno type="doi">10.1093/logcom/12.6.993</idno>
<idno type="url">https://api.istex.fr/document/75571AC51C40CB62AF55950D87DC4F9248EE95B1/fulltext/pdf</idno>
<idno type="wicri:Area/Istex/Corpus">001613</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001613</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Display Calculi for Nominal Tense Logics</title>
<author><name sortKey="Demri, Ste Phane" sort="Demri, Ste Phane" uniqKey="Demri S" first="Ste Phane" last="Demri">Ste Phane Demri</name>
<affiliation><mods:affiliation>Lab. Spécification et Vérification, CNRS, UMR 8643, ENS de Cachan, 61, av. du Pdt Wilson, 94235 Cachan Cedex, France. E-mail:</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Gore, Rajeev" sort="Gore, Rajeev" uniqKey="Gore R" first="Rajeev" last="Gore">Rajeev Gore</name>
<affiliation><mods:affiliation>Automated Reasoning Group and Department of Computer Science, Australian National University, Canberra ACT 0200, Australia. E-mail:</mods:affiliation>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series><title level="j">Journal of Logic and Computation</title>
<title level="j" type="abbrev">J Logic Computation</title>
<idno type="ISSN">0955-792X</idno>
<idno type="eISSN">1465-363X</idno>
<imprint><publisher>Oxford University Press</publisher>
<date type="published" when="2002-12">2002-12</date>
<biblScope unit="volume">12</biblScope>
<biblScope unit="issue">6</biblScope>
<biblScope unit="page" from="993">993</biblScope>
<biblScope unit="page" to="1016">1016</biblScope>
</imprint>
<idno type="ISSN">0955-792X</idno>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><idno type="ISSN">0955-792X</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Antecedent</term>
<term>Arbitrary sequents</term>
<term>Axiom</term>
<term>Axiom schema</term>
<term>Base cases</term>
<term>Calculus</term>
<term>Completeness</term>
<term>Completeness proof</term>
<term>Computer science</term>
<term>Demri</term>
<term>Derivable</term>
<term>Derivation</term>
<term>Difference operator</term>
<term>Disjoint</term>
<term>Disjoint unions</term>
<term>Display calculi</term>
<term>Display calculus</term>
<term>Display logic</term>
<term>Display postulates</term>
<term>Expressive power</term>
<term>Heorem</term>
<term>Inequality</term>
<term>Isomorphic copies</term>
<term>Last rule</term>
<term>Lecture notes</term>
<term>Logic</term>
<term>Modal</term>
<term>Modal frames</term>
<term>Modal logic</term>
<term>Modal logics</term>
<term>Modality</term>
<term>Natural translation</term>
<term>Nite</term>
<term>Nite sequence</term>
<term>Nominal</term>
<term>Nominal tense logics; display logic; cut elimination theorem; strong normalisation; Sahlqvist tense formulae</term>
<term>Philosophical logic</term>
<term>Primitive axioms</term>
<term>Primitive extensions</term>
<term>Proof systems</term>
<term>Propositional</term>
<term>Propositional variables</term>
<term>Resp</term>
<term>Sahlqvist</term>
<term>Sequent</term>
<term>Sequent calculi</term>
<term>Sequents</term>
<term>Slight variant</term>
<term>Soundness</term>
<term>Structural connectives</term>
<term>Structural rules</term>
<term>Substructural logics</term>
<term>Succedent</term>
<term>Symbolic logic</term>
<term>Technical report</term>
<term>Tense logic</term>
<term>Tense logics</term>
<term>Universal modality</term>
<term>Weak theorem</term>
</keywords>
<keywords scheme="Teeft" xml:lang="en"><term>Antecedent</term>
<term>Arbitrary sequents</term>
<term>Axiom</term>
<term>Axiom schema</term>
<term>Base cases</term>
<term>Calculus</term>
<term>Completeness</term>
<term>Completeness proof</term>
<term>Computer science</term>
<term>Demri</term>
<term>Derivable</term>
<term>Derivation</term>
<term>Difference operator</term>
<term>Disjoint</term>
<term>Disjoint unions</term>
<term>Display calculi</term>
<term>Display calculus</term>
<term>Display logic</term>
<term>Display postulates</term>
<term>Expressive power</term>
<term>Heorem</term>
<term>Inequality</term>
<term>Isomorphic copies</term>
<term>Last rule</term>
<term>Lecture notes</term>
<term>Logic</term>
<term>Modal</term>
<term>Modal frames</term>
<term>Modal logic</term>
<term>Modal logics</term>
<term>Modality</term>
<term>Natural translation</term>
<term>Nite</term>
<term>Nite sequence</term>
<term>Nominal</term>
<term>Philosophical logic</term>
<term>Primitive axioms</term>
<term>Primitive extensions</term>
<term>Proof systems</term>
<term>Propositional</term>
<term>Propositional variables</term>
<term>Resp</term>
<term>Sahlqvist</term>
<term>Sequent</term>
<term>Sequent calculi</term>
<term>Sequents</term>
<term>Slight variant</term>
<term>Soundness</term>
<term>Structural connectives</term>
<term>Structural rules</term>
<term>Substructural logics</term>
<term>Succedent</term>
<term>Symbolic logic</term>
<term>Technical report</term>
<term>Tense logic</term>
<term>Tense logics</term>
<term>Universal modality</term>
<term>Weak theorem</term>
</keywords>
</textClass>
<langUsage><language ident="en">en</language>
</langUsage>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">We define display calculi for nominal tense logics extending the minimal nominal tense logic (MNTL) by addition of primitive axioms. To do so, we use the natural translation ofMNTL into the minimal tense logic of inequality (L≠) which is known to be properly displayable by application of Kracht's results. The rules of the display calculus δMNTL for MNTL mimic those of the display calculus δL≠ for L≠. We show that every MNTL‐valid formula admits a cut‐free derivation in δMNTL. We also show that a restricted display calculus δ−MNTL, is not only complete for MNTL, but that it enjoys cut‐elimination for arbitrary sequents. Finally, we give a weak Sahlqvist‐type theorem for two semantically defined extensions of MNTL. Using Kracht's techniques we obtain sound and complete display calculi for these two extensions based upon δMNTL and δ−MNTL respectively. The display calculi based upon δMNTL enjoy cut‐elimination for valid formulae only, but those based upon δ−MNTL enjoy cut‐elimination for arbitrary sequents.</div>
</front>
</TEI>
<istex><corpusName>oup</corpusName>
<keywords><teeft><json:string>calculus</json:string>
<json:string>display calculi</json:string>
<json:string>derivable</json:string>
<json:string>resp</json:string>
<json:string>sequents</json:string>
<json:string>sequent</json:string>
<json:string>display calculus</json:string>
<json:string>structural rules</json:string>
<json:string>sahlqvist</json:string>
<json:string>axiom</json:string>
<json:string>propositional</json:string>
<json:string>primitive axioms</json:string>
<json:string>heorem</json:string>
<json:string>lecture notes</json:string>
<json:string>succedent</json:string>
<json:string>modal logic</json:string>
<json:string>nite</json:string>
<json:string>display postulates</json:string>
<json:string>demri</json:string>
<json:string>arbitrary sequents</json:string>
<json:string>tense logic</json:string>
<json:string>modal logics</json:string>
<json:string>difference operator</json:string>
<json:string>disjoint</json:string>
<json:string>completeness proof</json:string>
<json:string>derivation</json:string>
<json:string>soundness</json:string>
<json:string>antecedent</json:string>
<json:string>disjoint unions</json:string>
<json:string>display logic</json:string>
<json:string>philosophical logic</json:string>
<json:string>isomorphic copies</json:string>
<json:string>structural connectives</json:string>
<json:string>logic</json:string>
<json:string>modal</json:string>
<json:string>symbolic logic</json:string>
<json:string>weak theorem</json:string>
<json:string>proof systems</json:string>
<json:string>tense logics</json:string>
<json:string>computer science</json:string>
<json:string>modality</json:string>
<json:string>inequality</json:string>
<json:string>completeness</json:string>
<json:string>expressive power</json:string>
<json:string>nite sequence</json:string>
<json:string>substructural logics</json:string>
<json:string>axiom schema</json:string>
<json:string>slight variant</json:string>
<json:string>modal frames</json:string>
<json:string>universal modality</json:string>
<json:string>propositional variables</json:string>
<json:string>base cases</json:string>
<json:string>last rule</json:string>
<json:string>primitive extensions</json:string>
<json:string>natural translation</json:string>
<json:string>technical report</json:string>
<json:string>sequent calculi</json:string>
<json:string>nominal</json:string>
</teeft>
</keywords>
<author><json:item><name>Stéphane Demri</name>
<affiliations><json:string>Lab. Spécification et Vérification, CNRS, UMR 8643, ENS de Cachan, 61, av. du Pdt Wilson, 94235 Cachan Cedex, France. E-mail:</json:string>
</affiliations>
</json:item>
<json:item><name>Rajeev Goré</name>
<affiliations><json:string>Automated Reasoning Group and Department of Computer Science, Australian National University, Canberra ACT 0200, Australia. E-mail:</json:string>
</affiliations>
</json:item>
</author>
<subject><json:item><lang><json:string>eng</json:string>
</lang>
<value>Nominal tense logics; display logic; cut elimination theorem; strong normalisation; Sahlqvist tense formulae</value>
</json:item>
</subject>
<arkIstex>ark:/67375/HXZ-XBQKLVKJ-K</arkIstex>
<language><json:string>eng</json:string>
</language>
<originalGenre><json:string>research-article</json:string>
</originalGenre>
<abstract>We define display calculi for nominal tense logics extending the minimal nominal tense logic (MNTL) by addition of primitive axioms. To do so, we use the natural translation ofMNTL into the minimal tense logic of inequality (L≠) which is known to be properly displayable by application of Kracht's results. The rules of the display calculus δMNTL for MNTL mimic those of the display calculus δL≠ for L≠. We show that every MNTL‐valid formula admits a cut‐free derivation in δMNTL. We also show that a restricted display calculus δ−MNTL, is not only complete for MNTL, but that it enjoys cut‐elimination for arbitrary sequents. Finally, we give a weak Sahlqvist‐type theorem for two semantically defined extensions of MNTL. Using Kracht's techniques we obtain sound and complete display calculi for these two extensions based upon δMNTL and δ−MNTL respectively. The display calculi based upon δMNTL enjoy cut‐elimination for valid formulae only, but those based upon δ−MNTL enjoy cut‐elimination for arbitrary sequents.</abstract>
<qualityIndicators><score>8.896</score>
<pdfWordCount>9877</pdfWordCount>
<pdfCharCount>48652</pdfCharCount>
<pdfVersion>1.4</pdfVersion>
<pdfPageCount>24</pdfPageCount>
<pdfPageSize>612 x 792 pts (letter)</pdfPageSize>
<refBibsNative>false</refBibsNative>
<abstractWordCount>158</abstractWordCount>
<abstractCharCount>1021</abstractCharCount>
<keywordCount>1</keywordCount>
</qualityIndicators>
<title>Display Calculi for Nominal Tense Logics</title>
<genre><json:string>research-article</json:string>
</genre>
<host><title>Journal of Logic and Computation</title>
<language><json:string>unknown</json:string>
</language>
<issn><json:string>0955-792X</json:string>
</issn>
<eissn><json:string>1465-363X</json:string>
</eissn>
<publisherId><json:string>logcom</json:string>
</publisherId>
<volume>12</volume>
<issue>6</issue>
<pages><first>993</first>
<last>1016</last>
</pages>
<genre><json:string>journal</json:string>
</genre>
</host>
<namedEntities><unitex><date><json:string>2002</json:string>
</date>
<geogName></geogName>
<orgName><json:string>Australian Research Council International Fellowship</json:string>
<json:string>Relational Proof Systems</json:string>
<json:string>Australian Research Council Queen Elizabeth</json:string>
<json:string>Oxford University</json:string>
<json:string>Labelled Deductive Systems</json:string>
</orgName>
<orgName_funder></orgName_funder>
<orgName_provider></orgName_provider>
<persName><json:string>Jeremy E. Dawson</json:string>
<json:string>By</json:string>
</persName>
<placeName><json:string>Australia</json:string>
<json:string>Grenoble</json:string>
<json:string>France</json:string>
</placeName>
<ref_url></ref_url>
<ref_bibl><json:string>[50]</json:string>
<json:string>[4]</json:string>
<json:string>[45, 29, 28]</json:string>
<json:string>[34]</json:string>
<json:string>[46, 34]</json:string>
<json:string>[15, 17]</json:string>
<json:string>[7, 46, 53]</json:string>
<json:string>[55]</json:string>
<json:string>[51, 11, 52, 2]</json:string>
<json:string>[8]</json:string>
<json:string>[27, 12]</json:string>
<json:string>[5, 55]</json:string>
<json:string>[19, 53, 3]</json:string>
<json:string>[7, 44, 53, 47, 51, 11, 52, 2]</json:string>
<json:string>[38, 43, 21, 7]</json:string>
<json:string>[54]</json:string>
<json:string>[7, 8, 25]</json:string>
<json:string>[7, 8, 44]</json:string>
<json:string>[3]</json:string>
<json:string>[19, 46, 53]</json:string>
<json:string>[20]</json:string>
<json:string>[35, 36]</json:string>
<json:string>[5]</json:string>
<json:string>[48]</json:string>
<json:string>[30]</json:string>
<json:string>[7]</json:string>
<json:string>[54, 34, 55]</json:string>
<json:string>[14]</json:string>
<json:string>[10, 4]</json:string>
<json:string>[31, 32]</json:string>
<json:string>[9]</json:string>
<json:string>[13]</json:string>
<json:string>[7, 34]</json:string>
<json:string>[53, 46, 3]</json:string>
</ref_bibl>
<bibl></bibl>
</unitex>
</namedEntities>
<ark><json:string>ark:/67375/HXZ-XBQKLVKJ-K</json:string>
</ark>
<categories><wos><json:string>science</json:string>
<json:string>logic</json:string>
<json:string>computer science, theory & methods</json:string>
</wos>
<scienceMetrix><json:string>applied sciences</json:string>
<json:string>information & communication technologies</json:string>
<json:string>computation theory & mathematics</json:string>
</scienceMetrix>
<scopus><json:string>1 - Physical Sciences</json:string>
<json:string>2 - Mathematics</json:string>
<json:string>3 - Logic</json:string>
<json:string>1 - Physical Sciences</json:string>
<json:string>2 - Computer Science</json:string>
<json:string>3 - Hardware and Architecture</json:string>
<json:string>1 - Social Sciences</json:string>
<json:string>2 - Arts and Humanities</json:string>
<json:string>3 - Arts and Humanities (miscellaneous)</json:string>
<json:string>1 - Physical Sciences</json:string>
<json:string>2 - Computer Science</json:string>
<json:string>3 - Software</json:string>
<json:string>1 - Physical Sciences</json:string>
<json:string>2 - Mathematics</json:string>
<json:string>3 - Theoretical Computer Science</json:string>
</scopus>
<inist><json:string>sciences appliquees, technologies et medecines</json:string>
<json:string>sciences biologiques et medicales</json:string>
<json:string>sciences medicales</json:string>
<json:string>informatique, statistique et modelisations biomedicales</json:string>
</inist>
</categories>
<publicationDate>2002</publicationDate>
<copyrightDate>2002</copyrightDate>
<doi><json:string>10.1093/logcom/12.6.993</json:string>
</doi>
<id>75571AC51C40CB62AF55950D87DC4F9248EE95B1</id>
<score>1</score>
<fulltext><json:item><extension>pdf</extension>
<original>true</original>
<mimetype>application/pdf</mimetype>
<uri>https://api.istex.fr/document/75571AC51C40CB62AF55950D87DC4F9248EE95B1/fulltext/pdf</uri>
</json:item>
<json:item><extension>zip</extension>
<original>false</original>
<mimetype>application/zip</mimetype>
<uri>https://api.istex.fr/document/75571AC51C40CB62AF55950D87DC4F9248EE95B1/fulltext/zip</uri>
</json:item>
<istex:fulltextTEI uri="https://api.istex.fr/document/75571AC51C40CB62AF55950D87DC4F9248EE95B1/fulltext/tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Display Calculi for Nominal Tense Logics</title>
<respStmt><resp>Références bibliographiques récupérées via GROBID</resp>
<name resp="ISTEX-API">ISTEX-API (INIST-CNRS)</name>
</respStmt>
</titleStmt>
<publicationStmt><authority>ISTEX</authority>
<publisher scheme="https://publisher-list.data.istex.fr">Oxford University Press</publisher>
<availability><licence><p>Copyright Oxford University Press 2002</p>
</licence>
<p scheme="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-GTWS0RDP-M">oup</p>
</availability>
<date>2002</date>
</publicationStmt>
<notesStmt><note type="research-article" scheme="https://content-type.data.istex.fr/ark:/67375/XTP-1JC4F85T-7">research-article</note>
<note type="journal" scheme="https://publication-type.data.istex.fr/ark:/67375/JMC-0GLKJH51-B">journal</note>
<note>Received 10 April 2000.</note>
</notesStmt>
<sourceDesc><biblStruct type="inbook"><analytic><title level="a" type="main" xml:lang="en">Display Calculi for Nominal Tense Logics</title>
<author xml:id="author-0000"><persName><forename type="first">Stéphane</forename>
<surname>Demri</surname>
</persName>
<affiliation>Lab. Spécification et Vérification, CNRS, UMR 8643, ENS de Cachan, 61, av. du Pdt Wilson, 94235 Cachan Cedex, France. E-mail:</affiliation>
</author>
<author xml:id="author-0001"><persName><forename type="first">Rajeev</forename>
<surname>Goré</surname>
</persName>
<affiliation>Automated Reasoning Group and Department of Computer Science, Australian National University, Canberra ACT 0200, Australia. E-mail:</affiliation>
</author>
<idno type="istex">75571AC51C40CB62AF55950D87DC4F9248EE95B1</idno>
<idno type="ark">ark:/67375/HXZ-XBQKLVKJ-K</idno>
<idno type="DOI">10.1093/logcom/12.6.993</idno>
<idno type="local">120993</idno>
</analytic>
<monogr><title level="j">Journal of Logic and Computation</title>
<title level="j" type="abbrev">J Logic Computation</title>
<idno type="pISSN">0955-792X</idno>
<idno type="eISSN">1465-363X</idno>
<idno type="publisher-id">logcom</idno>
<idno type="PublisherID-hwp">logcom</idno>
<imprint><publisher>Oxford University Press</publisher>
<date type="published" when="2002-12"></date>
<biblScope unit="volume">12</biblScope>
<biblScope unit="issue">6</biblScope>
<biblScope unit="page" from="993">993</biblScope>
<biblScope unit="page" to="1016">1016</biblScope>
</imprint>
</monogr>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><creation><date>2002</date>
</creation>
<langUsage><language ident="en">en</language>
</langUsage>
<abstract xml:lang="en"><p>We define display calculi for nominal tense logics extending the minimal nominal tense logic (MNTL) by addition of primitive axioms. To do so, we use the natural translation ofMNTL into the minimal tense logic of inequality (L≠) which is known to be properly displayable by application of Kracht's results. The rules of the display calculus δMNTL for MNTL mimic those of the display calculus δL≠ for L≠. We show that every MNTL‐valid formula admits a cut‐free derivation in δMNTL. We also show that a restricted display calculus δ−MNTL, is not only complete for MNTL, but that it enjoys cut‐elimination for arbitrary sequents. Finally, we give a weak Sahlqvist‐type theorem for two semantically defined extensions of MNTL. Using Kracht's techniques we obtain sound and complete display calculi for these two extensions based upon δMNTL and δ−MNTL respectively. The display calculi based upon δMNTL enjoy cut‐elimination for valid formulae only, but those based upon δ−MNTL enjoy cut‐elimination for arbitrary sequents.</p>
</abstract>
<textClass xml:lang="en"><keywords scheme="keyword"><list><head>KWD</head>
<item><term>Nominal tense logics; display logic; cut elimination theorem; strong normalisation; Sahlqvist tense formulae</term>
</item>
</list>
</keywords>
</textClass>
</profileDesc>
<revisionDesc><change when="2002-12">Published</change>
<change xml:id="refBibs-istex" who="#ISTEX-API" when="2017-10-6">References added</change>
</revisionDesc>
</teiHeader>
</istex:fulltextTEI>
<json:item><extension>txt</extension>
<original>false</original>
<mimetype>text/plain</mimetype>
<uri>https://api.istex.fr/document/75571AC51C40CB62AF55950D87DC4F9248EE95B1/fulltext/txt</uri>
</json:item>
</fulltext>
<metadata><istex:metadataXml wicri:clean="corpus oup, element #text not found" wicri:toSee="no header"><istex:xmlDeclaration>version="1.0" encoding="US-ASCII"</istex:xmlDeclaration>
<istex:docType PUBLIC="-//NLM//DTD Journal Publishing DTD v2.3 20070202//EN" URI="journalpublishing.dtd" name="istex:docType"></istex:docType>
<istex:document><article xml:lang="en" article-type="research-article">

  <front>

    <journal-meta>

<journal-id journal-id-type="publisher-id">logcom</journal-id>

      <journal-id journal-id-type="hwp">logcom</journal-id>

      <journal-title>Journal of Logic and Computation</journal-title>

      <abbrev-journal-title abbrev-type="publisher">J Logic Computation</abbrev-journal-title>

      <issn pub-type="ppub">0955-792X</issn>

      <issn pub-type="epub">1465-363X</issn>

      <publisher>

        <publisher-name>Oxford University Press</publisher-name>

      </publisher>

    </journal-meta>

    <article-meta>

      <article-id pub-id-type="other">120993</article-id>

<article-id pub-id-type="doi">10.1093/logcom/12.6.993</article-id>

      <article-categories>

        <subj-group subj-group-type="heading">

          <subject>Original Article</subject>

        </subj-group>

      </article-categories>

      <title-group>

        <article-title>Display Calculi for Nominal Tense Logics</article-title>

      </title-group>

      <contrib-group>

        <contrib contrib-type="author">

          <name>

            <surname>Demri</surname>

            <given-names>Stéphane</given-names>

          </name>

          <xref rid="AFF1">1</xref>

        </contrib>

        <contrib contrib-type="author">

          <name>

            <surname>Goré</surname>

            <given-names>Rajeev</given-names>

          </name>

          <xref rid="AFF2">2</xref>

        </contrib>

        <aff><target target-type="aff" id="AFF1"></target>
<label>1</label>
Lab. Spécification et Vérification, CNRS, UMR 8643, ENS de Cachan, 61, av. du Pdt Wilson, 94235 Cachan Cedex, France. E-mail: <ext-link xlink:href="demri@lsv.ens-cachan.fr" ext-link-type="email"> demri@lsv.ens-cachan.fr</ext-link>
<target target-type="aff" id="AFF2"></target>
<label>2</label>
Automated Reasoning Group and Department of Computer Science, Australian National University, Canberra ACT 0200, Australia. E-mail: <ext-link xlink:href="rpg@arp.anu.edu.au" ext-link-type="email"> rpg@arp.anu.edu.au</ext-link>
</aff>

      </contrib-group>

      <pub-date pub-type="ppub">

        <month>12</month>

        <year>2002</year>

      </pub-date>

      <volume>12</volume>

      <issue>6</issue>

      <fpage>993</fpage>

      <lpage>1016</lpage>

      <permissions>

        <copyright-statement>Copyright Oxford University Press 2002</copyright-statement>

        <copyright-year>2002</copyright-year>

      </permissions>

      <abstract xml:lang="en">

        <p>We define display calculi for nominal tense logics extending the minimal nominal tense logic (<bold>MNTL</bold>
) by addition of primitive axioms. To do so, we use the natural translation of<bold>MNTL</bold>
 into the minimal tense logic of inequality (<bold><italic>L</italic>
</bold>
<bold><sub>≠</sub>
</bold>
) which is known to be properly displayable by application of Kracht's results. The rules of the display calculus <bold>δMNTL</bold>
 for <bold>MNTL</bold>
 mimic those of the display calculus <bold>δ<bold><italic>L</italic>
</bold>
<sub>≠</sub>
</bold>
 for <bold><italic>L</italic>
</bold>
<bold><sub>≠</sub>
</bold>
. We show that every <bold>MNTL</bold>
‐valid formula admits a cut‐free derivation in <bold>δMNTL</bold>
. We also show that a restricted display calculus <bold>δ<sup>−</sup>
MNTL</bold>
, is not only complete for <bold>MNTL</bold>
, but that it enjoys cut‐elimination for arbitrary sequents. Finally, we give a weak Sahlqvist‐type theorem for two semantically defined extensions of <bold>MNTL</bold>
. Using Kracht's techniques we obtain sound and complete display calculi for these two extensions based upon <bold>δMNTL</bold>
 and <bold>δ<sup>−</sup>
MNTL</bold>
 respectively. The display calculi based upon <bold>δMNTL</bold>
 enjoy cut‐elimination for valid formulae only, but those based upon <bold>δ<sup>−</sup>
MNTL</bold>
 enjoy cut‐elimination for arbitrary sequents.</p>

      </abstract>

      <kwd-group kwd-group-type="KWD" xml:lang="en">

        <kwd>Nominal tense logics; display logic; cut elimination theorem; strong normalisation; Sahlqvist tense formulae</kwd>

      </kwd-group>

      <custom-meta-wrap>

        <custom-meta>

          <meta-name>hwp-legacy-fpage</meta-name>

          <meta-value>993</meta-value>

        </custom-meta>

        <custom-meta>

          <meta-name>hwp-legacy-dochead</meta-name>

          <meta-value>Original Article</meta-value>

        </custom-meta>

      </custom-meta-wrap>

    </article-meta>

    <notes>

      <p content-type="arthw-misc">Received 10 April 2000. </p>

    </notes>

  </front>

</article>

</istex:document>
</istex:metadataXml>
<mods version="3.6"><titleInfo lang="en"><title>Display Calculi for Nominal Tense Logics</title>
</titleInfo>
<titleInfo type="alternative" lang="en" contentType="CDATA"><title>Display Calculi for Nominal Tense Logics</title>
</titleInfo>
<name type="personal"><namePart type="given">Stéphane</namePart>
<namePart type="family">Demri</namePart>
<affiliation>Lab. Spécification et Vérification, CNRS, UMR 8643, ENS de Cachan, 61, av. du Pdt Wilson, 94235 Cachan Cedex, France. E-mail:</affiliation>
<role><roleTerm type="text">author</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Rajeev</namePart>
<namePart type="family">Goré</namePart>
<affiliation>Automated Reasoning Group and Department of Computer Science, Australian National University, Canberra ACT 0200, Australia. E-mail:</affiliation>
<role><roleTerm type="text">author</roleTerm>
</role>
</name>
<typeOfResource>text</typeOfResource>
<genre type="research-article" displayLabel="research-article" authority="ISTEX" authorityURI="https://content-type.data.istex.fr" valueURI="https://content-type.data.istex.fr/ark:/67375/XTP-1JC4F85T-7">research-article</genre>
<originInfo><publisher>Oxford University Press</publisher>
<dateIssued encoding="w3cdtf">2002-12</dateIssued>
<copyrightDate encoding="w3cdtf">2002</copyrightDate>
</originInfo>
<language><languageTerm type="code" authority="iso639-2b">eng</languageTerm>
<languageTerm type="code" authority="rfc3066">en</languageTerm>
</language>
<abstract lang="en">We define display calculi for nominal tense logics extending the minimal nominal tense logic (MNTL) by addition of primitive axioms. To do so, we use the natural translation ofMNTL into the minimal tense logic of inequality (L≠) which is known to be properly displayable by application of Kracht's results. The rules of the display calculus δMNTL for MNTL mimic those of the display calculus δL≠ for L≠. We show that every MNTL‐valid formula admits a cut‐free derivation in δMNTL. We also show that a restricted display calculus δ−MNTL, is not only complete for MNTL, but that it enjoys cut‐elimination for arbitrary sequents. Finally, we give a weak Sahlqvist‐type theorem for two semantically defined extensions of MNTL. Using Kracht's techniques we obtain sound and complete display calculi for these two extensions based upon δMNTL and δ−MNTL respectively. The display calculi based upon δMNTL enjoy cut‐elimination for valid formulae only, but those based upon δ−MNTL enjoy cut‐elimination for arbitrary sequents.</abstract>
<note>Received 10 April 2000.</note>
<subject lang="en"><genre>KWD</genre>
<topic>Nominal tense logics; display logic; cut elimination theorem; strong normalisation; Sahlqvist tense formulae</topic>
</subject>
<relatedItem type="host"><titleInfo><title>Journal of Logic and Computation</title>
</titleInfo>
<titleInfo type="abbreviated"><title>J Logic Computation</title>
</titleInfo>
<genre type="journal" authority="ISTEX" authorityURI="https://publication-type.data.istex.fr" valueURI="https://publication-type.data.istex.fr/ark:/67375/JMC-0GLKJH51-B">journal</genre>
<identifier type="ISSN">0955-792X</identifier>
<identifier type="eISSN">1465-363X</identifier>
<identifier type="PublisherID">logcom</identifier>
<identifier type="PublisherID-hwp">logcom</identifier>
<part><date>2002</date>
<detail type="volume"><caption>vol.</caption>
<number>12</number>
</detail>
<detail type="issue"><caption>no.</caption>
<number>6</number>
</detail>
<extent unit="pages"><start>993</start>
<end>1016</end>
</extent>
</part>
</relatedItem>
<identifier type="istex">75571AC51C40CB62AF55950D87DC4F9248EE95B1</identifier>
<identifier type="DOI">10.1093/logcom/12.6.993</identifier>
<identifier type="local">120993</identifier>
<accessCondition type="use and reproduction" contentType="copyright">Copyright Oxford University Press 2002</accessCondition>
<recordInfo><recordContentSource authority="ISTEX" authorityURI="https://loaded-corpus.data.istex.fr" valueURI="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-GTWS0RDP-M">oup</recordContentSource>
<recordOrigin>Copyright Oxford University Press 2002</recordOrigin>
</recordInfo>
</mods>
<json:item><extension>json</extension>
<original>false</original>
<mimetype>application/json</mimetype>
<uri>https://api.istex.fr/document/75571AC51C40CB62AF55950D87DC4F9248EE95B1/metadata/json</uri>
</json:item>
</metadata>
<serie></serie>
</istex>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Asie/explor/AustralieFrV1/Data/Istex/Corpus

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

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

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

{{Explor lien
   |wiki=    Wicri/Asie
   |area=    AustralieFrV1
   |flux=    Istex
   |étape=   Corpus
   |type=    RBID
   |clé=     ISTEX:75571AC51C40CB62AF55950D87DC4F9248EE95B1
   |texte=   Display Calculi for Nominal Tense Logics
}}

This area was generated with Dilib version V0.6.33.
Data generation: Tue Dec 5 10:43:12 2017. Site generation: Tue Mar 5 14:07:20 2024

	Serveur d'exploration sur les relations entre la France et l'Australie
	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 les relations entre la France et l'Australie

Display Calculi for Nominal Tense Logics

Display Calculi for Nominal Tense Logics

Source :

English descriptors

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