Preuve automatique par paramodulation, réécriture et induction
Identifieur interne : 000C58 ( Crin/Curation ); précédent : 000C57; suivant : 000C59Preuve automatique par paramodulation, réécriture et induction
Auteurs : A. BouhoulaSource :
English descriptors
Abstract
De nombreuses applications en informatique font appel aux outils de la démonstration automatique. Parmi ces applications, nous retrouvons les systèmes experts, les bases de données déductives, les spécifications algébriques et la vérification des circuits. Au cours de ce travail, nous avons implanté un algorithme de démonstration par réfutation. L'accent est mis sur le traitement de la relation d'égalité dans la logique des clauses de Horn, car en pratique ce cadre est suffisamment général pour traiter la plupart des spécifications. Nous avons utilisé des heuristiques afin d'avoir un système efficace en temps d'exécution et produisant un nombre réduit de conséquences permettant d'obtenir une contradiction. D'autre part, nous avons proposé une nouvelle méthode de preuve par induction pour une théorie conditionnelle. Cette méthode permet la simplification des conjectures entre elles, la manipulation des équations non orientables et la réfutation d'equations qui ne sont pas des théorèmes inductifs. En particulier, si les axiomes sont des règles non conditionnelles la méthode est réfutationnellement complète.
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: Pour aller vers cette notice dans l'étape Curation :000C58
Links to Exploration step
CRIN:bouhoula91aLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="fr" wicri:score="-37">Preuve automatique par paramodulation, réécriture et induction</title></titleStmt><publicationStmt><idno type="RBID">CRIN:bouhoula91a</idno><date when="1991" year="1991">1991</date><idno type="wicri:Area/Crin/Corpus">000C58</idno><idno type="wicri:Area/Crin/Curation">000C58</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">000C58</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="fr">Preuve automatique par paramodulation, réécriture et induction</title><author><name sortKey="Bouhoula, A" sort="Bouhoula, A" uniqKey="Bouhoula A" first="A." last="Bouhoula">A. Bouhoula</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>automated deduction</term><term>paramodulation</term><term>resolution</term><term>rewriting induction</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="fr" wicri:score="-504">De nombreuses applications en informatique font appel aux outils de la démonstration automatique. Parmi ces applications, nous retrouvons les systèmes experts, les bases de données déductives, les spécifications algébriques et la vérification des circuits. Au cours de ce travail, nous avons implanté un algorithme de démonstration par réfutation. L'accent est mis sur le traitement de la relation d'égalité dans la logique des clauses de Horn, car en pratique ce cadre est suffisamment général pour traiter la plupart des spécifications. Nous avons utilisé des heuristiques afin d'avoir un système efficace en temps d'exécution et produisant un nombre réduit de conséquences permettant d'obtenir une contradiction. D'autre part, nous avons proposé une nouvelle méthode de preuve par induction pour une théorie conditionnelle. Cette méthode permet la simplification des conjectures entre elles, la manipulation des équations non orientables et la réfutation d'equations qui ne sont pas des théorèmes inductifs. En particulier, si les axiomes sont des règles non conditionnelles la méthode est réfutationnellement complète.</div></front></TEI><BibTex type="techreport"><ref>bouhoula91a</ref><crinnumber>91-R-204</crinnumber><category>15</category><equipe>EURECA</equipe><author><e>Bouhoula, A.</e></author><title>Preuve automatique par paramodulation, réécriture et induction</title><institution>Centre de Recherche en Informatique de Nancy</institution><year>1991</year><type>Rapport interne</type><address>Vandoeuvre-lès-Nancy</address><keywords><e>automated deduction</e><e>resolution</e><e>paramodulation</e><e>rewriting induction</e></keywords><abstract>De nombreuses applications en informatique font appel aux outils de la démonstration automatique. Parmi ces applications, nous retrouvons les systèmes experts, les bases de données déductives, les spécifications algébriques et la vérification des circuits. Au cours de ce travail, nous avons implanté un algorithme de démonstration par réfutation. L'accent est mis sur le traitement de la relation d'égalité dans la logique des clauses de Horn, car en pratique ce cadre est suffisamment général pour traiter la plupart des spécifications. Nous avons utilisé des heuristiques afin d'avoir un système efficace en temps d'exécution et produisant un nombre réduit de conséquences permettant d'obtenir une contradiction. D'autre part, nous avons proposé une nouvelle méthode de preuve par induction pour une théorie conditionnelle. Cette méthode permet la simplification des conjectures entre elles, la manipulation des équations non orientables et la réfutation d'equations qui ne sont pas des théorèmes inductifs. En particulier, si les axiomes sont des règles non conditionnelles la méthode est réfutationnellement complète.</abstract></BibTex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Crin/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000C58 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Crin/Curation/biblio.hfd -nk 000C58 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Crin
|étape= Curation
|type= RBID
|clé= CRIN:bouhoula91a
|texte= Preuve automatique par paramodulation, réécriture et induction
}}
| This area was generated with Dilib version V0.6.33. |  |