Ordered Resolution with Selection for H(@)
Identifieur interne : 006080 ( Main/Exploration ); précédent : 006079; suivant : 006081Ordered Resolution with Selection for H(@)
Auteurs : Carlos Areces ; Daniel GorinSource :
Abstract
The hybrid logic H(@) is obtained by adding nominals and the satisfaction operator @ to the basic modal logic. The resulting logic gains expressive power without increasing the complexity of the satisfi- ability problem, which remains within PSpace. A resolution calculus for H(@) was introduced in [5], but it did not provide strategies for ordered resolution and selection functions. Additionally, the problem of termination was left open. In this paper we address both issues. We first define proper notions of admissible orderings and selection functions and prove the refutational completeness of the obtained ordered resolution calculus using a standard «candidate model» construction [10]. Next, we refine some of the nominal-handling rules and show that the resulting calculus is sound, complete and can only generate a finite number of clauses, establishing termination. Finally, the theoretical results were tested empirically by implementing the new strategies into HyLoRes [6,18], an experimental prototype for the original calculus described in [5]. Both versions of the prover were compared and we discuss some preliminary results.
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: 004152
- to stream Crin, to step Curation: 004152
- to stream Crin, to step Checkpoint: 000528
- to stream Main, to step Merge: 006303
- to stream Main, to step Curation: 006080
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="123">Ordered Resolution with Selection for H(@)</title></titleStmt><publicationStmt><idno type="RBID">CRIN:areces05b</idno><date when="2005" year="2005">2005</date><idno type="wicri:Area/Crin/Corpus">004152</idno><idno type="wicri:Area/Crin/Curation">004152</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">004152</idno><idno type="wicri:Area/Crin/Checkpoint">000528</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">000528</idno><idno type="wicri:Area/Main/Merge">006303</idno><idno type="wicri:Area/Main/Curation">006080</idno><idno type="wicri:Area/Main/Exploration">006080</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Ordered Resolution with Selection for H(@)</title><author><name sortKey="Areces, Carlos" sort="Areces, Carlos" uniqKey="Areces C" first="Carlos" last="Areces">Carlos Areces</name></author><author><name sortKey="Gorin, Daniel" sort="Gorin, Daniel" uniqKey="Gorin D" first="Daniel" last="Gorin">Daniel Gorin</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en" wicri:score="3139">The hybrid logic H(@) is obtained by adding nominals and the satisfaction operator @ to the basic modal logic. The resulting logic gains expressive power without increasing the complexity of the satisfi- ability problem, which remains within PSpace. A resolution calculus for H(@) was introduced in [5], but it did not provide strategies for ordered resolution and selection functions. Additionally, the problem of termination was left open. In this paper we address both issues. We first define proper notions of admissible orderings and selection functions and prove the refutational completeness of the obtained ordered resolution calculus using a standard «candidate model» construction [10]. Next, we refine some of the nominal-handling rules and show that the resulting calculus is sound, complete and can only generate a finite number of clauses, establishing termination. Finally, the theoretical results were tested empirically by implementing the new strategies into HyLoRes [6,18], an experimental prototype for the original calculus described in [5]. Both versions of the prover were compared and we discuss some preliminary results.</div></front></TEI><affiliations><list></list><tree><noCountry><name sortKey="Areces, Carlos" sort="Areces, Carlos" uniqKey="Areces C" first="Carlos" last="Areces">Carlos Areces</name><name sortKey="Gorin, Daniel" sort="Gorin, Daniel" uniqKey="Gorin D" first="Daniel" last="Gorin">Daniel Gorin</name></noCountry></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 006080 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 006080 | 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é= CRIN:areces05b
|texte= Ordered Resolution with Selection for H(@)
}}
| This area was generated with Dilib version V0.6.33. |  |