Mechanizing common knowledge logic using COQ
Identifieur interne : 003C47 ( Istex/Corpus ); précédent : 003C46; suivant : 003C48Mechanizing common knowledge logic using COQ
Auteurs : Pierre LescanneSource :
- Annals of Mathematics and Artificial Intelligence [ 1012-2443 ] ; 2006-09-01.
English descriptors
- KwdEn :
Abstract
Abstract: This paper presents a formalization in Coq of Common Knowledge Logic and checks its adequacy on case studies. Those studies allow exploring experimentally the proof-theoretic side of Common Knowledge Logic. This work is original in that nobody has considered Higher Order Common Knowledge Logic from the point of view of proofs performed on a proof assistant. As a matter of facts, it is experimental by nature as it tries to draw conclusions from experiments.
Url:
DOI: 10.1007/s10472-006-9042-1
Links to Exploration step
ISTEX:FC0807A5AA0A8C54D1281454EFD8C74E09FFE746Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Mechanizing common knowledge logic using COQ</title><author><name sortKey="Lescanne, Pierre" sort="Lescanne, Pierre" uniqKey="Lescanne P" first="Pierre" last="Lescanne">Pierre Lescanne</name><affiliation><mods:affiliation>Laboratoire de l’Informatique du Parallélisme, École Normale Supérieure de Lyon 46, Allée d’Italie, 69364, Lyon 07, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: Pierre.Lescanne@ens-lyon.fr</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:FC0807A5AA0A8C54D1281454EFD8C74E09FFE746</idno><date when="2007" year="2007">2007</date><idno type="doi">10.1007/s10472-006-9042-1</idno><idno type="url">https://api.istex.fr/ark:/67375/VQC-BKRDSJBX-P/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003C47</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003C47</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Mechanizing common knowledge logic using COQ</title><author><name sortKey="Lescanne, Pierre" sort="Lescanne, Pierre" uniqKey="Lescanne P" first="Pierre" last="Lescanne">Pierre Lescanne</name><affiliation><mods:affiliation>Laboratoire de l’Informatique du Parallélisme, École Normale Supérieure de Lyon 46, Allée d’Italie, 69364, Lyon 07, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: Pierre.Lescanne@ens-lyon.fr</mods:affiliation></affiliation></author></analytic><monogr></monogr><series><title level="j">Annals of Mathematics and Artificial Intelligence</title><title level="j" type="abbrev">Ann Math Artif Intell</title><idno type="ISSN">1012-2443</idno><idno type="eISSN">1573-7470</idno><imprint><publisher>Kluwer Academic Publishers</publisher><pubPlace>Dordrecht</pubPlace><date type="published" when="2006-09-01">2006-09-01</date><biblScope unit="volume">48</biblScope><biblScope unit="issue">1-2</biblScope><biblScope unit="page" from="15">15</biblScope><biblScope unit="page" to="43">43</biblScope></imprint><idno type="ISSN">1012-2443</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">1012-2443</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>COQ</term><term>Common knowledge logic</term><term>Epistemic logic</term><term>Higher order common knowledge logic</term><term>Modalities</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: This paper presents a formalization in Coq of Common Knowledge Logic and checks its adequacy on case studies. Those studies allow exploring experimentally the proof-theoretic side of Common Knowledge Logic. This work is original in that nobody has considered Higher Order Common Knowledge Logic from the point of view of proofs performed on a proof assistant. As a matter of facts, it is experimental by nature as it tries to draw conclusions from experiments.</div></front></TEI><istex><corpusName>springer-journals</corpusName><author><json:item><name>Pierre Lescanne</name><affiliations><json:string>Laboratoire de l’Informatique du Parallélisme, École Normale Supérieure de Lyon 46, Allée d’Italie, 69364, Lyon 07, France</json:string><json:string>E-mail: Pierre.Lescanne@ens-lyon.fr</json:string></affiliations></json:item></author><subject><json:item><lang><json:string>eng</json:string></lang><value>Common knowledge logic</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>COQ</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>Epistemic logic</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>Higher order common knowledge logic</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>Modalities</value></json:item></subject><articleId><json:string>9042</json:string><json:string>s10472-006-9042-1</json:string></articleId><arkIstex>ark:/67375/VQC-BKRDSJBX-P</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>OriginalPaper</json:string></originalGenre><abstract>Abstract: This paper presents a formalization in Coq of Common Knowledge Logic and checks its adequacy on case studies. Those studies allow exploring experimentally the proof-theoretic side of Common Knowledge Logic. This work is original in that nobody has considered Higher Order Common Knowledge Logic from the point of view of proofs performed on a proof assistant. As a matter of facts, it is experimental by nature as it tries to draw conclusions from experiments.</abstract><qualityIndicators><refBibsNative>false</refBibsNative><abstractWordCount>75</abstractWordCount><abstractCharCount>470</abstractCharCount><keywordCount>5</keywordCount><score>7.9</score><pdfWordCount>11369</pdfWordCount><pdfCharCount>56904</pdfCharCount><pdfVersion>1.3</pdfVersion><pdfPageCount>29</pdfPageCount><pdfPageSize>439.37 x 666.142 pts</pdfPageSize></qualityIndicators><title>Mechanizing common knowledge logic using COQ</title><genre><json:string>research-article</json:string></genre><host><title>Annals of Mathematics and Artificial Intelligence</title><language><json:string>unknown</json:string></language><publicationDate>2007</publicationDate><copyrightDate>2007</copyrightDate><issn><json:string>1012-2443</json:string></issn><eissn><json:string>1573-7470</json:string></eissn><journalId><json:string>10472</json:string></journalId><volume>48</volume><issue>1-2</issue><pages><first>15</first><last>43</last></pages><genre><json:string>journal</json:string></genre><subject><json:item><value>Complexity</value></json:item><json:item><value>Computer Science, general</value></json:item><json:item><value>Mathematics, general</value></json:item><json:item><value>Artificial Intelligence (incl. Robotics)</value></json:item></subject></host><ark><json:string>ark:/67375/VQC-BKRDSJBX-P</json:string></ark><publicationDate>2006</publicationDate><copyrightDate>2007</copyrightDate><doi><json:string>10.1007/s10472-006-9042-1</json:string></doi><id>FC0807A5AA0A8C54D1281454EFD8C74E09FFE746</id><score>1</score><fulltext><json:item><extension>pdf</extension><original>true</original><mimetype>application/pdf</mimetype><uri>https://api.istex.fr/ark:/67375/VQC-BKRDSJBX-P/fulltext.pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/ark:/67375/VQC-BKRDSJBX-P/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/VQC-BKRDSJBX-P/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Mechanizing common knowledge logic using COQ</title></titleStmt><publicationStmt><authority>ISTEX</authority><publisher scheme="https://scientific-publisher.data.istex.fr">Kluwer Academic Publishers</publisher><pubPlace>Dordrecht</pubPlace><availability><licence><p>Springer Science+Business Media, Inc., 2007</p></licence><p scheme="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-3XSW68JL-F">springer</p></availability><date>2007</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></notesStmt><sourceDesc><biblStruct type="inbook"><analytic><title level="a" type="main" xml:lang="en">Mechanizing common knowledge logic using COQ</title><author xml:id="author-0000" corresp="yes"><persName><forename type="first">Pierre</forename><surname>Lescanne</surname></persName><email>Pierre.Lescanne@ens-lyon.fr</email><affiliation>Laboratoire de l’Informatique du Parallélisme, École Normale Supérieure de Lyon 46, Allée d’Italie, 69364, Lyon 07, France</affiliation></author><idno type="istex">FC0807A5AA0A8C54D1281454EFD8C74E09FFE746</idno><idno type="ark">ark:/67375/VQC-BKRDSJBX-P</idno><idno type="DOI">10.1007/s10472-006-9042-1</idno><idno type="article-id">9042</idno><idno type="article-id">s10472-006-9042-1</idno></analytic><monogr><title level="j">Annals of Mathematics and Artificial Intelligence</title><title level="j" type="abbrev">Ann Math Artif Intell</title><idno type="pISSN">1012-2443</idno><idno type="eISSN">1573-7470</idno><idno type="journal-ID">true</idno><idno type="issue-article-count">4</idno><idno type="volume-issue-count">4</idno><imprint><publisher>Kluwer Academic Publishers</publisher><pubPlace>Dordrecht</pubPlace><date type="published" when="2006-09-01"></date><biblScope unit="volume">48</biblScope><biblScope unit="issue">1-2</biblScope><biblScope unit="page" from="15">15</biblScope><biblScope unit="page" to="43">43</biblScope></imprint></monogr></biblStruct></sourceDesc></fileDesc><profileDesc><creation><date>2007</date></creation><langUsage><language ident="en">en</language></langUsage><abstract xml:lang="en"><p>Abstract: This paper presents a formalization in Coq of Common Knowledge Logic and checks its adequacy on case studies. Those studies allow exploring experimentally the proof-theoretic side of Common Knowledge Logic. This work is original in that nobody has considered Higher Order Common Knowledge Logic from the point of view of proofs performed on a proof assistant. As a matter of facts, it is experimental by nature as it tries to draw conclusions from experiments.</p></abstract><textClass xml:lang="en"><keywords scheme="keyword"><list><head>Keywords</head><item><term>Common knowledge logic</term></item><item><term>COQ</term></item><item><term>Epistemic logic</term></item><item><term>Higher order common knowledge logic</term></item><item><term>Modalities</term></item></list></keywords></textClass><textClass><classCode scheme="Mathematics Subject Classifications (2000)">03B42</classCode><classCode scheme="Mathematics Subject Classifications (2000)">03B15</classCode><classCode scheme="Mathematics Subject Classifications (2000)">03B35</classCode></textClass><textClass><keywords scheme="Journal Subject"><list><head>Computer Science</head><item><term>Complexity</term></item><item><term>Computer Science, general</term></item><item><term>Mathematics, general</term></item><item><term>Artificial Intelligence (incl. Robotics)</term></item></list></keywords></textClass></profileDesc><revisionDesc><change when="2006-09-01">Published</change></revisionDesc></teiHeader></istex:fulltextTEI><json:item><extension>txt</extension><original>false</original><mimetype>text/plain</mimetype><uri>https://api.istex.fr/ark:/67375/VQC-BKRDSJBX-P/fulltext.txt</uri></json:item></fulltext><metadata><istex:metadataXml wicri:clean="corpus springer-journals 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>Kluwer Academic Publishers</PublisherName><PublisherLocation>Dordrecht</PublisherLocation></PublisherInfo><Journal OutputMedium="All"><JournalInfo JournalProductType="ArchiveJournal" NumberingStyle="ContentOnly"><JournalID>10472</JournalID><JournalPrintISSN>1012-2443</JournalPrintISSN><JournalElectronicISSN>1573-7470</JournalElectronicISSN><JournalTitle>Annals of Mathematics and Artificial Intelligence</JournalTitle><JournalAbbreviatedTitle>Ann Math Artif Intell</JournalAbbreviatedTitle><JournalSubjectGroup><JournalSubject Type="Primary">Computer Science</JournalSubject><JournalSubject Type="Secondary">Complexity</JournalSubject><JournalSubject Type="Secondary">Computer Science, general </JournalSubject><JournalSubject Type="Secondary">Mathematics, general</JournalSubject><JournalSubject Type="Secondary">Artificial Intelligence (incl. Robotics)</JournalSubject></JournalSubjectGroup></JournalInfo><Volume OutputMedium="All"><VolumeInfo TocLevels="0" VolumeType="Regular"><VolumeIDStart>48</VolumeIDStart><VolumeIDEnd>48</VolumeIDEnd><VolumeIssueCount>4</VolumeIssueCount></VolumeInfo><Issue IssueType="Combined" OutputMedium="All"><IssueInfo TocLevels="0"><IssueIDStart>1</IssueIDStart><IssueIDEnd>2</IssueIDEnd><IssueArticleCount>4</IssueArticleCount><IssueHistory><OnlineDate><Year>2007</Year><Month>6</Month><Day>5</Day></OnlineDate><PrintDate><Year>2007</Year><Month>6</Month><Day>5</Day></PrintDate><CoverDate><Year>2006</Year><Month>9</Month></CoverDate></IssueHistory><IssueCopyright><CopyrightHolderName>Springer Science+Business Media B.V.</CopyrightHolderName><CopyrightYear>2007</CopyrightYear></IssueCopyright></IssueInfo><Article ID="s10472-006-9042-1" OutputMedium="All"><ArticleInfo ArticleType="OriginalPaper" ContainsESM="No" Language="En" NumberingStyle="ContentOnly" TocLevels="0"><ArticleID>9042</ArticleID><ArticleDOI>10.1007/s10472-006-9042-1</ArticleDOI><ArticleSequenceNumber>2</ArticleSequenceNumber><ArticleTitle Language="En">Mechanizing common knowledge logic using COQ</ArticleTitle><ArticleFirstPage>15</ArticleFirstPage><ArticleLastPage>43</ArticleLastPage><ArticleHistory><RegistrationDate><Year>2006</Year><Month>12</Month><Day>20</Day></RegistrationDate><OnlineDate><Year>2007</Year><Month>3</Month><Day>7</Day></OnlineDate></ArticleHistory><ArticleCopyright><CopyrightHolderName>Springer Science+Business Media, Inc.</CopyrightHolderName><CopyrightYear>2007</CopyrightYear></ArticleCopyright></ArticleInfo><ArticleHeader><AuthorGroup><Author AffiliationIDS="Aff1" CorrespondingAffiliationID="Aff1"><AuthorName DisplayOrder="Western"><GivenName>Pierre</GivenName><FamilyName>Lescanne</FamilyName></AuthorName><Contact><Email>Pierre.Lescanne@ens-lyon.fr</Email></Contact></Author><Affiliation ID="Aff1"><OrgName>Laboratoire de l’Informatique du Parallélisme, École Normale Supérieure de Lyon 46</OrgName><OrgAddress><Street>Allée d’Italie</Street><Postcode>69364</Postcode><City>Lyon 07</City><Country Code="FR">France</Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>This paper presents a formalization in C<Emphasis Type="SmallCaps">oq</Emphasis> of Common Knowledge Logic and checks its adequacy on case studies. Those studies allow exploring experimentally the proof-theoretic side of Common Knowledge Logic. This work is original in that nobody has considered Higher Order Common Knowledge Logic from the point of view of proofs performed on a proof assistant. As a matter of facts, it is experimental by nature as it tries to draw conclusions from experiments.</Para></Abstract><KeywordGroup Language="En"><Heading>Keywords</Heading><Keyword>Common knowledge logic</Keyword><Keyword>COQ</Keyword><Keyword>Epistemic logic</Keyword><Keyword>Higher order common knowledge logic</Keyword><Keyword>Modalities</Keyword></KeywordGroup><KeywordGroup Language="--"><Heading>Mathematics Subject Classifications (2000)</Heading><Keyword>03B42</Keyword><Keyword>03B15</Keyword><Keyword>03B35</Keyword></KeywordGroup></ArticleHeader><NoBody></NoBody></Article></Issue></Volume></Journal></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Mechanizing common knowledge logic using COQ</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>Mechanizing common knowledge logic using COQ</title></titleInfo><name type="personal" displayLabel="corresp"><namePart type="given">Pierre</namePart><namePart type="family">Lescanne</namePart><affiliation>Laboratoire de l’Informatique du Parallélisme, École Normale Supérieure de Lyon 46, Allée d’Italie, 69364, Lyon 07, France</affiliation><affiliation>E-mail: Pierre.Lescanne@ens-lyon.fr</affiliation><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre type="research-article" displayLabel="OriginalPaper" 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>Kluwer Academic Publishers</publisher><place><placeTerm type="text">Dordrecht</placeTerm></place><dateIssued encoding="w3cdtf">2006-09-01</dateIssued><copyrightDate encoding="w3cdtf">2007</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><abstract lang="en">Abstract: This paper presents a formalization in Coq of Common Knowledge Logic and checks its adequacy on case studies. Those studies allow exploring experimentally the proof-theoretic side of Common Knowledge Logic. This work is original in that nobody has considered Higher Order Common Knowledge Logic from the point of view of proofs performed on a proof assistant. As a matter of facts, it is experimental by nature as it tries to draw conclusions from experiments.</abstract><subject lang="en"><genre>Keywords</genre><topic>Common knowledge logic</topic><topic>COQ</topic><topic>Epistemic logic</topic><topic>Higher order common knowledge logic</topic><topic>Modalities</topic></subject><classification displayLabel="Mathematics Subject Classifications (2000)">03B42</classification><classification displayLabel="Mathematics Subject Classifications (2000)">03B15</classification><classification displayLabel="Mathematics Subject Classifications (2000)">03B35</classification><relatedItem type="host"><titleInfo><title>Annals of Mathematics and Artificial Intelligence</title></titleInfo><titleInfo type="abbreviated"><title>Ann Math Artif Intell</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><originInfo><publisher>Springer</publisher><dateIssued encoding="w3cdtf">2007-06-05</dateIssued><copyrightDate encoding="w3cdtf">2007</copyrightDate></originInfo><subject><genre>Computer Science</genre><topic>Complexity</topic><topic>Computer Science, general</topic><topic>Mathematics, general</topic><topic>Artificial Intelligence (incl. Robotics)</topic></subject><identifier type="ISSN">1012-2443</identifier><identifier type="eISSN">1573-7470</identifier><identifier type="JournalID">10472</identifier><identifier type="IssueArticleCount">4</identifier><identifier type="VolumeIssueCount">4</identifier><part><date>2006</date><detail type="volume"><number>48</number><caption>vol.</caption></detail><detail type="issue"><number>1-2</number><caption>no.</caption></detail><extent unit="pages"><start>15</start><end>43</end></extent></part><recordInfo><recordOrigin>Springer Science+Business Media B.V., 2007</recordOrigin></recordInfo></relatedItem><identifier type="istex">FC0807A5AA0A8C54D1281454EFD8C74E09FFE746</identifier><identifier type="ark">ark:/67375/VQC-BKRDSJBX-P</identifier><identifier type="DOI">10.1007/s10472-006-9042-1</identifier><identifier type="ArticleID">9042</identifier><identifier type="ArticleID">s10472-006-9042-1</identifier><accessCondition type="use and reproduction" contentType="copyright">Springer Science+Business Media, Inc., 2007</accessCondition><recordInfo><recordContentSource authority="ISTEX" authorityURI="https://loaded-corpus.data.istex.fr" valueURI="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-3XSW68JL-F">springer</recordContentSource><recordOrigin>Springer Science+Business Media, Inc., 2007</recordOrigin></recordInfo></mods><json:item><extension>json</extension><original>false</original><mimetype>application/json</mimetype><uri>https://api.istex.fr/ark:/67375/VQC-BKRDSJBX-P/record.json</uri></json:item></metadata><serie></serie></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 003C47 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 003C47 | 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:FC0807A5AA0A8C54D1281454EFD8C74E09FFE746
|texte= Mechanizing common knowledge logic using COQ
}}
| This area was generated with Dilib version V0.6.33. |  |