On a rewriting approach to satisfiability procedures : Extension, combination of theories and an experimental appraisal
Identifieur interne : 006610 ( Main/Merge ); précédent : 006609; suivant : 006611On a rewriting approach to satisfiability procedures : Extension, combination of theories and an experimental appraisal
Auteurs : Alessandro Armando [Italie] ; Maria Paola Bonacina [Italie] ; Silvio Ranise [France] ; Stephan Schulz [Italie]Source :
- Lecture notes in computer science [ 0302-9743 ] ; 2005.
Descripteurs français
- Pascal (Inist)
English descriptors
- KwdEn :
Abstract
The rewriting approach to T-satisfiability is based on establishing termination of a rewrite-based inference system for first-order logic on the T-satisfiability problem. Extending previous such results, including the quantifier-free theory of equality and the theory of arrays with or without extensionality, we prove termination for the theories of records with or without extensionality, integer offsets and integer offsets modulo. A general theorem for termination on combinations of theories, that covers any combination of the theories above, is given next. For empirical evaluation, the rewrite-based theorem prover E is compared with the validity checkers CVC and CVC Lite, on both synthetic and real-world benchmarks, including both valid and invalid instances. Parametric synthetic benchmarks test scalability, while real-world benchmarks test ability to handle huge sets of literals. Contrary to the folklore that a general-purpose prover cannot compete with specialized reasoners, the experiments are overall favorable to the theorem prover, showing that the rewriting approach is both elegant and practical.
Links toward previous steps (curation, corpus...)
- to stream PascalFrancis, to step Corpus: 000510
- to stream PascalFrancis, to step Curation: 000528
- to stream PascalFrancis, to step Checkpoint: 000473
Links to Exploration step
Pascal:05-0448349Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">On a rewriting approach to satisfiability procedures : Extension, combination of theories and an experimental appraisal</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, Viale Causa 13</s1><s2>16145 Genova</s2><s3>ITA</s3><sZ>1 aut.</sZ></inist:fA14><country>Italie</country><wicri:noRegion>16145 Genova</wicri:noRegion></affiliation></author><author><name sortKey="Bonacina, Maria Paola" sort="Bonacina, Maria Paola" uniqKey="Bonacina M" first="Maria Paola" last="Bonacina">Maria Paola Bonacina</name><affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Dipartimento di Informatica, Università degli Studi di Verona, Strada Le Grazie 15</s1><s2>37134 Verona</s2><s3>ITA</s3><sZ>2 aut.</sZ><sZ>4 aut.</sZ></inist:fA14><country>Italie</country><wicri:noRegion>37134 Verona</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="3"><inist:fA14 i1="03"><s1>LORIA & INRIA-Lorraine, 615 Rue du Jardin Botanique</s1><s2>54600 Villers-lès-Nancy</s2><s3>FRA</s3><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><settlement type="city">Villers-lès-Nancy</settlement></placeName></affiliation></author><author><name sortKey="Schulz, Stephan" sort="Schulz, Stephan" uniqKey="Schulz S" first="Stephan" last="Schulz">Stephan Schulz</name><affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Dipartimento di Informatica, Università degli Studi di Verona, Strada Le Grazie 15</s1><s2>37134 Verona</s2><s3>ITA</s3><sZ>2 aut.</sZ><sZ>4 aut.</sZ></inist:fA14><country>Italie</country><wicri:noRegion>37134 Verona</wicri:noRegion></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">INIST</idno><idno type="inist">05-0448349</idno><date when="2005">2005</date><idno type="stanalyst">PASCAL 05-0448349 INIST</idno><idno type="RBID">Pascal:05-0448349</idno><idno type="wicri:Area/PascalFrancis/Corpus">000510</idno><idno type="wicri:Area/PascalFrancis/Curation">000528</idno><idno type="wicri:Area/PascalFrancis/Checkpoint">000473</idno><idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000473</idno><idno type="wicri:doubleKey">0302-9743:2005:Armando A:on:a:rewriting</idno><idno type="wicri:Area/Main/Merge">006610</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">On a rewriting approach to satisfiability procedures : Extension, combination of theories and an experimental appraisal</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, Viale Causa 13</s1><s2>16145 Genova</s2><s3>ITA</s3><sZ>1 aut.</sZ></inist:fA14><country>Italie</country><wicri:noRegion>16145 Genova</wicri:noRegion></affiliation></author><author><name sortKey="Bonacina, Maria Paola" sort="Bonacina, Maria Paola" uniqKey="Bonacina M" first="Maria Paola" last="Bonacina">Maria Paola Bonacina</name><affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Dipartimento di Informatica, Università degli Studi di Verona, Strada Le Grazie 15</s1><s2>37134 Verona</s2><s3>ITA</s3><sZ>2 aut.</sZ><sZ>4 aut.</sZ></inist:fA14><country>Italie</country><wicri:noRegion>37134 Verona</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="3"><inist:fA14 i1="03"><s1>LORIA & INRIA-Lorraine, 615 Rue du Jardin Botanique</s1><s2>54600 Villers-lès-Nancy</s2><s3>FRA</s3><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><settlement type="city">Villers-lès-Nancy</settlement></placeName></affiliation></author><author><name sortKey="Schulz, Stephan" sort="Schulz, Stephan" uniqKey="Schulz S" first="Stephan" last="Schulz">Stephan Schulz</name><affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Dipartimento di Informatica, Università degli Studi di Verona, Strada Le Grazie 15</s1><s2>37134 Verona</s2><s3>ITA</s3><sZ>2 aut.</sZ><sZ>4 aut.</sZ></inist:fA14><country>Italie</country><wicri:noRegion>37134 Verona</wicri:noRegion></affiliation></author></analytic><series><title level="j" type="main">Lecture notes in computer science</title><idno type="ISSN">0302-9743</idno><imprint><date when="2005">2005</date></imprint></series></biblStruct></sourceDesc><seriesStmt><title level="j" type="main">Lecture notes in computer science</title><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>First order logic</term><term>Inference</term><term>Logical programming</term><term>Parametric test</term><term>Proof theory</term><term>Quantifier</term><term>Rewriting</term><term>Rewriting systems</term><term>Satisfiability</term><term>Satisfiability problem</term><term>Scalability</term><term>Termination problem</term><term>Theorem proving</term></keywords><keywords scheme="Pascal" xml:lang="fr"><term>Programmation logique</term><term>Système réécriture</term><term>Inférence</term><term>Logique ordre 1</term><term>Démonstration théorème</term><term>Théorie preuve</term><term>Extensibilité</term><term>Réécriture</term><term>Satisfiabilité</term><term>Quantificateur</term><term>Test paramétrique</term><term>Problème terminaison</term><term>Problème satisfiabilité</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">The rewriting approach to T-satisfiability is based on establishing termination of a rewrite-based inference system for first-order logic on the T-satisfiability problem. Extending previous such results, including the quantifier-free theory of equality and the theory of arrays with or without extensionality, we prove termination for the theories of records with or without extensionality, integer offsets and integer offsets modulo. A general theorem for termination on combinations of theories, that covers any combination of the theories above, is given next. For empirical evaluation, the rewrite-based theorem prover E is compared with the validity checkers CVC and CVC Lite, on both synthetic and real-world benchmarks, including both valid and invalid instances. Parametric synthetic benchmarks test scalability, while real-world benchmarks test ability to handle huge sets of literals. Contrary to the folklore that a general-purpose prover cannot compete with specialized reasoners, the experiments are overall favorable to the theorem prover, showing that the rewriting approach is both elegant and practical.</div></front></TEI><affiliations><list><country><li>France</li><li>Italie</li></country><region><li>Grand Est</li><li>Lorraine (région)</li></region><settlement><li>Villers-lès-Nancy</li></settlement></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="Bonacina, Maria Paola" sort="Bonacina, Maria Paola" uniqKey="Bonacina M" first="Maria Paola" last="Bonacina">Maria Paola Bonacina</name><name sortKey="Schulz, Stephan" sort="Schulz, Stephan" uniqKey="Schulz S" first="Stephan" last="Schulz">Stephan Schulz</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></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 006610 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 006610 | 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:05-0448349
|texte= On a rewriting approach to satisfiability procedures : Extension, combination of theories and an experimental appraisal
}}
| This area was generated with Dilib version V0.6.33. |  |