Specification and proof in membership equational logic
Identifieur interne :
000C52 ( PascalFrancis/Corpus );
précédent :
000C51;
suivant :
000C53
Specification and proof in membership equational logic
Auteurs : A. Bouhoula ;
J.-P. Jouannaud ;
J. MeseguerSource :
-
Lecture notes in computer science [ 0302-9743 ] ; 1997.
RBID : Pascal:97-0390438
Descripteurs français
English descriptors
Abstract
This paper is part of a long-term effort to increase expressiveness of algebraic specification languages while at the same time having a simple semantic basis on which efficient execution by rewriting and powerful theorem-proving tools can be based. In particular, our rewriting techniques provide semantic foundations for Maude's functional sublanguage, where they have been efficiently implemented. Membership equational logic is quite simple, and yet quite powerful. Its atomic formulae are equations and sort membership assertions, and its sentences are Horn clauses. It extends in a conservative way both order-sorted equational logic and partial algebra approaches, while Horn logic can be very easily encoded. After introducing the basic concepts of the logic, we give conditions and proof rules with which efficient equational deduction by rewriting can be achieved. We also give completion techniques to transform a specification into one meeting these conditions. We address the important issue of proving sufficient completeness of a specification. Using tree-automata techniques, we develop a test set based approach for proving inductive theorems about a specification Narrowing and proof techniques for parameterized specifications are investigated as well. Finally, we discuss the generality of our approach and how it extends several previous approaches.
Notice en format standard (ISO 2709)
Pour connaître la documentation sur le format Inist Standard.
| pA |
| A01 | 01 | 1 | | @0 0302-9743 |
|---|
| A05 | | | | @2 1214 |
|---|
| A08 | 01 | 1 | ENG | @1 Specification and proof in membership equational logic |
|---|
| A09 | 01 | 1 | ENG | @1 TAPSOFT '97 : theory and practice of software development : Lille, April 14-18, 1997 |
|---|
| A11 | 01 | 1 | | @1 BOUHOULA (A.) |
|---|
| A11 | 02 | 1 | | @1 JOUANNAUD (J.-P.) |
|---|
| A11 | 03 | 1 | | @1 MESEGUER (J.) |
|---|
| A12 | 01 | 1 | | @1 BIDOIT (Michel) @9 ed. |
|---|
| A12 | 02 | 1 | | @1 DAUCHET (Max) @9 ed. |
|---|
| A14 | 01 | | | @1 SRI International, Computer Science Laboratory, n 333 Ravenswood Avenue @2 Menlo Park, California 94025 @3 USA @Z 1 aut. @Z 2 aut. @Z 3 aut. |
|---|
| A14 | 02 | | | @1 INRIA Lorraine and CRIN, 615 rue du Jardin Botanique, B.P. 101 @2 54602 Villers-lès-Nancy @3 FRA @Z 1 aut. |
|---|
| A14 | 03 | | | @1 LRI, CNRS and Université de Paris-Sud, Bât 405 @2 91405 Orsay @3 FRA @Z 2 aut. |
|---|
| A20 | | | | @1 67-92 |
|---|
| A21 | | | | @1 1997 |
|---|
| A23 | 01 | | | @0 ENG |
|---|
| A43 | 01 | | | @1 INIST @2 16343 @5 354000062523660080 |
|---|
| A44 | | | | @0 0000 @1 © 1997 INIST-CNRS. All rights reserved. |
|---|
| A45 | | | | @0 25 ref. |
|---|
| A47 | 01 | 1 | | @0 97-0390438 |
|---|
| A60 | | | | @1 P @2 C |
|---|
| A61 | | | | @0 A |
|---|
| A64 | 01 | 1 | | @0 Lecture notes in computer science |
|---|
| A66 | 01 | | | @0 DEU |
|---|
| A66 | 02 | | | @0 USA |
|---|
| C01 | 01 | | ENG | @0 This paper is part of a long-term effort to increase expressiveness of algebraic specification languages while at the same time having a simple semantic basis on which efficient execution by rewriting and powerful theorem-proving tools can be based. In particular, our rewriting techniques provide semantic foundations for Maude's functional sublanguage, where they have been efficiently implemented. Membership equational logic is quite simple, and yet quite powerful. Its atomic formulae are equations and sort membership assertions, and its sentences are Horn clauses. It extends in a conservative way both order-sorted equational logic and partial algebra approaches, while Horn logic can be very easily encoded. After introducing the basic concepts of the logic, we give conditions and proof rules with which efficient equational deduction by rewriting can be achieved. We also give completion techniques to transform a specification into one meeting these conditions. We address the important issue of proving sufficient completeness of a specification. Using tree-automata techniques, we develop a test set based approach for proving inductive theorems about a specification Narrowing and proof techniques for parameterized specifications are investigated as well. Finally, we discuss the generality of our approach and how it extends several previous approaches. |
|---|
| C02 | 01 | X | | @0 001D02A02 |
|---|
| C03 | 01 | X | FRE | @0 Informatique théorique @5 01 |
|---|
| C03 | 01 | X | ENG | @0 Computer theory @5 01 |
|---|
| C03 | 01 | X | SPA | @0 Informática teórica @5 01 |
|---|
| C03 | 02 | X | FRE | @0 Théorie langage @5 02 |
|---|
| C03 | 02 | X | ENG | @0 Language theory @5 02 |
|---|
| C03 | 02 | X | SPA | @0 Teoría lenguaje @5 02 |
|---|
| C03 | 03 | X | FRE | @0 Sémantique opérationnelle @5 03 |
|---|
| C03 | 03 | X | ENG | @0 Operational semantics @5 03 |
|---|
| C03 | 03 | X | SPA | @0 Semantica operacional @5 03 |
|---|
| N21 | | | | @1 237 |
|---|
|
|---|
| pR |
| A30 | 01 | 1 | ENG | @1 International conference on vector and parallel processing @2 2 @3 Porto PRT @4 1996-09-25 |
|---|
|
|---|
Format Inist (serveur)
| NO : | PASCAL 97-0390438 INIST |
|---|
| ET : | Specification and proof in membership equational logic |
|---|
| AU : | BOUHOULA (A.); JOUANNAUD (J.-P.); MESEGUER (J.); BIDOIT (Michel); DAUCHET (Max) |
|---|
| AF : | SRI International, Computer Science Laboratory, n 333 Ravenswood Avenue/Menlo Park, California 94025/Etats-Unis (1 aut., 2 aut., 3 aut.); INRIA Lorraine and CRIN, 615 rue du Jardin Botanique, B.P. 101/54602 Villers-lès-Nancy/France (1 aut.); LRI, CNRS and Université de Paris-Sud, Bât 405/91405 Orsay/France (2 aut.) |
|---|
| DT : | Publication en série; Congrès; Niveau analytique |
|---|
| SO : | Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 1997; Vol. 1214; Pp. 67-92; Bibl. 25 ref. |
|---|
| LA : | Anglais |
|---|
| EA : | This paper is part of a long-term effort to increase expressiveness of algebraic specification languages while at the same time having a simple semantic basis on which efficient execution by rewriting and powerful theorem-proving tools can be based. In particular, our rewriting techniques provide semantic foundations for Maude's functional sublanguage, where they have been efficiently implemented. Membership equational logic is quite simple, and yet quite powerful. Its atomic formulae are equations and sort membership assertions, and its sentences are Horn clauses. It extends in a conservative way both order-sorted equational logic and partial algebra approaches, while Horn logic can be very easily encoded. After introducing the basic concepts of the logic, we give conditions and proof rules with which efficient equational deduction by rewriting can be achieved. We also give completion techniques to transform a specification into one meeting these conditions. We address the important issue of proving sufficient completeness of a specification. Using tree-automata techniques, we develop a test set based approach for proving inductive theorems about a specification Narrowing and proof techniques for parameterized specifications are investigated as well. Finally, we discuss the generality of our approach and how it extends several previous approaches. |
|---|
| CC : | 001D02A02 |
|---|
| FD : | Informatique théorique; Théorie langage; Sémantique opérationnelle |
|---|
| ED : | Computer theory; Language theory; Operational semantics |
|---|
| SD : | Informática teórica; Teoría lenguaje; Semantica operacional |
|---|
| LO : | INIST-16343.354000062523660080 |
|---|
| ID : | 97-0390438 |
|---|
Links to Exploration step
Pascal:97-0390438
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Specification and proof in membership equational logic</title>
<author><name sortKey="Bouhoula, A" sort="Bouhoula, A" uniqKey="Bouhoula A" first="A." last="Bouhoula">A. Bouhoula</name>
<affiliation><inist:fA14 i1="01"><s1>SRI International, Computer Science Laboratory, n 333 Ravenswood Avenue</s1>
<s2>Menlo Park, California 94025</s2>
<s3>USA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14><affiliation><inist:fA14 i1="02"><s1>INRIA Lorraine and CRIN, 615 rue du Jardin Botanique, B.P. 101</s1>
<s2>54602 Villers-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</inist:fA14><author><name sortKey="Jouannaud, J P" sort="Jouannaud, J P" uniqKey="Jouannaud J" first="J.-P." last="Jouannaud">J.-P. Jouannaud</name>
<affiliation><inist:fA14 i1="01"><s1>SRI International, Computer Science Laboratory, n 333 Ravenswood Avenue</s1>
<s2>Menlo Park, California 94025</s2>
<s3>USA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14><affiliation><inist:fA14 i1="03"><s1>LRI, CNRS and Université de Paris-Sud, Bât 405</s1>
<s2>91405 Orsay</s2>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</inist:fA14><author><name sortKey="Meseguer, J" sort="Meseguer, J" uniqKey="Meseguer J" first="J." last="Meseguer">J. Meseguer</name>
<affiliation><inist:fA14 i1="01"><s1>SRI International, Computer Science Laboratory, n 333 Ravenswood Avenue</s1>
<s2>Menlo Park, California 94025</s2>
<s3>USA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14><publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">97-0390438</idno>
<date when="1997">1997</date>
<idno type="stanalyst">PASCAL 97-0390438 INIST</idno>
<idno type="RBID">Pascal:97-0390438</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000C52</idno>
</publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Specification and proof in membership equational logic</title>
<author><name sortKey="Bouhoula, A" sort="Bouhoula, A" uniqKey="Bouhoula A" first="A." last="Bouhoula">A. Bouhoula</name>
<affiliation><inist:fA14 i1="01"><s1>SRI International, Computer Science Laboratory, n 333 Ravenswood Avenue</s1>
<s2>Menlo Park, California 94025</s2>
<s3>USA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14><affiliation><inist:fA14 i1="02"><s1>INRIA Lorraine and CRIN, 615 rue du Jardin Botanique, B.P. 101</s1>
<s2>54602 Villers-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</inist:fA14><author><name sortKey="Jouannaud, J P" sort="Jouannaud, J P" uniqKey="Jouannaud J" first="J.-P." last="Jouannaud">J.-P. Jouannaud</name>
<affiliation><inist:fA14 i1="01"><s1>SRI International, Computer Science Laboratory, n 333 Ravenswood Avenue</s1>
<s2>Menlo Park, California 94025</s2>
<s3>USA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14><affiliation><inist:fA14 i1="03"><s1>LRI, CNRS and Université de Paris-Sud, Bât 405</s1>
<s2>91405 Orsay</s2>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</inist:fA14><author><name sortKey="Meseguer, J" sort="Meseguer, J" uniqKey="Meseguer J" first="J." last="Meseguer">J. Meseguer</name>
<affiliation><inist:fA14 i1="01"><s1>SRI International, Computer Science Laboratory, n 333 Ravenswood Avenue</s1>
<s2>Menlo Park, California 94025</s2>
<s3>USA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14><series><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
<imprint><date when="1997">1997</date>
</imprint><seriesStmt><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
</seriesStmt><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Computer theory</term>
<term>Language theory</term>
<term>Operational semantics</term>
</keywords><keywords scheme="Pascal" xml:lang="fr"><term>Informatique théorique</term>
<term>Théorie langage</term>
<term>Sémantique opérationnelle</term>
</keywords><front><div type="abstract" xml:lang="en">This paper is part of a long-term effort to increase expressiveness of algebraic specification languages while at the same time having a simple semantic basis on which efficient execution by rewriting and powerful theorem-proving tools can be based. In particular, our rewriting techniques provide semantic foundations for Maude's functional sublanguage, where they have been efficiently implemented. Membership equational logic is quite simple, and yet quite powerful. Its atomic formulae are equations and sort membership assertions, and its sentences are Horn clauses. It extends in a conservative way both order-sorted equational logic and partial algebra approaches, while Horn logic can be very easily encoded. After introducing the basic concepts of the logic, we give conditions and proof rules with which efficient equational deduction by rewriting can be achieved. We also give completion techniques to transform a specification into one meeting these conditions. We address the important issue of proving sufficient completeness of a specification. Using tree-automata techniques, we develop a test set based approach for proving inductive theorems about a specification Narrowing and proof techniques for parameterized specifications are investigated as well. Finally, we discuss the generality of our approach and how it extends several previous approaches.</div>
</front><inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0302-9743</s0>
</fA01><fA05><s2>1214</s2>
</fA05><fA08 i1="01" i2="1" l="ENG"><s1>Specification and proof in membership equational logic</s1>
</fA08><fA09 i1="01" i2="1" l="ENG"><s1>TAPSOFT '97 : theory and practice of software development : Lille, April 14-18, 1997</s1>
</fA09><fA11 i1="01" i2="1"><s1>BOUHOULA (A.)</s1>
</fA11><fA11 i1="02" i2="1"><s1>JOUANNAUD (J.-P.)</s1>
</fA11><fA11 i1="03" i2="1"><s1>MESEGUER (J.)</s1>
</fA11><fA12 i1="01" i2="1"><s1>BIDOIT (Michel)</s1>
<s9>ed.</s9>
</fA12><fA12 i1="02" i2="1"><s1>DAUCHET (Max)</s1>
<s9>ed.</s9>
</fA12><fA14 i1="01"><s1>SRI International, Computer Science Laboratory, n 333 Ravenswood Avenue</s1>
<s2>Menlo Park, California 94025</s2>
<s3>USA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</fA14><fA14 i1="02"><s1>INRIA Lorraine and CRIN, 615 rue du Jardin Botanique, B.P. 101</s1>
<s2>54602 Villers-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</fA14><fA14 i1="03"><s1>LRI, CNRS and Université de Paris-Sud, Bât 405</s1>
<s2>91405 Orsay</s2>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</fA14><fA20><s1>67-92</s1>
</fA20><fA21><s1>1997</s1>
</fA21><fA23 i1="01"><s0>ENG</s0>
</fA23><fA43 i1="01"><s1>INIST</s1>
<s2>16343</s2>
<s5>354000062523660080</s5>
</fA43><fA44><s0>0000</s0>
<s1>© 1997 INIST-CNRS. All rights reserved.</s1>
</fA44><fA45><s0>25 ref.</s0>
</fA45><fA47 i1="01" i2="1"><s0>97-0390438</s0>
</fA47><fA60><s1>P</s1>
<s2>C</s2>
</fA60><fA64 i1="01" i2="1"><s0>Lecture notes in computer science</s0>
</fA64><fA66 i1="01"><s0>DEU</s0>
</fA66><fA66 i1="02"><s0>USA</s0>
</fA66><fC01 i1="01" l="ENG"><s0>This paper is part of a long-term effort to increase expressiveness of algebraic specification languages while at the same time having a simple semantic basis on which efficient execution by rewriting and powerful theorem-proving tools can be based. In particular, our rewriting techniques provide semantic foundations for Maude's functional sublanguage, where they have been efficiently implemented. Membership equational logic is quite simple, and yet quite powerful. Its atomic formulae are equations and sort membership assertions, and its sentences are Horn clauses. It extends in a conservative way both order-sorted equational logic and partial algebra approaches, while Horn logic can be very easily encoded. After introducing the basic concepts of the logic, we give conditions and proof rules with which efficient equational deduction by rewriting can be achieved. We also give completion techniques to transform a specification into one meeting these conditions. We address the important issue of proving sufficient completeness of a specification. Using tree-automata techniques, we develop a test set based approach for proving inductive theorems about a specification Narrowing and proof techniques for parameterized specifications are investigated as well. Finally, we discuss the generality of our approach and how it extends several previous approaches.</s0>
</fC01><fC02 i1="01" i2="X"><s0>001D02A02</s0>
</fC02><fC03 i1="01" i2="X" l="FRE"><s0>Informatique théorique</s0>
<s5>01</s5>
</fC03><fC03 i1="01" i2="X" l="ENG"><s0>Computer theory</s0>
<s5>01</s5>
</fC03><fC03 i1="01" i2="X" l="SPA"><s0>Informática teórica</s0>
<s5>01</s5>
</fC03><fC03 i1="02" i2="X" l="FRE"><s0>Théorie langage</s0>
<s5>02</s5>
</fC03><fC03 i1="02" i2="X" l="ENG"><s0>Language theory</s0>
<s5>02</s5>
</fC03><fC03 i1="02" i2="X" l="SPA"><s0>Teoría lenguaje</s0>
<s5>02</s5>
</fC03><fC03 i1="03" i2="X" l="FRE"><s0>Sémantique opérationnelle</s0>
<s5>03</s5>
</fC03><fC03 i1="03" i2="X" l="ENG"><s0>Operational semantics</s0>
<s5>03</s5>
</fC03><fC03 i1="03" i2="X" l="SPA"><s0>Semantica operacional</s0>
<s5>03</s5>
</fC03><fN21><s1>237</s1>
</fN21><pR><fA30 i1="01" i2="1" l="ENG"><s1>International conference on vector and parallel processing</s1>
<s2>2</s2>
<s3>Porto PRT</s3>
<s4>1996-09-25</s4>
</fA30><server><NO>PASCAL 97-0390438 INIST</NO>
<ET>Specification and proof in membership equational logic</ET>
<AU>BOUHOULA (A.); JOUANNAUD (J.-P.); MESEGUER (J.); BIDOIT (Michel); DAUCHET (Max)</AU>
<AF>SRI International, Computer Science Laboratory, n 333 Ravenswood Avenue/Menlo Park, California 94025/Etats-Unis (1 aut., 2 aut., 3 aut.); INRIA Lorraine and CRIN, 615 rue du Jardin Botanique, B.P. 101/54602 Villers-lès-Nancy/France (1 aut.); LRI, CNRS and Université de Paris-Sud, Bât 405/91405 Orsay/France (2 aut.)</AF>
<DT>Publication en série; Congrès; Niveau analytique</DT>
<SO>Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 1997; Vol. 1214; Pp. 67-92; Bibl. 25 ref.</SO>
<LA>Anglais</LA>
<EA>This paper is part of a long-term effort to increase expressiveness of algebraic specification languages while at the same time having a simple semantic basis on which efficient execution by rewriting and powerful theorem-proving tools can be based. In particular, our rewriting techniques provide semantic foundations for Maude's functional sublanguage, where they have been efficiently implemented. Membership equational logic is quite simple, and yet quite powerful. Its atomic formulae are equations and sort membership assertions, and its sentences are Horn clauses. It extends in a conservative way both order-sorted equational logic and partial algebra approaches, while Horn logic can be very easily encoded. After introducing the basic concepts of the logic, we give conditions and proof rules with which efficient equational deduction by rewriting can be achieved. We also give completion techniques to transform a specification into one meeting these conditions. We address the important issue of proving sufficient completeness of a specification. Using tree-automata techniques, we develop a test set based approach for proving inductive theorems about a specification Narrowing and proof techniques for parameterized specifications are investigated as well. Finally, we discuss the generality of our approach and how it extends several previous approaches.</EA>
<CC>001D02A02</CC>
<FD>Informatique théorique; Théorie langage; Sémantique opérationnelle</FD>
<ED>Computer theory; Language theory; Operational semantics</ED>
<SD>Informática teórica; Teoría lenguaje; Semantica operacional</SD>
<LO>INIST-16343.354000062523660080</LO>
<ID>97-0390438</ID>
</server>
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 000C52 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000C52 | 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:97-0390438
|texte= Specification and proof in membership equational logic
}}
| 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 |  |
