Automatisation de l'application de l'hypothèse de récurrence dans la preuve des formules implicatives
Identifieur interne : 005A00 ( Main/Exploration ); précédent : 005999; suivant : 005A01Automatisation de l'application de l'hypothèse de récurrence dans la preuve des formules implicatives
Auteurs : Inès Mouakher [Tunisie] ; Francis Alexandre [France] ; Khaled Bsaïes [Tunisie]Source :
Abstract
L'objectif général de ce travail est de prouver les propriétés des programmes logiques (ensemble de clauses de Horn). Ces propriétés sont des formules de la forme A <-- B où A et B sont des conjonctions d'atomes. Nous disposons d'un ensemble de règles de déductions tels que le pliage, le dépliage et la simplification. La preuve consiste à appliquer l'une de ces règles sur la formule à prouver jusqu'à aboutir à un ensemble de formules triviales. Une étape essentielle dans le processus de la preuve est la réussite du pliage qui peut être vue comme l'application d'une hypothèse de récurrence dans une preuve inductive. Nous proposons des stratégies pour automatiser partiellement le processus de preuve en nous basant sur une analyse statique des formules et des programmes.
Url:
Affiliations:
- France, Tunisie
- Grand Est, Lorraine (région)
- Nancy
- Institut national polytechnique de Lorraine, Université Nancy 2, Université de Lorraine
Links toward previous steps (curation, corpus...)
- to stream Hal, to step Corpus: 005756
- to stream Hal, to step Curation: 005756
- to stream Hal, to step Checkpoint: 004634
- to stream Main, to step Merge: 005C44
- to stream Main, to step Curation: 005A00
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="fr">Automatisation de l'application de l'hypothèse de récurrence dans la preuve des formules implicatives</title><author><name sortKey="Mouakher, Ines" sort="Mouakher, Ines" uniqKey="Mouakher I" first="Inès" last="Mouakher">Inès Mouakher</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-6266" status="INCOMING"><orgName>Faculté des Sciences de Tunis</orgName><orgName type="acronym">FST</orgName><desc><address><country key="TN"></country></address></desc><listRelation><relation active="#struct-300651" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-300651" type="direct"><org type="institution" xml:id="struct-300651" status="VALID"><orgName>Faculté des Sciences de Tunis [Tunis]</orgName><desc><address><country key="TN"></country></address><ref type="url">http://www.fst.rnu.tn/fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>Tunisie</country></affiliation></author><author><name sortKey="Alexandre, Francis" sort="Alexandre, Francis" uniqKey="Alexandre F" first="Francis" last="Alexandre">Francis Alexandre</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-2492" status="OLD"><orgName>Development of specifications</orgName><orgName type="acronym">DEDALE</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/equipes/dedale</ref></desc><listRelation><relation active="#struct-160" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-300291" type="indirect"></relation><relation active="#struct-300292" type="indirect"></relation><relation active="#struct-300293" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-160" type="direct"><org type="laboratory" xml:id="struct-160" status="OLD"><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation name="UMR7503" active="#struct-441569" type="direct"></relation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-300291" type="direct"></relation><relation active="#struct-300292" type="direct"></relation><relation active="#struct-300293" type="direct"></relation></listRelation></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-300291" type="indirect"><org type="institution" xml:id="struct-300291" status="OLD"><orgName>Université Henri Poincaré - Nancy 1</orgName><orgName type="acronym">UHP</orgName><date type="end">2011-12-31</date><desc><address><addrLine>24-30 rue Lionnois, BP 60120, 54 003 NANCY cedex, France</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300292" type="indirect"><org type="institution" xml:id="struct-300292" status="OLD"><orgName>Université Nancy 2</orgName><date type="end">2011-12-31</date><desc><address><addrLine>91 avenue de la Libération, BP 454, 54001 Nancy cedex</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300293" type="indirect"><org type="institution" xml:id="struct-300293" status="OLD"><orgName>Institut National Polytechnique de Lorraine</orgName><orgName type="acronym">INPL</orgName><date type="end">2011-12-31</date><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université Nancy 2</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Institut national polytechnique de Lorraine</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName></affiliation></author><author><name sortKey="Bsaies, Khaled" sort="Bsaies, Khaled" uniqKey="Bsaies K" first="Khaled" last="Bsaïes">Khaled Bsaïes</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-6266" status="INCOMING"><orgName>Faculté des Sciences de Tunis</orgName><orgName type="acronym">FST</orgName><desc><address><country key="TN"></country></address></desc><listRelation><relation active="#struct-300651" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-300651" type="direct"><org type="institution" xml:id="struct-300651" status="VALID"><orgName>Faculté des Sciences de Tunis [Tunis]</orgName><desc><address><country key="TN"></country></address><ref type="url">http://www.fst.rnu.tn/fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>Tunisie</country></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:inria-00000070</idno><idno type="halId">inria-00000070</idno><idno type="halUri">https://hal.inria.fr/inria-00000070</idno><idno type="url">https://hal.inria.fr/inria-00000070</idno><date when="2005-06-08">2005-06-08</date><idno type="wicri:Area/Hal/Corpus">005756</idno><idno type="wicri:Area/Hal/Curation">005756</idno><idno type="wicri:Area/Hal/Checkpoint">004634</idno><idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">004634</idno><idno type="wicri:Area/Main/Merge">005C44</idno><idno type="wicri:Area/Main/Curation">005A00</idno><idno type="wicri:Area/Main/Exploration">005A00</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="fr">Automatisation de l'application de l'hypothèse de récurrence dans la preuve des formules implicatives</title><author><name sortKey="Mouakher, Ines" sort="Mouakher, Ines" uniqKey="Mouakher I" first="Inès" last="Mouakher">Inès Mouakher</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-6266" status="INCOMING"><orgName>Faculté des Sciences de Tunis</orgName><orgName type="acronym">FST</orgName><desc><address><country key="TN"></country></address></desc><listRelation><relation active="#struct-300651" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-300651" type="direct"><org type="institution" xml:id="struct-300651" status="VALID"><orgName>Faculté des Sciences de Tunis [Tunis]</orgName><desc><address><country key="TN"></country></address><ref type="url">http://www.fst.rnu.tn/fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>Tunisie</country></affiliation></author><author><name sortKey="Alexandre, Francis" sort="Alexandre, Francis" uniqKey="Alexandre F" first="Francis" last="Alexandre">Francis Alexandre</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-2492" status="OLD"><orgName>Development of specifications</orgName><orgName type="acronym">DEDALE</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/equipes/dedale</ref></desc><listRelation><relation active="#struct-160" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-300291" type="indirect"></relation><relation active="#struct-300292" type="indirect"></relation><relation active="#struct-300293" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-160" type="direct"><org type="laboratory" xml:id="struct-160" status="OLD"><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation name="UMR7503" active="#struct-441569" type="direct"></relation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-300291" type="direct"></relation><relation active="#struct-300292" type="direct"></relation><relation active="#struct-300293" type="direct"></relation></listRelation></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-300291" type="indirect"><org type="institution" xml:id="struct-300291" status="OLD"><orgName>Université Henri Poincaré - Nancy 1</orgName><orgName type="acronym">UHP</orgName><date type="end">2011-12-31</date><desc><address><addrLine>24-30 rue Lionnois, BP 60120, 54 003 NANCY cedex, France</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300292" type="indirect"><org type="institution" xml:id="struct-300292" status="OLD"><orgName>Université Nancy 2</orgName><date type="end">2011-12-31</date><desc><address><addrLine>91 avenue de la Libération, BP 454, 54001 Nancy cedex</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300293" type="indirect"><org type="institution" xml:id="struct-300293" status="OLD"><orgName>Institut National Polytechnique de Lorraine</orgName><orgName type="acronym">INPL</orgName><date type="end">2011-12-31</date><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université Nancy 2</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Institut national polytechnique de Lorraine</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName></affiliation></author><author><name sortKey="Bsaies, Khaled" sort="Bsaies, Khaled" uniqKey="Bsaies K" first="Khaled" last="Bsaïes">Khaled Bsaïes</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-6266" status="INCOMING"><orgName>Faculté des Sciences de Tunis</orgName><orgName type="acronym">FST</orgName><desc><address><country key="TN"></country></address></desc><listRelation><relation active="#struct-300651" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-300651" type="direct"><org type="institution" xml:id="struct-300651" status="VALID"><orgName>Faculté des Sciences de Tunis [Tunis]</orgName><desc><address><country key="TN"></country></address><ref type="url">http://www.fst.rnu.tn/fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>Tunisie</country></affiliation></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="fr">L'objectif général de ce travail est de prouver les propriétés des programmes logiques (ensemble de clauses de Horn). Ces propriétés sont des formules de la forme A <-- B où A et B sont des conjonctions d'atomes. Nous disposons d'un ensemble de règles de déductions tels que le pliage, le dépliage et la simplification. La preuve consiste à appliquer l'une de ces règles sur la formule à prouver jusqu'à aboutir à un ensemble de formules triviales. Une étape essentielle dans le processus de la preuve est la réussite du pliage qui peut être vue comme l'application d'une hypothèse de récurrence dans une preuve inductive. Nous proposons des stratégies pour automatiser partiellement le processus de preuve en nous basant sur une analyse statique des formules et des programmes.</div></front></TEI><affiliations><list><country><li>France</li><li>Tunisie</li></country><region><li>Grand Est</li><li>Lorraine (région)</li></region><settlement><li>Nancy</li></settlement><orgName><li>Institut national polytechnique de Lorraine</li><li>Université Nancy 2</li><li>Université de Lorraine</li></orgName></list><tree><country name="Tunisie"><noRegion><name sortKey="Mouakher, Ines" sort="Mouakher, Ines" uniqKey="Mouakher I" first="Inès" last="Mouakher">Inès Mouakher</name></noRegion><name sortKey="Bsaies, Khaled" sort="Bsaies, Khaled" uniqKey="Bsaies K" first="Khaled" last="Bsaïes">Khaled Bsaïes</name></country><country name="France"><region name="Grand Est"><name sortKey="Alexandre, Francis" sort="Alexandre, Francis" uniqKey="Alexandre F" first="Francis" last="Alexandre">Francis Alexandre</name></region></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 005A00 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 005A00 | 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é= Hal:inria-00000070
|texte= Automatisation de l'application de l'hypothèse de récurrence dans la preuve des formules implicatives
}}
| This area was generated with Dilib version V0.6.33. |  |