Experiments on Supporting Interactive Proof Using Resolution
Identifieur interne : 001810 ( Istex/Checkpoint ); précédent : 001809; suivant : 001811Experiments on Supporting Interactive Proof Using Resolution
Auteurs : Jia Meng [Royaume-Uni] ; Lawrence C. Paulson [Royaume-Uni]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: Interactive theorem provers can model complex systems, but require much effort to prove theorems. Resolution theorem provers are automatic and powerful, but they are designed to be used for very different applications. This paper reports a series of experiments designed to determine whether resolution can support interactive proof as it is currently done. In particular, we present a sound and practical encoding in first-order logic of Isabelle’s type classes.
Url:
DOI: 10.1007/978-3-540-25984-8_28
Affiliations:
Links toward previous steps (curation, corpus...)
Links to Exploration step
ISTEX:B8198536B2DC9C1D70C04FAB11C39115B8A95089Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Experiments on Supporting Interactive Proof Using Resolution</title>
<author><name sortKey="Meng, Jia" sort="Meng, Jia" uniqKey="Meng J" first="Jia" last="Meng">Jia Meng</name>
</author>
<author><name sortKey="Paulson, Lawrence C" sort="Paulson, Lawrence C" uniqKey="Paulson L" first="Lawrence C." last="Paulson">Lawrence C. Paulson</name>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:B8198536B2DC9C1D70C04FAB11C39115B8A95089</idno>
<date when="2004" year="2004">2004</date>
<idno type="doi">10.1007/978-3-540-25984-8_28</idno>
<idno type="url">https://api.istex.fr/ark:/67375/HCB-69137JPG-S/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">002B71</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002B71</idno>
<idno type="wicri:Area/Istex/Curation">002B34</idno>
<idno type="wicri:Area/Istex/Checkpoint">001810</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001810</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Experiments on Supporting Interactive Proof Using Resolution</title>
<author><name sortKey="Meng, Jia" sort="Meng, Jia" uniqKey="Meng J" first="Jia" last="Meng">Jia Meng</name>
<affiliation wicri:level="4"><country xml:lang="fr">Royaume-Uni</country>
<wicri:regionArea>Computer Laboratory, University of Cambridge, 15 JJ Thomson Avenue, CB3 0FD, Cambridge</wicri:regionArea>
<orgName type="university">Université de Cambridge</orgName>
<placeName><settlement type="city">Cambridge</settlement>
<region type="country">Angleterre</region>
<region type="région" nuts="1">Angleterre de l'Est</region>
</placeName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">Royaume-Uni</country>
</affiliation>
</author>
<author><name sortKey="Paulson, Lawrence C" sort="Paulson, Lawrence C" uniqKey="Paulson L" first="Lawrence C." last="Paulson">Lawrence C. Paulson</name>
<affiliation wicri:level="4"><country xml:lang="fr">Royaume-Uni</country>
<wicri:regionArea>Computer Laboratory, University of Cambridge, 15 JJ Thomson Avenue, CB3 0FD, Cambridge</wicri:regionArea>
<orgName type="university">Université de Cambridge</orgName>
<placeName><settlement type="city">Cambridge</settlement>
<region type="country">Angleterre</region>
<region type="région" nuts="1">Angleterre de l'Est</region>
</placeName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">Royaume-Uni</country>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</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: Interactive theorem provers can model complex systems, but require much effort to prove theorems. Resolution theorem provers are automatic and powerful, but they are designed to be used for very different applications. This paper reports a series of experiments designed to determine whether resolution can support interactive proof as it is currently done. In particular, we present a sound and practical encoding in first-order logic of Isabelle’s type classes.</div>
</front>
</TEI>
<affiliations><list><country><li>Royaume-Uni</li>
</country>
<region><li>Angleterre</li>
<li>Angleterre de l'Est</li>
</region>
<settlement><li>Cambridge</li>
</settlement>
<orgName><li>Université de Cambridge</li>
</orgName>
</list>
<tree><country name="Royaume-Uni"><region name="Angleterre"><name sortKey="Meng, Jia" sort="Meng, Jia" uniqKey="Meng J" first="Jia" last="Meng">Jia Meng</name>
</region>
<name sortKey="Meng, Jia" sort="Meng, Jia" uniqKey="Meng J" first="Jia" last="Meng">Jia Meng</name>
<name sortKey="Paulson, Lawrence C" sort="Paulson, Lawrence C" uniqKey="Paulson L" first="Lawrence C." last="Paulson">Lawrence C. Paulson</name>
<name sortKey="Paulson, Lawrence C" sort="Paulson, Lawrence C" uniqKey="Paulson L" first="Lawrence C." last="Paulson">Lawrence C. Paulson</name>
</country>
</tree>
</affiliations>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Checkpoint
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001810 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Checkpoint/biblio.hfd -nk 001810 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Lorraine |area= InforLorV4 |flux= Istex |étape= Checkpoint |type= RBID |clé= ISTEX:B8198536B2DC9C1D70C04FAB11C39115B8A95089 |texte= Experiments on Supporting Interactive Proof Using Resolution }}
![]() | This area was generated with Dilib version V0.6.33. | ![]() |