A new combination procedure for the word problem that generalizes fusion decidability results in modal logics
Identifieur interne : 005822 ( Main/Merge ); précédent : 005821; suivant : 005823A new combination procedure for the word problem that generalizes fusion decidability results in modal logics
Auteurs : Franz Baader [Allemagne] ; Silvio Ghilardi [Italie] ; Cesare Tinelli [États-Unis]Source :
- Information and computation : (Print) [ 0890-5401 ] ; 2006.
Descripteurs français
- Pascal (Inist)
- Wicri :
- topic : Décision.
English descriptors
- KwdEn :
Abstract
Previous results for combining decision procedures for the word problem in the non-disjoint case do not apply to equational theories induced by modal logics-which are not disjoint for sharing the theory of Boolean algebras. Conversely, decidability results for the fusion of modal logics are strongly tailored towards the special theories at hand, and thus do not generalize to other types of equational theories. In this paper, we present a new approach for combining decision procedures for the word problem in the non-disjoint case that applies to equational theories induced by modal logics, but is not restricted to them. The known fusion decidability results for modal logics are instances of our approach. However, even for equational theories induced by modal logics our results are more general since they are not restricted to so-called normal modal logics.
Links toward previous steps (curation, corpus...)
- to stream PascalFrancis, to step Corpus: 000416
- to stream PascalFrancis, to step Curation: 000617
- to stream PascalFrancis, to step Checkpoint: 000417
Links to Exploration step
Pascal:06-0527634Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">A new combination procedure for the word problem that generalizes fusion decidability results in modal logics</title>
<author><name sortKey="Baader, Franz" sort="Baader, Franz" uniqKey="Baader F" first="Franz" last="Baader">Franz Baader</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>Institut fur Theoretische Informatik, TU Dresden</s1>
<s3>DEU</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
<country>Allemagne</country>
<wicri:noRegion>TU Dresden</wicri:noRegion>
<wicri:noRegion>Institut fur Theoretische Informatik, TU Dresden</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Ghilardi, Silvio" sort="Ghilardi, Silvio" uniqKey="Ghilardi S" first="Silvio" last="Ghilardi">Silvio Ghilardi</name>
<affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Dipartimen to di Scienze dell'Informazione, Università degli Studi di Milano</s1>
<s3>ITA</s3>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>Italie</country>
<wicri:noRegion>Dipartimen to di Scienze dell'Informazione, Università degli Studi di Milano</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Tinelli, Cesare" sort="Tinelli, Cesare" uniqKey="Tinelli C" first="Cesare" last="Tinelli">Cesare Tinelli</name>
<affiliation wicri:level="4"><inist:fA14 i1="03"><s1>Department of Computer Science, The University of Iowa</s1>
<s3>USA</s3>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>États-Unis</country>
<placeName><settlement type="city">Iowa City</settlement>
<region type="state">Iowa</region>
</placeName>
<orgName type="university">Université de l'Iowa</orgName>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">06-0527634</idno>
<date when="2006">2006</date>
<idno type="stanalyst">PASCAL 06-0527634 INIST</idno>
<idno type="RBID">Pascal:06-0527634</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000416</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000617</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000417</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000417</idno>
<idno type="wicri:doubleKey">0890-5401:2006:Baader F:a:new:combination</idno>
<idno type="wicri:Area/Main/Merge">005822</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">A new combination procedure for the word problem that generalizes fusion decidability results in modal logics</title>
<author><name sortKey="Baader, Franz" sort="Baader, Franz" uniqKey="Baader F" first="Franz" last="Baader">Franz Baader</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>Institut fur Theoretische Informatik, TU Dresden</s1>
<s3>DEU</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
<country>Allemagne</country>
<wicri:noRegion>TU Dresden</wicri:noRegion>
<wicri:noRegion>Institut fur Theoretische Informatik, TU Dresden</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Ghilardi, Silvio" sort="Ghilardi, Silvio" uniqKey="Ghilardi S" first="Silvio" last="Ghilardi">Silvio Ghilardi</name>
<affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Dipartimen to di Scienze dell'Informazione, Università degli Studi di Milano</s1>
<s3>ITA</s3>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>Italie</country>
<wicri:noRegion>Dipartimen to di Scienze dell'Informazione, Università degli Studi di Milano</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Tinelli, Cesare" sort="Tinelli, Cesare" uniqKey="Tinelli C" first="Cesare" last="Tinelli">Cesare Tinelli</name>
<affiliation wicri:level="4"><inist:fA14 i1="03"><s1>Department of Computer Science, The University of Iowa</s1>
<s3>USA</s3>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>États-Unis</country>
<placeName><settlement type="city">Iowa City</settlement>
<region type="state">Iowa</region>
</placeName>
<orgName type="university">Université de l'Iowa</orgName>
</affiliation>
</author>
</analytic>
<series><title level="j" type="main">Information and computation : (Print)</title>
<title level="j" type="abbreviated">Inf. comput. : (Print)</title>
<idno type="ISSN">0890-5401</idno>
<imprint><date when="2006">2006</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><title level="j" type="main">Information and computation : (Print)</title>
<title level="j" type="abbreviated">Inf. comput. : (Print)</title>
<idno type="ISSN">0890-5401</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Boolean algebra</term>
<term>Computer theory</term>
<term>Decidability</term>
<term>Decision</term>
<term>Equational theory</term>
<term>Modal logic</term>
<term>Sharing</term>
<term>Type theory</term>
<term>Word</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Mot</term>
<term>Décidabilité</term>
<term>Logique modale</term>
<term>Décision</term>
<term>Théorie équationnelle</term>
<term>Partage</term>
<term>Algèbre Boole</term>
<term>Théorie type</term>
<term>Informatique théorique</term>
<term>Procédure décision</term>
<term>Problème mot</term>
<term>03B45</term>
<term>06Exx</term>
<term>03B15</term>
</keywords>
<keywords scheme="Wicri" type="topic" xml:lang="fr"><term>Décision</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Previous results for combining decision procedures for the word problem in the non-disjoint case do not apply to equational theories induced by modal logics-which are not disjoint for sharing the theory of Boolean algebras. Conversely, decidability results for the fusion of modal logics are strongly tailored towards the special theories at hand, and thus do not generalize to other types of equational theories. In this paper, we present a new approach for combining decision procedures for the word problem in the non-disjoint case that applies to equational theories induced by modal logics, but is not restricted to them. The known fusion decidability results for modal logics are instances of our approach. However, even for equational theories induced by modal logics our results are more general since they are not restricted to so-called normal modal logics.</div>
</front>
</TEI>
<affiliations><list><country><li>Allemagne</li>
<li>Italie</li>
<li>États-Unis</li>
</country>
<region><li>Iowa</li>
</region>
<settlement><li>Iowa City</li>
</settlement>
<orgName><li>Université de l'Iowa</li>
</orgName>
</list>
<tree><country name="Allemagne"><noRegion><name sortKey="Baader, Franz" sort="Baader, Franz" uniqKey="Baader F" first="Franz" last="Baader">Franz Baader</name>
</noRegion>
</country>
<country name="Italie"><noRegion><name sortKey="Ghilardi, Silvio" sort="Ghilardi, Silvio" uniqKey="Ghilardi S" first="Silvio" last="Ghilardi">Silvio Ghilardi</name>
</noRegion>
</country>
<country name="États-Unis"><region name="Iowa"><name sortKey="Tinelli, Cesare" sort="Tinelli, Cesare" uniqKey="Tinelli C" first="Cesare" last="Tinelli">Cesare Tinelli</name>
</region>
</country>
</tree>
</affiliations>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Merge
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 005822 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 005822 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Lorraine |area= InforLorV4 |flux= Main |étape= Merge |type= RBID |clé= Pascal:06-0527634 |texte= A new combination procedure for the word problem that generalizes fusion decidability results in modal logics }}
![]() | This area was generated with Dilib version V0.6.33. | ![]() |