28586 articles – 22070 references  [version française]

inria-00519035, version 1

## Resolution with Order and Selection for Hybrid Logics

Carlos Areces () 1, Daniel Gorin 1

Journal of Automated Reasoning 46, 1 (2010) 1-42

• 1:  TALARIS (INRIA Nancy - Grand Est / LORIA)

• CNRS : UMR7503 – INRIA – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL) France

### Bibliographic reference

• Type of document: Articles in peer-reviewed journal
• Domain: Computer Science/Logic in Computer Science
• Title: Resolution with Order and Selection for Hybrid Logics
• Abstract: We investigate labeled resolution calculi for hybrid logics with inference rules restricted via selection functions and orders. We start by providing a sound and refutationally complete calculus for the hybrid logic $\mathcal{H}(@,{\downarrow},\mathsf{A})$, even under restrictions by selection functions and orders. Then, by imposing further restrictions in the original calculus, we develop a sound, complete and terminating calculus for the $\mathcal{H}(@)$ sublanguage. The proof scheme we use to show refutational completeness of these calculi is an adaptation of a standard completeness proof for saturation-based calculi for first-order logic that guarantees completeness even under redundancy elimination. In fact, one of the contributions of this article is to show that the general framework of saturation-based proving for first-order logic with equality can be naturally adapted to saturation-based calculi for other languages, in particular modal and hybrid logics.
• Full text language: English
• Journal title:  Journal of Automated Reasoning Publisher Springer Verlag (Germany) ISSN 0168-7433 (eISSN : 1573-0670)
• Publication date: 2010-02-01
• Audience: international
• Commercial editor: Springer
• Volume: 46
• Number: 1
• Pagination: 1-42
• DOI: 10.1007/s10817-010-9167-0
• Keywords: Modal logic - Resolution calculus - Order and selection function constraints - Soundness and completeness - Termination

• inria-00519035, version 1
• oai:hal.inria.fr:inria-00519035
• From:
• Submitted on: Friday, 17 September 2010 20:32:32
• Updated on: Wednesday, 22 June 2011 11:38:06