Curation
Istex
Racine
Curation
Checkpoint
Istex
Racine
Istex
Exploration
Accueil
Racine
Racine

Serveur d'exploration sur la recherche en informatique en Lorraine

Attention, ce site est en cours de développement !
Attention, site généré par des moyens informatiques à partir de corpus bruts.
Les informations ne sont donc pas validées.

A divergence critic

Identifieur interne : 001F84 ( Istex/Curation ); précédent : 001F83; suivant : 001F85

A divergence critic

Auteurs : Toby Walsh [France]

Source :

RBID : ISTEX:8A8060C3DE8FAA9ED00B1064CE8585169A53D22A

Abstract

Abstract: Inductive theorem provers often diverge. This paper describes a critic which monitors the construction of inductive proofs attempting to identify diverging proof attempts. The critic proposes lemmas and generalizations which hopefully allow the proof to go through without divergence. The critic enables the system SPIKE to prove many theorems completely automatically from the definitions alone.

Url:
DOI: 10.1007/3-540-58156-1_2

Links toward previous steps (curation, corpus...)

Links to Exploration step

ISTEX:8A8060C3DE8FAA9ED00B1064CE8585169A53D22A

Le document en format XML

<record>
<TEI wicri:istexFullTextTei="biblStruct">
<teiHeader>
<fileDesc>
<titleStmt>
<title xml:lang="en">A divergence critic</title>
<author>
<name sortKey="Walsh, Toby" sort="Walsh, Toby" uniqKey="Walsh T" first="Toby" last="Walsh">Toby Walsh</name>
<affiliation wicri:level="1">
<mods:affiliation>INRIA-Lorraine, 615, rue du Jardin Botanique, B.P. 101, F-54602, Villers-les-Nancy, France</mods:affiliation>
<country xml:lang="fr">France</country>
<wicri:regionArea>INRIA-Lorraine, 615, rue du Jardin Botanique, B.P. 101, F-54602, Villers-les-Nancy</wicri:regionArea>
</affiliation>
<affiliation wicri:level="1">
<mods:affiliation>E-mail: walsh@loria.fr</mods:affiliation>
<country wicri:rule="url">France</country>
</affiliation>
</author>
</titleStmt>
<publicationStmt>
<idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:8A8060C3DE8FAA9ED00B1064CE8585169A53D22A</idno>
<date when="1994" year="1994">1994</date>
<idno type="doi">10.1007/3-540-58156-1_2</idno>
<idno type="url">https://api.istex.fr/ark:/67375/HCB-MG1JT2ZG-T/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">002010</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002010</idno>
<idno type="wicri:Area/Istex/Curation">001F84</idno>
</publicationStmt>
<sourceDesc>
<biblStruct>
<analytic>
<title level="a" type="main" xml:lang="en">A divergence critic</title>
<author>
<name sortKey="Walsh, Toby" sort="Walsh, Toby" uniqKey="Walsh T" first="Toby" last="Walsh">Toby Walsh</name>
<affiliation wicri:level="1">
<mods:affiliation>INRIA-Lorraine, 615, rue du Jardin Botanique, B.P. 101, F-54602, Villers-les-Nancy, France</mods:affiliation>
<country xml:lang="fr">France</country>
<wicri:regionArea>INRIA-Lorraine, 615, rue du Jardin Botanique, B.P. 101, F-54602, Villers-les-Nancy</wicri:regionArea>
</affiliation>
<affiliation wicri:level="1">
<mods:affiliation>E-mail: walsh@loria.fr</mods:affiliation>
<country wicri:rule="url">France</country>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series>
<title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title>
<title level="s" type="abbrev">Lect Notes Comput Sci</title>
<idno type="ISSN">0302-9743</idno>
<idno type="eISSN">1611-3349</idno>
<idno type="ISSN">0302-9743</idno>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt>
<idno type="ISSN">0302-9743</idno>
</seriesStmt>
</fileDesc>
<profileDesc>
<textClass></textClass>
</profileDesc>
</teiHeader>
<front>
<div type="abstract" xml:lang="en">Abstract: Inductive theorem provers often diverge. This paper describes a critic which monitors the construction of inductive proofs attempting to identify diverging proof attempts. The critic proposes lemmas and generalizations which hopefully allow the proof to go through without divergence. The critic enables the system SPIKE to prove many theorems completely automatically from the definitions alone.</div>
</front>
</TEI>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Curation

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001F84 | SxmlIndent | more

Ou

HfdSelect -h $EXPLOR_AREA/Data/Istex/Curation/biblio.hfd -nk 001F84 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Istex
   |étape=   Curation
   |type=    RBID
   |clé=     ISTEX:8A8060C3DE8FAA9ED00B1064CE8585169A53D22A
   |texte=   A divergence critic
}}
Wicri

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