"higher-order" mathematics in B
Identifieur interne :
000882 ( PascalFrancis/Corpus );
précédent :
000881;
suivant :
000883
"higher-order" mathematics in B
Auteurs : Jean-Raymond Abriall ;
Dominique Cansell ;
Guy LaffitteSource :
-
Lecture notes in computer science [ 0302-9743 ] ; 2002.
RBID : Pascal:02-0201117
Descripteurs français
English descriptors
Abstract
In this paper, we investigate the possibility to mechanize the proof of some real complex mathematical theorems in B [1]. For this, we propose a little structure language which allows one to encode mathematical structures and their accompanying theorems. A little tool is also proposed, which translates this language into B, so that Atelier B, the tool associated with B, can be used to prove the theorems. As an illustrative example, we eventually (mechanically) prove the Theorem of Zermelo [6] stating that any set can be well-ordered. The present study constitutes a complete reshaping of an earlier (1993) unpublished work (referenced in [4]) done by two of the authors, where the classical theorems of Haussdorf and Zorn were also proved.
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 2272 |
|---|
| A08 | 01 | 1 | ENG | @1 "higher-order" mathematics in B |
|---|
| A09 | 01 | 1 | ENG | @1 ZB 2002 : formal specification and development in Z and B : Grenoble, 23-25 January 2002 |
|---|
| A11 | 01 | 1 | | @1 ABRIALL (Jean-Raymond) |
|---|
| A11 | 02 | 1 | | @1 CANSELL (Dominique) |
|---|
| A11 | 03 | 1 | | @1 LAFFITTE (Guy) |
|---|
| A12 | 01 | 1 | | @1 BERT (Didier) @9 ed. |
|---|
| A12 | 02 | 1 | | @1 BOWEN (Jonathan P.) @9 ed. |
|---|
| A12 | 03 | 1 | | @1 HENSON (Martin C.) @9 ed. |
|---|
| A12 | 04 | 1 | | @1 ROBINSON (Ken) @9 ed. |
|---|
| A14 | 01 | | | @1 LORIA @2 Metz @3 FRA @Z 2 aut. |
|---|
| A14 | 02 | | | @1 INSEE @2 Nantes @3 FRA @Z 3 aut. |
|---|
| A20 | | | | @1 370-393 |
|---|
| A21 | | | | @1 2002 |
|---|
| A23 | 01 | | | @0 ENG |
|---|
| A26 | 01 | | | @0 3-540-43166-7 |
|---|
| A43 | 01 | | | @1 INIST @2 16343 @5 354000097054510190 |
|---|
| A44 | | | | @0 0000 @1 © 2002 INIST-CNRS. All rights reserved. |
|---|
| A45 | | | | @0 8 ref. |
|---|
| A47 | 01 | 1 | | @0 02-0201117 |
|---|
| A60 | | | | @1 P @2 C |
|---|
| A61 | | | | @0 A |
|---|
| A64 | 01 | 1 | | @0 Lecture notes in computer science |
|---|
| A66 | 01 | | | @0 DEU |
|---|
| C01 | 01 | | ENG | @0 In this paper, we investigate the possibility to mechanize the proof of some real complex mathematical theorems in B [1]. For this, we propose a little structure language which allows one to encode mathematical structures and their accompanying theorems. A little tool is also proposed, which translates this language into B, so that Atelier B, the tool associated with B, can be used to prove the theorems. As an illustrative example, we eventually (mechanically) prove the Theorem of Zermelo [6] stating that any set can be well-ordered. The present study constitutes a complete reshaping of an earlier (1993) unpublished work (referenced in [4]) done by two of the authors, where the classical theorems of Haussdorf and Zorn were also proved. |
|---|
| C02 | 01 | X | | @0 001D02A05 |
|---|
| C03 | 01 | X | FRE | @0 Spécification formelle @5 04 |
|---|
| C03 | 01 | X | ENG | @0 Formal specification @5 04 |
|---|
| C03 | 01 | X | SPA | @0 Especificación formal @5 04 |
|---|
| C03 | 02 | X | FRE | @0 Démonstration théorème @5 05 |
|---|
| C03 | 02 | X | ENG | @0 Theorem proving @5 05 |
|---|
| C03 | 02 | X | SPA | @0 Demostración teorema @5 05 |
|---|
| C03 | 03 | X | FRE | @0 Langage B @4 CD @5 96 |
|---|
| C03 | 03 | X | ENG | @0 B language @4 CD @5 96 |
|---|
| C03 | 04 | X | FRE | @0 Logique ordre supérieur @4 CD @5 97 |
|---|
| C03 | 04 | X | ENG | @0 Higher order logic @4 CD @5 97 |
|---|
| N21 | | | | @1 119 |
|---|
| N82 | | | | @1 PSI |
|---|
|
|---|
| pR |
| A30 | 01 | 1 | ENG | @1 International conference of B and Z users @2 2 @3 Grenoble FRA @4 2002-01-23 |
|---|
|
|---|
Format Inist (serveur)
| NO : | PASCAL 02-0201117 INIST |
|---|
| ET : | "higher-order" mathematics in B |
|---|
| AU : | ABRIALL (Jean-Raymond); CANSELL (Dominique); LAFFITTE (Guy); BERT (Didier); BOWEN (Jonathan P.); HENSON (Martin C.); ROBINSON (Ken) |
|---|
| AF : | LORIA/Metz/France (2 aut.); INSEE/Nantes/France (3 aut.) |
|---|
| DT : | Publication en série; Congrès; Niveau analytique |
|---|
| SO : | Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 2002; Vol. 2272; Pp. 370-393; Bibl. 8 ref. |
|---|
| LA : | Anglais |
|---|
| EA : | In this paper, we investigate the possibility to mechanize the proof of some real complex mathematical theorems in B [1]. For this, we propose a little structure language which allows one to encode mathematical structures and their accompanying theorems. A little tool is also proposed, which translates this language into B, so that Atelier B, the tool associated with B, can be used to prove the theorems. As an illustrative example, we eventually (mechanically) prove the Theorem of Zermelo [6] stating that any set can be well-ordered. The present study constitutes a complete reshaping of an earlier (1993) unpublished work (referenced in [4]) done by two of the authors, where the classical theorems of Haussdorf and Zorn were also proved. |
|---|
| CC : | 001D02A05 |
|---|
| FD : | Spécification formelle; Démonstration théorème; Langage B; Logique ordre supérieur |
|---|
| ED : | Formal specification; Theorem proving; B language; Higher order logic |
|---|
| SD : | Especificación formal; Demostración teorema |
|---|
| LO : | INIST-16343.354000097054510190 |
|---|
| ID : | 02-0201117 |
|---|
Links to Exploration step
Pascal:02-0201117
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">"higher-order" mathematics in B</title>
<author><name sortKey="Abriall, Jean Raymond" sort="Abriall, Jean Raymond" uniqKey="Abriall J" first="Jean-Raymond" last="Abriall">Jean-Raymond Abriall</name>
</author><author><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA</s1>
<s2>Metz</s2>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</inist:fA14><author><name sortKey="Laffitte, Guy" sort="Laffitte, Guy" uniqKey="Laffitte G" first="Guy" last="Laffitte">Guy Laffitte</name>
<affiliation><inist:fA14 i1="02"><s1>INSEE</s1>
<s2>Nantes</s2>
<s3>FRA</s3>
<sZ>3 aut.</sZ>
</inist:fA14><publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">02-0201117</idno>
<date when="2002">2002</date>
<idno type="stanalyst">PASCAL 02-0201117 INIST</idno>
<idno type="RBID">Pascal:02-0201117</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000882</idno>
</publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">"higher-order" mathematics in B</title>
<author><name sortKey="Abriall, Jean Raymond" sort="Abriall, Jean Raymond" uniqKey="Abriall J" first="Jean-Raymond" last="Abriall">Jean-Raymond Abriall</name>
</author><author><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA</s1>
<s2>Metz</s2>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</inist:fA14><author><name sortKey="Laffitte, Guy" sort="Laffitte, Guy" uniqKey="Laffitte G" first="Guy" last="Laffitte">Guy Laffitte</name>
<affiliation><inist:fA14 i1="02"><s1>INSEE</s1>
<s2>Nantes</s2>
<s3>FRA</s3>
<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="2002">2002</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>B language</term>
<term>Formal specification</term>
<term>Higher order logic</term>
<term>Theorem proving</term>
</keywords><keywords scheme="Pascal" xml:lang="fr"><term>Spécification formelle</term>
<term>Démonstration théorème</term>
<term>Langage B</term>
<term>Logique ordre supérieur</term>
</keywords><front><div type="abstract" xml:lang="en">In this paper, we investigate the possibility to mechanize the proof of some real complex mathematical theorems in B [1]. For this, we propose a little structure language which allows one to encode mathematical structures and their accompanying theorems. A little tool is also proposed, which translates this language into B, so that Atelier B, the tool associated with B, can be used to prove the theorems. As an illustrative example, we eventually (mechanically) prove the Theorem of Zermelo [6] stating that any set can be well-ordered. The present study constitutes a complete reshaping of an earlier (1993) unpublished work (referenced in [4]) done by two of the authors, where the classical theorems of Haussdorf and Zorn were also proved.</div>
</front><inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0302-9743</s0>
</fA01><fA05><s2>2272</s2>
</fA05><fA08 i1="01" i2="1" l="ENG"><s1>"higher-order" mathematics in B</s1>
</fA08><fA09 i1="01" i2="1" l="ENG"><s1>ZB 2002 : formal specification and development in Z and B : Grenoble, 23-25 January 2002</s1>
</fA09><fA11 i1="01" i2="1"><s1>ABRIALL (Jean-Raymond)</s1>
</fA11><fA11 i1="02" i2="1"><s1>CANSELL (Dominique)</s1>
</fA11><fA11 i1="03" i2="1"><s1>LAFFITTE (Guy)</s1>
</fA11><fA12 i1="01" i2="1"><s1>BERT (Didier)</s1>
<s9>ed.</s9>
</fA12><fA12 i1="02" i2="1"><s1>BOWEN (Jonathan P.)</s1>
<s9>ed.</s9>
</fA12><fA12 i1="03" i2="1"><s1>HENSON (Martin C.)</s1>
<s9>ed.</s9>
</fA12><fA12 i1="04" i2="1"><s1>ROBINSON (Ken)</s1>
<s9>ed.</s9>
</fA12><fA14 i1="01"><s1>LORIA</s1>
<s2>Metz</s2>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</fA14><fA14 i1="02"><s1>INSEE</s1>
<s2>Nantes</s2>
<s3>FRA</s3>
<sZ>3 aut.</sZ>
</fA14><fA20><s1>370-393</s1>
</fA20><fA21><s1>2002</s1>
</fA21><fA23 i1="01"><s0>ENG</s0>
</fA23><fA26 i1="01"><s0>3-540-43166-7</s0>
</fA26><fA43 i1="01"><s1>INIST</s1>
<s2>16343</s2>
<s5>354000097054510190</s5>
</fA43><fA44><s0>0000</s0>
<s1>© 2002 INIST-CNRS. All rights reserved.</s1>
</fA44><fA45><s0>8 ref.</s0>
</fA45><fA47 i1="01" i2="1"><s0>02-0201117</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><fC01 i1="01" l="ENG"><s0>In this paper, we investigate the possibility to mechanize the proof of some real complex mathematical theorems in B [1]. For this, we propose a little structure language which allows one to encode mathematical structures and their accompanying theorems. A little tool is also proposed, which translates this language into B, so that Atelier B, the tool associated with B, can be used to prove the theorems. As an illustrative example, we eventually (mechanically) prove the Theorem of Zermelo [6] stating that any set can be well-ordered. The present study constitutes a complete reshaping of an earlier (1993) unpublished work (referenced in [4]) done by two of the authors, where the classical theorems of Haussdorf and Zorn were also proved.</s0>
</fC01><fC02 i1="01" i2="X"><s0>001D02A05</s0>
</fC02><fC03 i1="01" i2="X" l="FRE"><s0>Spécification formelle</s0>
<s5>04</s5>
</fC03><fC03 i1="01" i2="X" l="ENG"><s0>Formal specification</s0>
<s5>04</s5>
</fC03><fC03 i1="01" i2="X" l="SPA"><s0>Especificación formal</s0>
<s5>04</s5>
</fC03><fC03 i1="02" i2="X" l="FRE"><s0>Démonstration théorème</s0>
<s5>05</s5>
</fC03><fC03 i1="02" i2="X" l="ENG"><s0>Theorem proving</s0>
<s5>05</s5>
</fC03><fC03 i1="02" i2="X" l="SPA"><s0>Demostración teorema</s0>
<s5>05</s5>
</fC03><fC03 i1="03" i2="X" l="FRE"><s0>Langage B</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03><fC03 i1="03" i2="X" l="ENG"><s0>B language</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03><fC03 i1="04" i2="X" l="FRE"><s0>Logique ordre supérieur</s0>
<s4>CD</s4>
<s5>97</s5>
</fC03><fC03 i1="04" i2="X" l="ENG"><s0>Higher order logic</s0>
<s4>CD</s4>
<s5>97</s5>
</fC03><fN21><s1>119</s1>
</fN21><fN82><s1>PSI</s1>
</fN82><pR><fA30 i1="01" i2="1" l="ENG"><s1>International conference of B and Z users</s1>
<s2>2</s2>
<s3>Grenoble FRA</s3>
<s4>2002-01-23</s4>
</fA30><server><NO>PASCAL 02-0201117 INIST</NO>
<ET>"higher-order" mathematics in B</ET>
<AU>ABRIALL (Jean-Raymond); CANSELL (Dominique); LAFFITTE (Guy); BERT (Didier); BOWEN (Jonathan P.); HENSON (Martin C.); ROBINSON (Ken)</AU>
<AF>LORIA/Metz/France (2 aut.); INSEE/Nantes/France (3 aut.)</AF>
<DT>Publication en série; Congrès; Niveau analytique</DT>
<SO>Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 2002; Vol. 2272; Pp. 370-393; Bibl. 8 ref.</SO>
<LA>Anglais</LA>
<EA>In this paper, we investigate the possibility to mechanize the proof of some real complex mathematical theorems in B [1]. For this, we propose a little structure language which allows one to encode mathematical structures and their accompanying theorems. A little tool is also proposed, which translates this language into B, so that Atelier B, the tool associated with B, can be used to prove the theorems. As an illustrative example, we eventually (mechanically) prove the Theorem of Zermelo [6] stating that any set can be well-ordered. The present study constitutes a complete reshaping of an earlier (1993) unpublished work (referenced in [4]) done by two of the authors, where the classical theorems of Haussdorf and Zorn were also proved.</EA>
<CC>001D02A05</CC>
<FD>Spécification formelle; Démonstration théorème; Langage B; Logique ordre supérieur</FD>
<ED>Formal specification; Theorem proving; B language; Higher order logic</ED>
<SD>Especificación formal; Demostración teorema</SD>
<LO>INIST-16343.354000097054510190</LO>
<ID>02-0201117</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 000882 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000882 | 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:02-0201117
|texte= "higher-order" mathematics in B
}}
| 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 |  |
