Implémentation d'un prouveur de théorèmes inductifs dans le système REVE
Identifieur interne : 00E899 ( Main/Exploration ); précédent : 00E898; suivant : 00E900Implémentation d'un prouveur de théorèmes inductifs dans le système REVE
Auteurs : A. LazrekSource :
English descriptors
- KwdEn :
Abstract
Le but de ce travail est l'étude et l'implémentation de deux outils. Le premier outil est pour tester la validité (ou non) d'une équation dans l'algèbre initiale d'une spécification. Dans cette spécification on n'interdit pas les relations entre les constructeurs\, ; par contre on suppose que la spécification de base est inductivement complète. Le second outil est pour tester la complétude de définition d'une spécification en permettant des relations entre les constructeurs.
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: 000209
- to stream Crin, to step Curation: 000209
- to stream Crin, to step Checkpoint: 004313
- to stream Main, to step Merge: 00F188
- to stream Main, to step Curation: 00E899
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="fr" wicri:score="-225">Implémentation d'un prouveur de théorèmes inductifs dans le système REVE</title></titleStmt><publicationStmt><idno type="RBID">CRIN:lazrek85a</idno><date when="1985" year="1985">1985</date><idno type="wicri:Area/Crin/Corpus">000209</idno><idno type="wicri:Area/Crin/Curation">000209</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">000209</idno><idno type="wicri:Area/Crin/Checkpoint">004313</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">004313</idno><idno type="wicri:Area/Main/Merge">00F188</idno><idno type="wicri:Area/Main/Curation">00E899</idno><idno type="wicri:Area/Main/Exploration">00E899</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="fr">Implémentation d'un prouveur de théorèmes inductifs dans le système REVE</title><author><name sortKey="Lazrek, A" sort="Lazrek, A" uniqKey="Lazrek A" first="A." last="Lazrek">A. Lazrek</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>theorem proving</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="fr" wicri:score="-136">Le but de ce travail est l'étude et l'implémentation de deux outils. Le premier outil est pour tester la validité (ou non) d'une équation dans l'algèbre initiale d'une spécification. Dans cette spécification on n'interdit pas les relations entre les constructeurs\, ; par contre on suppose que la spécification de base est inductivement complète. Le second outil est pour tester la complétude de définition d'une spécification en permettant des relations entre les constructeurs.</div></front></TEI><affiliations><list></list><tree><noCountry><name sortKey="Lazrek, A" sort="Lazrek, A" uniqKey="Lazrek A" first="A." last="Lazrek">A. Lazrek</name></noCountry></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 00E899 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 00E899 | 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é= CRIN:lazrek85a
|texte= Implémentation d'un prouveur de théorèmes inductifs dans le système REVE
}}
| This area was generated with Dilib version V0.6.33. |  |