InforLorV4, PascalFrancis, Corpus, bibRecord, 000308

Decidability and undecidability results for nelson-oppen and rewrite-based decision procedures

Identifieur interne : 000308 ( PascalFrancis/Corpus ); précédent : 000307; suivant : 000309

Decidability and undecidability results for nelson-oppen and rewrite-based decision procedures

Auteurs : Maria Paola Bonacina ; Silvio Ghilardi ; Enrica Nicolini ; Silvio Ranise ; Daniele Zucchelli

Source :

Lecture notes in computer science

RBID : Pascal:08-0306266

Descripteurs français

Pascal (Inist)
- Décidabilité, Théorie preuve, Démonstration automatique, Système réécriture, Prise de décision, Indécidabilité, Satisfiabilité, Réécriture, Satisfaction contrainte, Problème satisfiabilité, Modélisation, ..

English descriptors

KwdEn :
- Automatic proving, Constraint satisfaction, Decidability, Decision making, Modeling, Proof theory, Rewriting, Rewriting systems, Satisfiability, Satisfiability problem, Undecidability.

Abstract

In the context of combinations of theories with disjoint signatures, we classify the component theories according to the decidability of constraint satisfiability problems in arbitrary and in infinite models, respectively. We exhibit a theory Ti such that satisfiability is decidable, but satisfiability in infinite models is undecidable. It follows that satisfiability in T₁ U T₂ is undecidable, whenever T₂ has only infinite models, even if signatures are disjoint and satisfiability in T₂ is decidable. In the second part of the paper we strengthen the Nelson-Oppen decidability transfer result, by showing that it applies to theories over disjoint signatures, whose satisfiability problem, in either arbitrary or infinite models, is decidable. We show that. this result covers decision procedures based on rewriting, complementing recent work on combination of theories in the rewrite-based approach to satisfiability.

Notice en format standard (ISO 2709)

Pour connaître la documentation sur le format Inist Standard.

A05				`@2 4130`
A08	`01`	`1`	`ENG`	`@1 Decidability and undecidability results for nelson-oppen and rewrite-based decision procedures`
A09	`01`	`1`	`ENG`	`@1 Automated reasoning : Third international joint conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006 : proceedings`
A11	`01`	`1`		`@1 PAOLA BONACINA (Maria)`
A11	`02`	`1`		`@1 GHILARDI (Silvio)`
A11	`03`	`1`		`@1 NICOLINI (Enrica)`
A11	`04`	`1`		`@1 RANISE (Silvio)`
A11	`05`	`1`		`@1 ZUCCHELLI (Daniele)`
A12	`01`	`1`		`@1 FURBACH (Ulrich) @9 ed.`
A12	`02`	`1`		`@1 SHANKAR (Natarajan) @9 ed.`
A14	`01`			`@1 Dipartimento di Informtica, Università degli Studi di Verona @3 ITA @Z 1 aut.`
A14	`02`			`@1 Dipartimento di Informatica, Università degli Studi di Milano @3 ITA @Z 2 aut. @Z 4 aut. @Z 5 aut.`
A14	`03`			`@1 Dipartimento di Matematica, Università degli Studi di Milano @3 ITA @Z 3 aut.`
A14	`04`			`@1 LORIA & INRIA-Lorraine @2 Nancy @3 FRA @Z 4 aut. @Z 5 aut.`
A20				`@1 513-527`
A21				`@1 2006`
A23	`01`			`@0 ENG`
A26	`01`			`@0 3-540-37187-7`
A43	`01`			`@1 INIST @2 16343 @5 354000153610670400`
A44				`@0 0000 @1 © 2008 INIST-CNRS. All rights reserved.`
A45				`@0 24 ref.`
A47	`01`	`1`		`@0 08-0306266`
A60				`@1 P @2 C`
A61				`@0 A`
A64	`01`	`2`		`@0 Lecture notes in computer science`
A66	`01`			`@0 DEU`
C01	`01`		`ENG`	@0 In the context of combinations of theories with disjoint signatures, we classify the component theories according to the decidability of constraint satisfiability problems in arbitrary and in infinite models, respectively. We exhibit a theory Ti such that satisfiability is decidable, but satisfiability in infinite models is undecidable. It follows that satisfiability in T₁ U T₂ is undecidable, whenever T₂ has only infinite models, even if signatures are disjoint and satisfiability in T₂ is decidable. In the second part of the paper we strengthen the Nelson-Oppen decidability transfer result, by showing that it applies to theories over disjoint signatures, whose satisfiability problem, in either arbitrary or infinite models, is decidable. We show that. this result covers decision procedures based on rewriting, complementing recent work on combination of theories in the rewrite-based approach to satisfiability.
C02	`01`	`X`		`@0 001A02A01F`
C02	`02`	`X`		`@0 001D02A02`
C03	`01`	`X`	`FRE`	`@0 Décidabilité @5 06`
C03	`01`	`X`	`ENG`	`@0 Decidability @5 06`
C03	`01`	`X`	`SPA`	`@0 Decidibilidad @5 06`
C03	`02`	`X`	`FRE`	`@0 Théorie preuve @5 07`
C03	`02`	`X`	`ENG`	`@0 Proof theory @5 07`
C03	`02`	`X`	`SPA`	`@0 Teoría demonstración @5 07`
C03	`03`	`X`	`FRE`	`@0 Démonstration automatique @5 08`
C03	`03`	`X`	`ENG`	`@0 Automatic proving @5 08`
C03	`03`	`X`	`SPA`	`@0 Demostración automática @5 08`
C03	`04`	`3`	`FRE`	`@0 Système réécriture @5 09`
C03	`04`	`3`	`ENG`	`@0 Rewriting systems @5 09`
C03	`05`	`X`	`FRE`	`@0 Prise de décision @5 10`
C03	`05`	`X`	`ENG`	`@0 Decision making @5 10`
C03	`05`	`X`	`SPA`	`@0 Toma decision @5 10`
C03	`06`	`X`	`FRE`	`@0 Indécidabilité @5 18`
C03	`06`	`X`	`ENG`	`@0 Undecidability @5 18`
C03	`06`	`X`	`SPA`	`@0 Indecidibilidad @5 18`
C03	`07`	`X`	`FRE`	`@0 Satisfiabilité @5 19`
C03	`07`	`X`	`ENG`	`@0 Satisfiability @5 19`
C03	`07`	`X`	`SPA`	`@0 Satisfactibilidad @5 19`
C03	`08`	`X`	`FRE`	`@0 Réécriture @5 20`
C03	`08`	`X`	`ENG`	`@0 Rewriting @5 20`
C03	`08`	`X`	`SPA`	`@0 Reescritura @5 20`
C03	`09`	`X`	`FRE`	`@0 Satisfaction contrainte @5 23`
C03	`09`	`X`	`ENG`	`@0 Constraint satisfaction @5 23`
C03	`09`	`X`	`SPA`	`@0 Satisfaccion restricción @5 23`
C03	`10`	`X`	`FRE`	`@0 Problème satisfiabilité @5 24`
C03	`10`	`X`	`ENG`	`@0 Satisfiability problem @5 24`
C03	`10`	`X`	`SPA`	`@0 Problema satisfactibilidad @5 24`
C03	`11`	`X`	`FRE`	`@0 Modélisation @5 25`
C03	`11`	`X`	`ENG`	`@0 Modeling @5 25`
C03	`11`	`X`	`SPA`	`@0 Modelización @5 25`
C03	`12`	`X`	`FRE`	`@0 . @4 INC @5 82`
N21				`@1 189`
N44	`01`			`@1 OTO`
N82				`@1 OTO`

A30	`01`	`1`	`ENG`	`@1 International Joint Conference on Automated Reasoning @2 3 @3 Seattle Wa USA @4 2006`

Format Inist (serveur)

NO :	PASCAL 08-0306266 INIST
ET :	Decidability and undecidability results for nelson-oppen and rewrite-based decision procedures
AU :	PAOLA BONACINA (Maria); GHILARDI (Silvio); NICOLINI (Enrica); RANISE (Silvio); ZUCCHELLI (Daniele); FURBACH (Ulrich); SHANKAR (Natarajan)
AF :	Dipartimento di Informtica, Università degli Studi di Verona/Italie (1 aut.); Dipartimento di Informatica, Università degli Studi di Milano/Italie (2 aut., 4 aut., 5 aut.); Dipartimento di Matematica, Università degli Studi di Milano/Italie (3 aut.); LORIA & INRIA-Lorraine/Nancy/France (4 aut., 5 aut.)
DT :	Publication en série; Congrès; Niveau analytique
SO :	Lecture notes in computer science; Allemagne; Da. 2006; Vol. 4130; Pp. 513-527; Bibl. 24 ref.
LA :	Anglais
EA :	In the context of combinations of theories with disjoint signatures, we classify the component theories according to the decidability of constraint satisfiability problems in arbitrary and in infinite models, respectively. We exhibit a theory Ti such that satisfiability is decidable, but satisfiability in infinite models is undecidable. It follows that satisfiability in T₁ U T₂ is undecidable, whenever T₂ has only infinite models, even if signatures are disjoint and satisfiability in T₂ is decidable. In the second part of the paper we strengthen the Nelson-Oppen decidability transfer result, by showing that it applies to theories over disjoint signatures, whose satisfiability problem, in either arbitrary or infinite models, is decidable. We show that. this result covers decision procedures based on rewriting, complementing recent work on combination of theories in the rewrite-based approach to satisfiability.
CC :	001A02A01F; 001D02A02
FD :	Décidabilité; Théorie preuve; Démonstration automatique; Système réécriture; Prise de décision; Indécidabilité; Satisfiabilité; Réécriture; Satisfaction contrainte; Problème satisfiabilité; Modélisation; .
ED :	Decidability; Proof theory; Automatic proving; Rewriting systems; Decision making; Undecidability; Satisfiability; Rewriting; Constraint satisfaction; Satisfiability problem; Modeling
SD :	Decidibilidad; Teoría demonstración; Demostración automática; Toma decision; Indecidibilidad; Satisfactibilidad; Reescritura; Satisfaccion restricción; Problema satisfactibilidad; Modelización
LO :	INIST-16343.354000153610670400
ID :	08-0306266

Links to Exploration step

Pascal:08-0306266

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Decidability and undecidability results for nelson-oppen and rewrite-based decision procedures</title>
<author><name sortKey="Paola Bonacina, Maria" sort="Paola Bonacina, Maria" uniqKey="Paola Bonacina M" first="Maria" last="Paola Bonacina">Maria Paola Bonacina</name>
<affiliation><inist:fA14 i1="01"><s1>Dipartimento di Informtica, Università degli Studi di Verona</s1>
<s3>ITA</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Ghilardi, Silvio" sort="Ghilardi, Silvio" uniqKey="Ghilardi S" first="Silvio" last="Ghilardi">Silvio Ghilardi</name>
<affiliation><inist:fA14 i1="02"><s1>Dipartimento di Informatica, Università degli Studi di Milano</s1>
<s3>ITA</s3>
<sZ>2 aut.</sZ>
<sZ>4 aut.</sZ>
<sZ>5 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Nicolini, Enrica" sort="Nicolini, Enrica" uniqKey="Nicolini E" first="Enrica" last="Nicolini">Enrica Nicolini</name>
<affiliation><inist:fA14 i1="03"><s1>Dipartimento di Matematica, Università degli Studi di Milano</s1>
<s3>ITA</s3>
<sZ>3 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name>
<affiliation><inist:fA14 i1="02"><s1>Dipartimento di Informatica, Università degli Studi di Milano</s1>
<s3>ITA</s3>
<sZ>2 aut.</sZ>
<sZ>4 aut.</sZ>
<sZ>5 aut.</sZ>
</inist:fA14>
</affiliation>
<affiliation><inist:fA14 i1="04"><s1>LORIA & INRIA-Lorraine</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>4 aut.</sZ>
<sZ>5 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Zucchelli, Daniele" sort="Zucchelli, Daniele" uniqKey="Zucchelli D" first="Daniele" last="Zucchelli">Daniele Zucchelli</name>
<affiliation><inist:fA14 i1="02"><s1>Dipartimento di Informatica, Università degli Studi di Milano</s1>
<s3>ITA</s3>
<sZ>2 aut.</sZ>
<sZ>4 aut.</sZ>
<sZ>5 aut.</sZ>
</inist:fA14>
</affiliation>
<affiliation><inist:fA14 i1="04"><s1>LORIA & INRIA-Lorraine</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>4 aut.</sZ>
<sZ>5 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">08-0306266</idno>
<date when="2006">2006</date>
<idno type="stanalyst">PASCAL 08-0306266 INIST</idno>
<idno type="RBID">Pascal:08-0306266</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000308</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Decidability and undecidability results for nelson-oppen and rewrite-based decision procedures</title>
<author><name sortKey="Paola Bonacina, Maria" sort="Paola Bonacina, Maria" uniqKey="Paola Bonacina M" first="Maria" last="Paola Bonacina">Maria Paola Bonacina</name>
<affiliation><inist:fA14 i1="01"><s1>Dipartimento di Informtica, Università degli Studi di Verona</s1>
<s3>ITA</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Ghilardi, Silvio" sort="Ghilardi, Silvio" uniqKey="Ghilardi S" first="Silvio" last="Ghilardi">Silvio Ghilardi</name>
<affiliation><inist:fA14 i1="02"><s1>Dipartimento di Informatica, Università degli Studi di Milano</s1>
<s3>ITA</s3>
<sZ>2 aut.</sZ>
<sZ>4 aut.</sZ>
<sZ>5 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Nicolini, Enrica" sort="Nicolini, Enrica" uniqKey="Nicolini E" first="Enrica" last="Nicolini">Enrica Nicolini</name>
<affiliation><inist:fA14 i1="03"><s1>Dipartimento di Matematica, Università degli Studi di Milano</s1>
<s3>ITA</s3>
<sZ>3 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name>
<affiliation><inist:fA14 i1="02"><s1>Dipartimento di Informatica, Università degli Studi di Milano</s1>
<s3>ITA</s3>
<sZ>2 aut.</sZ>
<sZ>4 aut.</sZ>
<sZ>5 aut.</sZ>
</inist:fA14>
</affiliation>
<affiliation><inist:fA14 i1="04"><s1>LORIA & INRIA-Lorraine</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>4 aut.</sZ>
<sZ>5 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Zucchelli, Daniele" sort="Zucchelli, Daniele" uniqKey="Zucchelli D" first="Daniele" last="Zucchelli">Daniele Zucchelli</name>
<affiliation><inist:fA14 i1="02"><s1>Dipartimento di Informatica, Università degli Studi di Milano</s1>
<s3>ITA</s3>
<sZ>2 aut.</sZ>
<sZ>4 aut.</sZ>
<sZ>5 aut.</sZ>
</inist:fA14>
</affiliation>
<affiliation><inist:fA14 i1="04"><s1>LORIA & INRIA-Lorraine</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>4 aut.</sZ>
<sZ>5 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
</analytic>
<series><title level="j" type="main">Lecture notes in computer science</title>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><title level="j" type="main">Lecture notes in computer science</title>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Automatic proving</term>
<term>Constraint satisfaction</term>
<term>Decidability</term>
<term>Decision making</term>
<term>Modeling</term>
<term>Proof theory</term>
<term>Rewriting</term>
<term>Rewriting systems</term>
<term>Satisfiability</term>
<term>Satisfiability problem</term>
<term>Undecidability</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Décidabilité</term>
<term>Théorie preuve</term>
<term>Démonstration automatique</term>
<term>Système réécriture</term>
<term>Prise de décision</term>
<term>Indécidabilité</term>
<term>Satisfiabilité</term>
<term>Réécriture</term>
<term>Satisfaction contrainte</term>
<term>Problème satisfiabilité</term>
<term>Modélisation</term>
<term>.</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">In the context of combinations of theories with disjoint signatures, we classify the component theories according to the decidability of constraint satisfiability problems in arbitrary and in infinite models, respectively. We exhibit a theory Ti such that satisfiability is decidable, but satisfiability in infinite models is undecidable. It follows that satisfiability in T<sub>1</sub>
 U T<sub>2</sub>
 is undecidable, whenever T<sub>2</sub>
 has only infinite models, even if signatures are disjoint and satisfiability in T<sub>2</sub>
 is decidable. In the second part of the paper we strengthen the Nelson-Oppen decidability transfer result, by showing that it applies to theories over disjoint signatures, whose satisfiability problem, in either arbitrary or infinite models, is decidable. We show that. this result covers decision procedures based on rewriting, complementing recent work on combination of theories in the rewrite-based approach to satisfiability.</div>
</front>
</TEI>
<inist><standard h6="B"><pA><fA05><s2>4130</s2>
</fA05>
<fA08 i1="01" i2="1" l="ENG"><s1>Decidability and undecidability results for nelson-oppen and rewrite-based decision procedures</s1>
</fA08>
<fA09 i1="01" i2="1" l="ENG"><s1>Automated reasoning : Third international joint conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006 : proceedings</s1>
</fA09>
<fA11 i1="01" i2="1"><s1>PAOLA BONACINA (Maria)</s1>
</fA11>
<fA11 i1="02" i2="1"><s1>GHILARDI (Silvio)</s1>
</fA11>
<fA11 i1="03" i2="1"><s1>NICOLINI (Enrica)</s1>
</fA11>
<fA11 i1="04" i2="1"><s1>RANISE (Silvio)</s1>
</fA11>
<fA11 i1="05" i2="1"><s1>ZUCCHELLI (Daniele)</s1>
</fA11>
<fA12 i1="01" i2="1"><s1>FURBACH (Ulrich)</s1>
<s9>ed.</s9>
</fA12>
<fA12 i1="02" i2="1"><s1>SHANKAR (Natarajan)</s1>
<s9>ed.</s9>
</fA12>
<fA14 i1="01"><s1>Dipartimento di Informtica, Università degli Studi di Verona</s1>
<s3>ITA</s3>
<sZ>1 aut.</sZ>
</fA14>
<fA14 i1="02"><s1>Dipartimento di Informatica, Università degli Studi di Milano</s1>
<s3>ITA</s3>
<sZ>2 aut.</sZ>
<sZ>4 aut.</sZ>
<sZ>5 aut.</sZ>
</fA14>
<fA14 i1="03"><s1>Dipartimento di Matematica, Università degli Studi di Milano</s1>
<s3>ITA</s3>
<sZ>3 aut.</sZ>
</fA14>
<fA14 i1="04"><s1>LORIA & INRIA-Lorraine</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>4 aut.</sZ>
<sZ>5 aut.</sZ>
</fA14>
<fA20><s1>513-527</s1>
</fA20>
<fA21><s1>2006</s1>
</fA21>
<fA23 i1="01"><s0>ENG</s0>
</fA23>
<fA26 i1="01"><s0>3-540-37187-7</s0>
</fA26>
<fA43 i1="01"><s1>INIST</s1>
<s2>16343</s2>
<s5>354000153610670400</s5>
</fA43>
<fA44><s0>0000</s0>
<s1>© 2008 INIST-CNRS. All rights reserved.</s1>
</fA44>
<fA45><s0>24 ref.</s0>
</fA45>
<fA47 i1="01" i2="1"><s0>08-0306266</s0>
</fA47>
<fA60><s1>P</s1>
<s2>C</s2>
</fA60>
<fA61><s0>A</s0>
</fA61>
<fA64 i1="01" i2="2"><s0>Lecture notes in computer science</s0>
</fA64>
<fA66 i1="01"><s0>DEU</s0>
</fA66>
<fC01 i1="01" l="ENG"><s0>In the context of combinations of theories with disjoint signatures, we classify the component theories according to the decidability of constraint satisfiability problems in arbitrary and in infinite models, respectively. We exhibit a theory Ti such that satisfiability is decidable, but satisfiability in infinite models is undecidable. It follows that satisfiability in T<sub>1</sub>
 U T<sub>2</sub>
 is undecidable, whenever T<sub>2</sub>
 has only infinite models, even if signatures are disjoint and satisfiability in T<sub>2</sub>
 is decidable. In the second part of the paper we strengthen the Nelson-Oppen decidability transfer result, by showing that it applies to theories over disjoint signatures, whose satisfiability problem, in either arbitrary or infinite models, is decidable. We show that. this result covers decision procedures based on rewriting, complementing recent work on combination of theories in the rewrite-based approach to satisfiability.</s0>
</fC01>
<fC02 i1="01" i2="X"><s0>001A02A01F</s0>
</fC02>
<fC02 i1="02" i2="X"><s0>001D02A02</s0>
</fC02>
<fC03 i1="01" i2="X" l="FRE"><s0>Décidabilité</s0>
<s5>06</s5>
</fC03>
<fC03 i1="01" i2="X" l="ENG"><s0>Decidability</s0>
<s5>06</s5>
</fC03>
<fC03 i1="01" i2="X" l="SPA"><s0>Decidibilidad</s0>
<s5>06</s5>
</fC03>
<fC03 i1="02" i2="X" l="FRE"><s0>Théorie preuve</s0>
<s5>07</s5>
</fC03>
<fC03 i1="02" i2="X" l="ENG"><s0>Proof theory</s0>
<s5>07</s5>
</fC03>
<fC03 i1="02" i2="X" l="SPA"><s0>Teoría demonstración</s0>
<s5>07</s5>
</fC03>
<fC03 i1="03" i2="X" l="FRE"><s0>Démonstration automatique</s0>
<s5>08</s5>
</fC03>
<fC03 i1="03" i2="X" l="ENG"><s0>Automatic proving</s0>
<s5>08</s5>
</fC03>
<fC03 i1="03" i2="X" l="SPA"><s0>Demostración automática</s0>
<s5>08</s5>
</fC03>
<fC03 i1="04" i2="3" l="FRE"><s0>Système réécriture</s0>
<s5>09</s5>
</fC03>
<fC03 i1="04" i2="3" l="ENG"><s0>Rewriting systems</s0>
<s5>09</s5>
</fC03>
<fC03 i1="05" i2="X" l="FRE"><s0>Prise de décision</s0>
<s5>10</s5>
</fC03>
<fC03 i1="05" i2="X" l="ENG"><s0>Decision making</s0>
<s5>10</s5>
</fC03>
<fC03 i1="05" i2="X" l="SPA"><s0>Toma decision</s0>
<s5>10</s5>
</fC03>
<fC03 i1="06" i2="X" l="FRE"><s0>Indécidabilité</s0>
<s5>18</s5>
</fC03>
<fC03 i1="06" i2="X" l="ENG"><s0>Undecidability</s0>
<s5>18</s5>
</fC03>
<fC03 i1="06" i2="X" l="SPA"><s0>Indecidibilidad</s0>
<s5>18</s5>
</fC03>
<fC03 i1="07" i2="X" l="FRE"><s0>Satisfiabilité</s0>
<s5>19</s5>
</fC03>
<fC03 i1="07" i2="X" l="ENG"><s0>Satisfiability</s0>
<s5>19</s5>
</fC03>
<fC03 i1="07" i2="X" l="SPA"><s0>Satisfactibilidad</s0>
<s5>19</s5>
</fC03>
<fC03 i1="08" i2="X" l="FRE"><s0>Réécriture</s0>
<s5>20</s5>
</fC03>
<fC03 i1="08" i2="X" l="ENG"><s0>Rewriting</s0>
<s5>20</s5>
</fC03>
<fC03 i1="08" i2="X" l="SPA"><s0>Reescritura</s0>
<s5>20</s5>
</fC03>
<fC03 i1="09" i2="X" l="FRE"><s0>Satisfaction contrainte</s0>
<s5>23</s5>
</fC03>
<fC03 i1="09" i2="X" l="ENG"><s0>Constraint satisfaction</s0>
<s5>23</s5>
</fC03>
<fC03 i1="09" i2="X" l="SPA"><s0>Satisfaccion restricción</s0>
<s5>23</s5>
</fC03>
<fC03 i1="10" i2="X" l="FRE"><s0>Problème satisfiabilité</s0>
<s5>24</s5>
</fC03>
<fC03 i1="10" i2="X" l="ENG"><s0>Satisfiability problem</s0>
<s5>24</s5>
</fC03>
<fC03 i1="10" i2="X" l="SPA"><s0>Problema satisfactibilidad</s0>
<s5>24</s5>
</fC03>
<fC03 i1="11" i2="X" l="FRE"><s0>Modélisation</s0>
<s5>25</s5>
</fC03>
<fC03 i1="11" i2="X" l="ENG"><s0>Modeling</s0>
<s5>25</s5>
</fC03>
<fC03 i1="11" i2="X" l="SPA"><s0>Modelización</s0>
<s5>25</s5>
</fC03>
<fC03 i1="12" i2="X" l="FRE"><s0>.</s0>
<s4>INC</s4>
<s5>82</s5>
</fC03>
<fN21><s1>189</s1>
</fN21>
<fN44 i1="01"><s1>OTO</s1>
</fN44>
<fN82><s1>OTO</s1>
</fN82>
</pA>
<pR><fA30 i1="01" i2="1" l="ENG"><s1>International Joint Conference on Automated Reasoning</s1>
<s2>3</s2>
<s3>Seattle Wa USA</s3>
<s4>2006</s4>
</fA30>
</pR>
</standard>
<server><NO>PASCAL 08-0306266 INIST</NO>
<ET>Decidability and undecidability results for nelson-oppen and rewrite-based decision procedures</ET>
<AU>PAOLA BONACINA (Maria); GHILARDI (Silvio); NICOLINI (Enrica); RANISE (Silvio); ZUCCHELLI (Daniele); FURBACH (Ulrich); SHANKAR (Natarajan)</AU>
<AF>Dipartimento di Informtica, Università degli Studi di Verona/Italie (1 aut.); Dipartimento di Informatica, Università degli Studi di Milano/Italie (2 aut., 4 aut., 5 aut.); Dipartimento di Matematica, Università degli Studi di Milano/Italie (3 aut.); LORIA & INRIA-Lorraine/Nancy/France (4 aut., 5 aut.)</AF>
<DT>Publication en série; Congrès; Niveau analytique</DT>
<SO>Lecture notes in computer science; Allemagne; Da. 2006; Vol. 4130; Pp. 513-527; Bibl. 24 ref.</SO>
<LA>Anglais</LA>
<EA>In the context of combinations of theories with disjoint signatures, we classify the component theories according to the decidability of constraint satisfiability problems in arbitrary and in infinite models, respectively. We exhibit a theory Ti such that satisfiability is decidable, but satisfiability in infinite models is undecidable. It follows that satisfiability in T<sub>1</sub>
 U T<sub>2</sub>
 is undecidable, whenever T<sub>2</sub>
 has only infinite models, even if signatures are disjoint and satisfiability in T<sub>2</sub>
 is decidable. In the second part of the paper we strengthen the Nelson-Oppen decidability transfer result, by showing that it applies to theories over disjoint signatures, whose satisfiability problem, in either arbitrary or infinite models, is decidable. We show that. this result covers decision procedures based on rewriting, complementing recent work on combination of theories in the rewrite-based approach to satisfiability.</EA>
<CC>001A02A01F; 001D02A02</CC>
<FD>Décidabilité; Théorie preuve; Démonstration automatique; Système réécriture; Prise de décision; Indécidabilité; Satisfiabilité; Réécriture; Satisfaction contrainte; Problème satisfiabilité; Modélisation; .</FD>
<ED>Decidability; Proof theory; Automatic proving; Rewriting systems; Decision making; Undecidability; Satisfiability; Rewriting; Constraint satisfaction; Satisfiability problem; Modeling</ED>
<SD>Decidibilidad; Teoría demonstración; Demostración automática; Toma decision; Indecidibilidad; Satisfactibilidad; Reescritura; Satisfaccion restricción; Problema satisfactibilidad; Modelización</SD>
<LO>INIST-16343.354000153610670400</LO>
<ID>08-0306266</ID>
</server>
</inist>
</record>

Pour manipuler ce document sous Unix (Dilib)

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

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

HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000308 | SxmlIndent | more

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

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    PascalFrancis
   |étape=   Corpus
   |type=    RBID
   |clé=     Pascal:08-0306266
   |texte=   Decidability and undecidability results for nelson-oppen and rewrite-based decision procedures
}}

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

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

Serveur d'exploration sur la recherche en informatique en Lorraine

Decidability and undecidability results for nelson-oppen and rewrite-based decision procedures

Decidability and undecidability results for nelson-oppen and rewrite-based decision procedures

Source :

Descripteurs français

English descriptors

Abstract

Notice en format standard (ISO 2709)

Format Inist (serveur)

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