Combining proof-search and linear counter-model construction
Identifieur interne : 003943 ( Crin/Corpus ); précédent : 003942; suivant : 003944Combining proof-search and linear counter-model construction
Auteurs : Dominique Larchey-WendlingSource :
English descriptors
- KwdEn :
Abstract
In this talk, we present a proof-search algorithm that integrates a counter-model generation method based on the computation of semantic fixpoints. It is dedicated to Gödel-Dummett Logic, that is a so-called intermediate logic with linear Kripke models, but we aim to apply similar techniques, based on combination of proof and countermodel searchs, to other ressources logics. Reference counting techniques are central for an efficient implementation of those fixpoint computations.
Links to Exploration step
CRIN:larchey-wendling03aLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="393">Combining proof-search and linear counter-model construction</title></titleStmt><publicationStmt><idno type="RBID">CRIN:larchey-wendling03a</idno><date when="2003" year="2003">2003</date><idno type="wicri:Area/Crin/Corpus">003943</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Combining proof-search and linear counter-model construction</title><author><name sortKey="Larchey Wendling, Dominique" sort="Larchey Wendling, Dominique" uniqKey="Larchey Wendling D" first="Dominique" last="Larchey-Wendling">Dominique Larchey-Wendling</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>counter-models</term><term>fixpoints.</term><term>intermediate logics</term><term>proof-search</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en" wicri:score="2114">In this talk, we present a proof-search algorithm that integrates a counter-model generation method based on the computation of semantic fixpoints. It is dedicated to Gödel-Dummett Logic, that is a so-called intermediate logic with linear Kripke models, but we aim to apply similar techniques, based on combination of proof and countermodel searchs, to other ressources logics. Reference counting techniques are central for an efficient implementation of those fixpoint computations.</div></front></TEI><BibTex type="inproceedings"><ref>larchey-wendling03a</ref><crinnumber>A03-R-209</crinnumber><category>6</category><equipe>TYPES</equipe><author><e>Larchey-Wendling, Dominique</e></author><title>Combining proof-search and linear counter-model construction</title><booktitle>{First APPSEM-II Workshop 2003 - (Applied Semantics II), Nottingham, UK.}</booktitle><year>2003</year><month>Mar</month><keywords><e>intermediate logics</e><e>proof-search</e><e>counter-models</e><e>fixpoints.</e></keywords><abstract>In this talk, we present a proof-search algorithm that integrates a counter-model generation method based on the computation of semantic fixpoints. It is dedicated to Gödel-Dummett Logic, that is a so-called intermediate logic with linear Kripke models, but we aim to apply similar techniques, based on combination of proof and countermodel searchs, to other ressources logics. Reference counting techniques are central for an efficient implementation of those fixpoint computations.</abstract></BibTex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Crin/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 003943 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Crin/Corpus/biblio.hfd -nk 003943 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Crin
|étape= Corpus
|type= RBID
|clé= CRIN:larchey-wendling03a
|texte= Combining proof-search and linear counter-model construction
}}
| This area was generated with Dilib version V0.6.33. |  |