InforLorV4, Main, Exploration, bibRecord, 007B76

A rewriting approach to satisfiability procedures

Identifieur interne : 007B76 ( Main/Exploration ); précédent : 007B75; suivant : 007B77

A rewriting approach to satisfiability procedures

Auteurs : Alessandro Armando [Italie] ; Silvio Ranise [Italie, France] ; Michaël Rusinowitch [France]

Source :

Information and computation : (Print) [ 0890-5401 ] ; 2003.

RBID : Pascal:03-0426820

Descripteurs français

Pascal (Inist)
- Informatique théorique, Logique mathématique, Système réécriture, Théorie preuve, Traitement liste, Homomorphisme, Extension, Satisfaisabilité, Logique ordre 1, Superposition, Cryptage, Logique équationnelle, Déduction automatique, Réécriture terme, Procédure décision.

English descriptors

KwdEn :
- Automated deduction, Computer theory, Decision procedure, Encryption, Equational logic, Extension, First order logic, Homomorphism, List processing, Mathematical logic, Proof theory, Rewriting systems, Satisfiability, Superposition, Term rewriting.

Abstract

We show how a well-known superposition-based inference system for first-order equational logic can be used almost directly for deciding satisfiability in various theories including lists, encryption, extensional arrays, extensional finite sets, and combinations of them. We also give a superposition-based decision procedure for homomorphism.

Affiliations:

Links toward previous steps (curation, corpus...)

to stream PascalFrancis, to step Corpus: 000763
to stream PascalFrancis, to step Curation: 000280
to stream PascalFrancis, to step Checkpoint: 000732
to stream Main, to step Merge: 007F91
to stream Main, to step Curation: 007B76

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">A rewriting approach to satisfiability procedures</title>
<author><name sortKey="Armando, Alessandro" sort="Armando, Alessandro" uniqKey="Armando A" first="Alessandro" last="Armando">Alessandro Armando</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>DIST-Università degli Studi di Genova, via all'Opera Pia 13</s1>
<s2>Genova 16145</s2>
<s3>ITA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>Italie</country>
<wicri:noRegion>Genova 16145</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>DIST-Università degli Studi di Genova, via all'Opera Pia 13</s1>
<s2>Genova 16145</s2>
<s3>ITA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>Italie</country>
<wicri:noRegion>Genova 16145</wicri:noRegion>
</affiliation>
<affiliation wicri:level="3"><inist:fA14 i1="02"><s1>LORIA & INRIA-Lorraine, 615, rue du Jardin Botanique, BP 101</s1>
<s2>Villers les Nancy 54602</s2>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
</placeName>
</affiliation>
</author>
<author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michaël" last="Rusinowitch">Michaël Rusinowitch</name>
<affiliation wicri:level="3"><inist:fA14 i1="02"><s1>LORIA & INRIA-Lorraine, 615, rue du Jardin Botanique, BP 101</s1>
<s2>Villers les Nancy 54602</s2>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
</placeName>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">03-0426820</idno>
<date when="2003">2003</date>
<idno type="stanalyst">PASCAL 03-0426820 INIST</idno>
<idno type="RBID">Pascal:03-0426820</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000763</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000280</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000732</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000732</idno>
<idno type="wicri:doubleKey">0890-5401:2003:Armando A:a:rewriting:approach</idno>
<idno type="wicri:Area/Main/Merge">007F91</idno>
<idno type="wicri:Area/Main/Curation">007B76</idno>
<idno type="wicri:Area/Main/Exploration">007B76</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">A rewriting approach to satisfiability procedures</title>
<author><name sortKey="Armando, Alessandro" sort="Armando, Alessandro" uniqKey="Armando A" first="Alessandro" last="Armando">Alessandro Armando</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>DIST-Università degli Studi di Genova, via all'Opera Pia 13</s1>
<s2>Genova 16145</s2>
<s3>ITA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>Italie</country>
<wicri:noRegion>Genova 16145</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>DIST-Università degli Studi di Genova, via all'Opera Pia 13</s1>
<s2>Genova 16145</s2>
<s3>ITA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>Italie</country>
<wicri:noRegion>Genova 16145</wicri:noRegion>
</affiliation>
<affiliation wicri:level="3"><inist:fA14 i1="02"><s1>LORIA & INRIA-Lorraine, 615, rue du Jardin Botanique, BP 101</s1>
<s2>Villers les Nancy 54602</s2>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
</placeName>
</affiliation>
</author>
<author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michaël" last="Rusinowitch">Michaël Rusinowitch</name>
<affiliation wicri:level="3"><inist:fA14 i1="02"><s1>LORIA & INRIA-Lorraine, 615, rue du Jardin Botanique, BP 101</s1>
<s2>Villers les Nancy 54602</s2>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
</placeName>
</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="2003">2003</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>Automated deduction</term>
<term>Computer theory</term>
<term>Decision procedure</term>
<term>Encryption</term>
<term>Equational logic</term>
<term>Extension</term>
<term>First order logic</term>
<term>Homomorphism</term>
<term>List processing</term>
<term>Mathematical logic</term>
<term>Proof theory</term>
<term>Rewriting systems</term>
<term>Satisfiability</term>
<term>Superposition</term>
<term>Term rewriting</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Informatique théorique</term>
<term>Logique mathématique</term>
<term>Système réécriture</term>
<term>Théorie preuve</term>
<term>Traitement liste</term>
<term>Homomorphisme</term>
<term>Extension</term>
<term>Satisfaisabilité</term>
<term>Logique ordre 1</term>
<term>Superposition</term>
<term>Cryptage</term>
<term>Logique équationnelle</term>
<term>Déduction automatique</term>
<term>Réécriture terme</term>
<term>Procédure décision</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">We show how a well-known superposition-based inference system for first-order equational logic can be used almost directly for deciding satisfiability in various theories including lists, encryption, extensional arrays, extensional finite sets, and combinations of them. We also give a superposition-based decision procedure for homomorphism.</div>
</front>
</TEI>
<affiliations><list><country><li>France</li>
<li>Italie</li>
</country>
<region><li>Grand Est</li>
<li>Lorraine (région)</li>
</region>
</list>
<tree><country name="Italie"><noRegion><name sortKey="Armando, Alessandro" sort="Armando, Alessandro" uniqKey="Armando A" first="Alessandro" last="Armando">Alessandro Armando</name>
</noRegion>
<name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name>
</country>
<country name="France"><region name="Grand Est"><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name>
</region>
<name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michaël" last="Rusinowitch">Michaël Rusinowitch</name>
</country>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration

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

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 007B76 | SxmlIndent | more

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

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     Pascal:03-0426820
   |texte=   A rewriting approach to satisfiability 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

A rewriting approach to satisfiability procedures

A rewriting approach to satisfiability procedures

Source :

Descripteurs français

English descriptors

Abstract

Links toward previous steps (curation, corpus...)

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

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