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.

Combining and automating classical and non-classical logics in classical higher-order logics

Identifieur interne : 001794 ( Istex/Corpus ); précédent : 001793; suivant : 001795

Combining and automating classical and non-classical logics in classical higher-order logics

Auteurs : Christoph Benzmüller

Source :

RBID : ISTEX:66DC056FECD94BC479D88167A3E49EDD4002FF46

English descriptors

Abstract

Abstract: Numerous classical and non-classical logics can be elegantly embedded in Church’s simple type theory, also known as classical higher-order logic. Examples include propositional and quantified multimodal logics, intuitionistic logics, logics for security, and logics for spatial reasoning. Furthermore, simple type theory is sufficiently expressive to model combinations of embedded logics and it has a well understood semantics. Off-the-shelf reasoning systems for simple type theory exist that can be uniformly employed for reasoning within and about embedded logics and logics combinations. In this article we focus on combinations of (quantified) epistemic and doxastic logics and study their application for modeling and automating the reasoning of rational agents. We present illustrating example problems and report on experiments with off-the-shelf higher-order automated theorem provers.

Url:
DOI: 10.1007/s10472-011-9249-7

Links to Exploration step

ISTEX:66DC056FECD94BC479D88167A3E49EDD4002FF46

Le document en format XML

<record>
<TEI wicri:istexFullTextTei="biblStruct">
<teiHeader>
<fileDesc>
<titleStmt>
<title xml:lang="en">Combining and automating classical and non-classical logics in classical higher-order logics</title>
<author>
<name sortKey="Benzmuller, Christoph" sort="Benzmuller, Christoph" uniqKey="Benzmuller C" first="Christoph" last="Benzmüller">Christoph Benzmüller</name>
<affiliation>
<mods:affiliation>Articulate Software, Angwin, CA, USA</mods:affiliation>
</affiliation>
<affiliation>
<mods:affiliation>E-mail: c.benzmueller@googlemail.com</mods:affiliation>
</affiliation>
</author>
</titleStmt>
<publicationStmt>
<idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:66DC056FECD94BC479D88167A3E49EDD4002FF46</idno>
<date when="2011" year="2011">2011</date>
<idno type="doi">10.1007/s10472-011-9249-7</idno>
<idno type="url">https://api.istex.fr/ark:/67375/VQC-VPX5CN5S-G/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">001794</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001794</idno>
</publicationStmt>
<sourceDesc>
<biblStruct>
<analytic>
<title level="a" type="main" xml:lang="en">Combining and automating classical and non-classical logics in classical higher-order logics</title>
<author>
<name sortKey="Benzmuller, Christoph" sort="Benzmuller, Christoph" uniqKey="Benzmuller C" first="Christoph" last="Benzmüller">Christoph Benzmüller</name>
<affiliation>
<mods:affiliation>Articulate Software, Angwin, CA, USA</mods:affiliation>
</affiliation>
<affiliation>
<mods:affiliation>E-mail: c.benzmueller@googlemail.com</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>Springer Netherlands</publisher>
<pubPlace>Dordrecht</pubPlace>
<date type="published" when="2011-06-01">2011-06-01</date>
<biblScope unit="volume">62</biblScope>
<biblScope unit="issue">1-2</biblScope>
<biblScope unit="page" from="103">103</biblScope>
<biblScope unit="page" to="128">128</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>Classical and non-classical logics</term>
<term>Classical higher-order logic</term>
<term>Higher-order automated theorem proving</term>
<term>Knowledge representation</term>
<term>Logic combinations</term>
<term>Quantified multimodal logics</term>
<term>Semantic embeddings</term>
</keywords>
</textClass>
<langUsage>
<language ident="en">en</language>
</langUsage>
</profileDesc>
</teiHeader>
<front>
<div type="abstract" xml:lang="en">Abstract: Numerous classical and non-classical logics can be elegantly embedded in Church’s simple type theory, also known as classical higher-order logic. Examples include propositional and quantified multimodal logics, intuitionistic logics, logics for security, and logics for spatial reasoning. Furthermore, simple type theory is sufficiently expressive to model combinations of embedded logics and it has a well understood semantics. Off-the-shelf reasoning systems for simple type theory exist that can be uniformly employed for reasoning within and about embedded logics and logics combinations. In this article we focus on combinations of (quantified) epistemic and doxastic logics and study their application for modeling and automating the reasoning of rational agents. We present illustrating example problems and report on experiments with off-the-shelf higher-order automated theorem provers.</div>
</front>
</TEI>
<istex>
<corpusName>springer-journals</corpusName>
<author>
<json:item>
<name>Christoph Benzmüller</name>
<affiliations>
<json:string>Articulate Software, Angwin, CA, USA</json:string>
<json:string>E-mail: c.benzmueller@googlemail.com</json:string>
</affiliations>
</json:item>
</author>
<subject>
<json:item>
<lang>
<json:string>eng</json:string>
</lang>
<value>Classical and non-classical logics</value>
</json:item>
<json:item>
<lang>
<json:string>eng</json:string>
</lang>
<value>Quantified multimodal logics</value>
</json:item>
<json:item>
<lang>
<json:string>eng</json:string>
</lang>
<value>Logic combinations</value>
</json:item>
<json:item>
<lang>
<json:string>eng</json:string>
</lang>
<value>Classical higher-order logic</value>
</json:item>
<json:item>
<lang>
<json:string>eng</json:string>
</lang>
<value>Semantic embeddings</value>
</json:item>
<json:item>
<lang>
<json:string>eng</json:string>
</lang>
<value>Knowledge representation</value>
</json:item>
<json:item>
<lang>
<json:string>eng</json:string>
</lang>
<value>Higher-order automated theorem proving</value>
</json:item>
</subject>
<articleId>
<json:string>9249</json:string>
<json:string>s10472-011-9249-7</json:string>
</articleId>
<arkIstex>ark:/67375/VQC-VPX5CN5S-G</arkIstex>
<language>
<json:string>eng</json:string>
</language>
<originalGenre>
<json:string>OriginalPaper</json:string>
</originalGenre>
<abstract>Abstract: Numerous classical and non-classical logics can be elegantly embedded in Church’s simple type theory, also known as classical higher-order logic. Examples include propositional and quantified multimodal logics, intuitionistic logics, logics for security, and logics for spatial reasoning. Furthermore, simple type theory is sufficiently expressive to model combinations of embedded logics and it has a well understood semantics. Off-the-shelf reasoning systems for simple type theory exist that can be uniformly employed for reasoning within and about embedded logics and logics combinations. In this article we focus on combinations of (quantified) epistemic and doxastic logics and study their application for modeling and automating the reasoning of rational agents. We present illustrating example problems and report on experiments with off-the-shelf higher-order automated theorem provers.</abstract>
<qualityIndicators>
<score>8.464</score>
<pdfWordCount>10203</pdfWordCount>
<pdfCharCount>56831</pdfCharCount>
<pdfVersion>1.4</pdfVersion>
<pdfPageCount>26</pdfPageCount>
<pdfPageSize>439.37 x 666.142 pts</pdfPageSize>
<refBibsNative>false</refBibsNative>
<abstractWordCount>122</abstractWordCount>
<abstractCharCount>905</abstractCharCount>
<keywordCount>7</keywordCount>
</qualityIndicators>
<title>Combining and automating classical and non-classical logics in classical higher-order logics</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>2011</publicationDate>
<copyrightDate>2011</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>62</volume>
<issue>1-2</issue>
<pages>
<first>103</first>
<last>128</last>
</pages>
<genre>
<json:string>journal</json:string>
</genre>
<editor>
<json:item>
<name>Jürgen Dix</name>
</json:item>
<json:item>
<name>João Leite</name>
</json:item>
</editor>
<subject>
<json:item>
<value>Mathematics, general</value>
</json:item>
<json:item>
<value>Artificial Intelligence (incl. Robotics)</value>
</json:item>
<json:item>
<value>Statistical Physics, Dynamical Systems and Complexity</value>
</json:item>
<json:item>
<value>Computer Science, general</value>
</json:item>
</subject>
</host>
<ark>
<json:string>ark:/67375/VQC-VPX5CN5S-G</json:string>
</ark>
<publicationDate>2011</publicationDate>
<copyrightDate>2011</copyrightDate>
<doi>
<json:string>10.1007/s10472-011-9249-7</json:string>
</doi>
<id>66DC056FECD94BC479D88167A3E49EDD4002FF46</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-VPX5CN5S-G/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-VPX5CN5S-G/bundle.zip</uri>
</json:item>
<istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/VQC-VPX5CN5S-G/fulltext.tei">
<teiHeader>
<fileDesc>
<titleStmt>
<title level="a" type="main" xml:lang="en">Combining and automating classical and non-classical logics in classical higher-order logics</title>
</titleStmt>
<publicationStmt>
<authority>ISTEX</authority>
<publisher scheme="https://scientific-publisher.data.istex.fr">Springer Netherlands</publisher>
<pubPlace>Dordrecht</pubPlace>
<availability>
<licence>
<p>Springer Science+Business Media B.V., 2011</p>
</licence>
<p scheme="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-3XSW68JL-F">springer</p>
</availability>
<date>2011</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">Combining and automating classical and non-classical logics in classical higher-order logics</title>
<author xml:id="author-0000" corresp="yes">
<persName>
<forename type="first">Christoph</forename>
<surname>Benzmüller</surname>
</persName>
<email>c.benzmueller@googlemail.com</email>
<affiliation>Articulate Software, Angwin, CA, USA</affiliation>
</author>
<idno type="istex">66DC056FECD94BC479D88167A3E49EDD4002FF46</idno>
<idno type="ark">ark:/67375/VQC-VPX5CN5S-G</idno>
<idno type="DOI">10.1007/s10472-011-9249-7</idno>
<idno type="article-id">9249</idno>
<idno type="article-id">s10472-011-9249-7</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">7</idno>
<idno type="volume-issue-count">4</idno>
<editor xml:id="book-author-0000">
<persName>
<forename type="first">Jürgen</forename>
<surname>Dix</surname>
</persName>
</editor>
<editor xml:id="book-author-0001">
<persName>
<forename type="first">João</forename>
<surname>Leite</surname>
</persName>
</editor>
<imprint>
<publisher>Springer Netherlands</publisher>
<pubPlace>Dordrecht</pubPlace>
<date type="published" when="2011-06-01"></date>
<biblScope unit="volume">62</biblScope>
<biblScope unit="issue">1-2</biblScope>
<biblScope unit="page" from="103">103</biblScope>
<biblScope unit="page" to="128">128</biblScope>
</imprint>
</monogr>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc>
<creation>
<date>2011</date>
</creation>
<langUsage>
<language ident="en">en</language>
</langUsage>
<abstract xml:lang="en">
<p>Abstract: Numerous classical and non-classical logics can be elegantly embedded in Church’s simple type theory, also known as classical higher-order logic. Examples include propositional and quantified multimodal logics, intuitionistic logics, logics for security, and logics for spatial reasoning. Furthermore, simple type theory is sufficiently expressive to model combinations of embedded logics and it has a well understood semantics. Off-the-shelf reasoning systems for simple type theory exist that can be uniformly employed for reasoning within and about embedded logics and logics combinations. In this article we focus on combinations of (quantified) epistemic and doxastic logics and study their application for modeling and automating the reasoning of rational agents. We present illustrating example problems and report on experiments with off-the-shelf higher-order automated theorem provers.</p>
</abstract>
<textClass xml:lang="en">
<keywords scheme="keyword">
<list>
<head>Keywords</head>
<item>
<term>Classical and non-classical logics</term>
</item>
<item>
<term>Quantified multimodal logics</term>
</item>
<item>
<term>Logic combinations</term>
</item>
<item>
<term>Classical higher-order logic</term>
</item>
<item>
<term>Semantic embeddings</term>
</item>
<item>
<term>Knowledge representation</term>
</item>
<item>
<term>Higher-order automated theorem proving</term>
</item>
</list>
</keywords>
</textClass>
<textClass>
<classCode scheme="Mathematics Subject Classifications (2010)">03B62</classCode>
<classCode scheme="Mathematics Subject Classifications (2010)">03B42</classCode>
<classCode scheme="Mathematics Subject Classifications (2010)">03B44</classCode>
<classCode scheme="Mathematics Subject Classifications (2010)">03B45</classCode>
<classCode scheme="Mathematics Subject Classifications (2010)">03B35</classCode>
<classCode scheme="Mathematics Subject Classifications (2010)">03B20</classCode>
<classCode scheme="Mathematics Subject Classifications (2010)">03B15</classCode>
<classCode scheme="Mathematics Subject Classifications (2010)">68T27</classCode>
<classCode scheme="Mathematics Subject Classifications (2010)">68T30</classCode>
<classCode scheme="Mathematics Subject Classifications (2010)">68T15</classCode>
</textClass>
<textClass>
<keywords scheme="Journal Subject">
<list>
<head>Computer Science</head>
<item>
<term>Mathematics, general</term>
</item>
<item>
<term>Artificial Intelligence (incl. Robotics)</term>
</item>
<item>
<term>Statistical Physics, Dynamical Systems and Complexity</term>
</item>
<item>
<term>Computer Science, general</term>
</item>
</list>
</keywords>
</textClass>
</profileDesc>
<revisionDesc>
<change when="2011-06-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-VPX5CN5S-G/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>Springer Netherlands</PublisherName>
<PublisherLocation>Dordrecht</PublisherLocation>
</PublisherInfo>
<Journal OutputMedium="All">
<JournalInfo JournalProductType="NonStandardArchiveJournal" 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">Mathematics, general</JournalSubject>
<JournalSubject Type="Secondary">Artificial Intelligence (incl. Robotics)</JournalSubject>
<JournalSubject Type="Secondary">Statistical Physics, Dynamical Systems and Complexity</JournalSubject>
<JournalSubject Type="Secondary">Computer Science, general</JournalSubject>
</JournalSubjectGroup>
</JournalInfo>
<Volume OutputMedium="All">
<VolumeInfo TocLevels="0" VolumeType="Regular">
<VolumeIDStart>62</VolumeIDStart>
<VolumeIDEnd>62</VolumeIDEnd>
<VolumeIssueCount>4</VolumeIssueCount>
</VolumeInfo>
<Issue IssueType="Combined" OutputMedium="All">
<IssueInfo IssueType="Combined" TocLevels="0">
<IssueIDStart>1</IssueIDStart>
<IssueIDEnd>2</IssueIDEnd>
<IssueTitle Language="En">Special Issue:Computational logics in Multi-agent Systems (CLIMA XI)</IssueTitle>
<IssueArticleCount>7</IssueArticleCount>
<IssueHistory>
<OnlineDate>
<Year>2011</Year>
<Month>12</Month>
<Day>15</Day>
</OnlineDate>
<PrintDate>
<Year>2011</Year>
<Month>12</Month>
<Day>14</Day>
</PrintDate>
<CoverDate>
<Year>2011</Year>
<Month>6</Month>
</CoverDate>
<PricelistYear>2011</PricelistYear>
</IssueHistory>
<IssueCopyright>
<CopyrightHolderName>Springer Science+Business Media B.V.</CopyrightHolderName>
<CopyrightYear>2011</CopyrightYear>
</IssueCopyright>
</IssueInfo>
<IssueHeader>
<EditorGroup>
<Editor>
<EditorName DisplayOrder="Western">
<GivenName>Jürgen</GivenName>
<FamilyName>Dix</FamilyName>
</EditorName>
</Editor>
<Editor>
<EditorName DisplayOrder="Western">
<GivenName>João</GivenName>
<FamilyName>Leite</FamilyName>
</EditorName>
</Editor>
</EditorGroup>
</IssueHeader>
<Article ID="s10472-011-9249-7" OutputMedium="All">
<ArticleInfo ArticleType="OriginalPaper" ContainsESM="No" Language="En" NumberingStyle="ContentOnly" TocLevels="0">
<ArticleID>9249</ArticleID>
<ArticleDOI>10.1007/s10472-011-9249-7</ArticleDOI>
<ArticleSequenceNumber>6</ArticleSequenceNumber>
<ArticleTitle Language="En">Combining and automating classical and non-classical logics in classical higher-order logics</ArticleTitle>
<ArticleFirstPage>103</ArticleFirstPage>
<ArticleLastPage>128</ArticleLastPage>
<ArticleHistory>
<RegistrationDate>
<Year>2011</Year>
<Month>6</Month>
<Day>10</Day>
</RegistrationDate>
<OnlineDate>
<Year>2011</Year>
<Month>7</Month>
<Day>9</Day>
</OnlineDate>
</ArticleHistory>
<ArticleCopyright>
<CopyrightHolderName>Springer Science+Business Media B.V.</CopyrightHolderName>
<CopyrightYear>2011</CopyrightYear>
</ArticleCopyright>
<ArticleGrants 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>
</ArticleGrants>
</ArticleInfo>
<ArticleHeader>
<AuthorGroup>
<Author AffiliationIDS="Aff1" CorrespondingAffiliationID="Aff1">
<AuthorName DisplayOrder="Western">
<GivenName>Christoph</GivenName>
<FamilyName>Benzmüller</FamilyName>
</AuthorName>
<Contact>
<Email>c.benzmueller@googlemail.com</Email>
</Contact>
</Author>
<Affiliation ID="Aff1">
<OrgName>Articulate Software</OrgName>
<OrgAddress>
<City>Angwin</City>
<State>CA</State>
<Country Code="US">USA</Country>
</OrgAddress>
</Affiliation>
</AuthorGroup>
<Abstract ID="Abs1" Language="En">
<Heading>Abstract</Heading>
<Para>Numerous classical and non-classical logics can be elegantly embedded in Church’s simple type theory, also known as classical higher-order logic. Examples include propositional and quantified multimodal logics, intuitionistic logics, logics for security, and logics for spatial reasoning. Furthermore, simple type theory is sufficiently expressive to model combinations of embedded logics and it has a well understood semantics. Off-the-shelf reasoning systems for simple type theory exist that can be uniformly employed for reasoning
<Emphasis Type="Italic">within</Emphasis>
and
<Emphasis Type="Italic">about</Emphasis>
embedded logics and logics combinations. In this article we focus on combinations of (quantified) epistemic and doxastic logics and study their application for modeling and automating the reasoning of rational agents. We present illustrating example problems and report on experiments with off-the-shelf higher-order automated theorem provers.</Para>
</Abstract>
<KeywordGroup Language="En">
<Heading>Keywords</Heading>
<Keyword>Classical and non-classical logics</Keyword>
<Keyword>Quantified multimodal logics</Keyword>
<Keyword>Logic combinations</Keyword>
<Keyword>Classical higher-order logic</Keyword>
<Keyword>Semantic embeddings</Keyword>
<Keyword>Knowledge representation</Keyword>
<Keyword>Higher-order automated theorem proving</Keyword>
</KeywordGroup>
<KeywordGroup Language="--">
<Heading>Mathematics Subject Classifications (2010)</Heading>
<Keyword>03B62</Keyword>
<Keyword>03B42</Keyword>
<Keyword>03B44</Keyword>
<Keyword>03B45</Keyword>
<Keyword>03B35</Keyword>
<Keyword>03B20</Keyword>
<Keyword>03B15</Keyword>
<Keyword>68T27</Keyword>
<Keyword>68T30</Keyword>
<Keyword>68T15</Keyword>
</KeywordGroup>
<ArticleNote Type="Misc">
<SimplePara>This work has been funded by the German Research Foundation (DFG) under grant BE 2501/6-1.</SimplePara>
</ArticleNote>
</ArticleHeader>
<NoBody></NoBody>
</Article>
</Issue>
</Volume>
</Journal>
</Publisher>
</istex:document>
</istex:metadataXml>
<mods version="3.6">
<titleInfo lang="en">
<title>Combining and automating classical and non-classical logics in classical higher-order logics</title>
</titleInfo>
<titleInfo type="alternative" contentType="CDATA">
<title>Combining and automating classical and non-classical logics in classical higher-order logics</title>
</titleInfo>
<name type="personal" displayLabel="corresp">
<namePart type="given">Christoph</namePart>
<namePart type="family">Benzmüller</namePart>
<affiliation>Articulate Software, Angwin, CA, USA</affiliation>
<affiliation>E-mail: c.benzmueller@googlemail.com</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>Springer Netherlands</publisher>
<place>
<placeTerm type="text">Dordrecht</placeTerm>
</place>
<dateIssued encoding="w3cdtf">2011-06-01</dateIssued>
<copyrightDate encoding="w3cdtf">2011</copyrightDate>
</originInfo>
<language>
<languageTerm type="code" authority="rfc3066">en</languageTerm>
<languageTerm type="code" authority="iso639-2b">eng</languageTerm>
</language>
<abstract lang="en">Abstract: Numerous classical and non-classical logics can be elegantly embedded in Church’s simple type theory, also known as classical higher-order logic. Examples include propositional and quantified multimodal logics, intuitionistic logics, logics for security, and logics for spatial reasoning. Furthermore, simple type theory is sufficiently expressive to model combinations of embedded logics and it has a well understood semantics. Off-the-shelf reasoning systems for simple type theory exist that can be uniformly employed for reasoning within and about embedded logics and logics combinations. In this article we focus on combinations of (quantified) epistemic and doxastic logics and study their application for modeling and automating the reasoning of rational agents. We present illustrating example problems and report on experiments with off-the-shelf higher-order automated theorem provers.</abstract>
<subject lang="en">
<genre>Keywords</genre>
<topic>Classical and non-classical logics</topic>
<topic>Quantified multimodal logics</topic>
<topic>Logic combinations</topic>
<topic>Classical higher-order logic</topic>
<topic>Semantic embeddings</topic>
<topic>Knowledge representation</topic>
<topic>Higher-order automated theorem proving</topic>
</subject>
<classification displayLabel="Mathematics Subject Classifications (2010)">03B62</classification>
<classification displayLabel="Mathematics Subject Classifications (2010)">03B42</classification>
<classification displayLabel="Mathematics Subject Classifications (2010)">03B44</classification>
<classification displayLabel="Mathematics Subject Classifications (2010)">03B45</classification>
<classification displayLabel="Mathematics Subject Classifications (2010)">03B35</classification>
<classification displayLabel="Mathematics Subject Classifications (2010)">03B20</classification>
<classification displayLabel="Mathematics Subject Classifications (2010)">03B15</classification>
<classification displayLabel="Mathematics Subject Classifications (2010)">68T27</classification>
<classification displayLabel="Mathematics Subject Classifications (2010)">68T30</classification>
<classification displayLabel="Mathematics Subject Classifications (2010)">68T15</classification>
<relatedItem type="host">
<titleInfo>
<title>Annals of Mathematics and Artificial Intelligence</title>
</titleInfo>
<titleInfo type="abbreviated">
<title>Ann Math Artif Intell</title>
</titleInfo>
<name type="personal">
<namePart type="given">Jürgen</namePart>
<namePart type="family">Dix</namePart>
<role>
<roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">João</namePart>
<namePart type="family">Leite</namePart>
<role>
<roleTerm type="text">editor</roleTerm>
</role>
</name>
<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">2011-12-15</dateIssued>
<copyrightDate encoding="w3cdtf">2011</copyrightDate>
</originInfo>
<subject>
<genre>Computer Science</genre>
<topic>Mathematics, general</topic>
<topic>Artificial Intelligence (incl. Robotics)</topic>
<topic>Statistical Physics, Dynamical Systems and Complexity</topic>
<topic>Computer Science, general</topic>
</subject>
<identifier type="ISSN">1012-2443</identifier>
<identifier type="eISSN">1573-7470</identifier>
<identifier type="JournalID">10472</identifier>
<identifier type="IssueArticleCount">7</identifier>
<identifier type="VolumeIssueCount">4</identifier>
<part>
<date>2011</date>
<detail type="issue">
<title>Special Issue:Computational logics in Multi-agent Systems (CLIMA XI)</title>
</detail>
<detail type="volume">
<number>62</number>
<caption>vol.</caption>
</detail>
<detail type="issue">
<number>1-2</number>
<caption>no.</caption>
</detail>
<extent unit="pages">
<start>103</start>
<end>128</end>
</extent>
</part>
<recordInfo>
<recordOrigin>Springer Science+Business Media B.V., 2011</recordOrigin>
</recordInfo>
</relatedItem>
<identifier type="istex">66DC056FECD94BC479D88167A3E49EDD4002FF46</identifier>
<identifier type="ark">ark:/67375/VQC-VPX5CN5S-G</identifier>
<identifier type="DOI">10.1007/s10472-011-9249-7</identifier>
<identifier type="ArticleID">9249</identifier>
<identifier type="ArticleID">s10472-011-9249-7</identifier>
<accessCondition type="use and reproduction" contentType="copyright">Springer Science+Business Media B.V., 2011</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 B.V., 2011</recordOrigin>
</recordInfo>
</mods>
<json:item>
<extension>json</extension>
<original>false</original>
<mimetype>application/json</mimetype>
<uri>https://api.istex.fr/ark:/67375/VQC-VPX5CN5S-G/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 001794 | SxmlIndent | more

Ou

HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 001794 | 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:66DC056FECD94BC479D88167A3E49EDD4002FF46
   |texte=   Combining and automating classical and non-classical logics in classical higher-order logics
}}

Wicri

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