Przejdź do sekcji głównej Przejdź do głównego menu Przejdź do stopki
  • Zarejestruj
  • Zaloguj
  • Język
    • English
    • Język Polski
  • Menu
  • Strona domowa
  • Aktualny numer
  • Archiwum
  • Prace online
  • O czasopiśmie
    • O czasopiśmie
    • Przesyłanie tekstów
    • Zespół redakcyjny
    • Rada redakcyjna
    • Proces recenzji
    • Komitet Logic and Logical Philosophy
    • Polityka Open Access
    • Polityka prywatności
    • Kontakt
  • Zarejestruj
  • Zaloguj
  • Język:
  • English
  • Język Polski

Logic and Logical Philosophy

Decision procedures for some strong hybrid logics
  • Strona domowa
  • /
  • Decision procedures for some strong hybrid logics
  1. Strona domowa /
  2. Archiwum /
  3. Tom 22 Nr 4 (2013): December /
  4. Artykuły

Decision procedures for some strong hybrid logics

Autor

  • Andrzej Indrzejczak Department of Logic, Nicolaus Copernicus University
  • Michał Zawidzki University of Lódź

DOI:

https://doi.org/10.12775/LLP.2013.022

Słowa kluczowe

hybrid logics, modal logics, tableau calculi, sequent calculi, decision procedures, automated reasoning

Abstrakt

Hybrid logics are extensions of standard modal logics, which significantly increase the expressive power of the latter. Since most of hybrid logics are known to be decidable, decision procedures for them is a widely investigated field of research. So far, several tableau calculi for hybrid logics have been presented in the literature. In this paper we introduce a sound, complete and terminating tableau calculus TH(@,E,D,♦ −) for hybrid logics with the satisfaction operators, the universal modality, the difference modality and the inverse modality as well as the corresponding sequent calculus SH(@,E,D,♦ −). They not only uniformly cover relatively wide range of various hybrid logics but they are also conceptually simple and enable effective search for a minimal model for a satisfiable formula. The main novelty is the exploitation of the unrestricted blocking mechanism introduced as an explicit, sound tableau rule.

Biogramy autorów

Andrzej Indrzejczak - Department of Logic, Nicolaus Copernicus University

Department of Logic and Methodology of Sciences

Michał Zawidzki - University of Lódź

Department of Logic and Methodology of Sciences

Bibliografia

D’Agostino, M., “Tableau methods for Classical Propositional Logic”, pages 45–123 in: M. D’Agostino et al (eds.), Handbook of Tableau Methods, Kluwer Academic Publishers, Dordrecht, 1999. DOI: 10.1007/978-94-017-1754-0_2

Areces, C., P. Blackburn, and M. Marx, “A road-map on complexity for hybrid logics”, pages 307–321 in: Proc. of the 8th Annual Conference of the European Association for Computer Science Logic (CSL 1999), Madrid, Spain. DOI: 10.1007/3-540-48168-0_22

Blackburn, P., “Internalizing labelled deduction”, J. Log. Comput., 10 (2000), 1: 137–168. DOI: 10.1093/logcom/10.1.137

Blackburn, P., and T. Bolander, “Termination for Hybrid Tableaus”, J. Log. Comput. 17 (2007), 3: 517–554.

Blackburn, P., Y. Venema, and M. de Rijke, Modal Logics, Cambridge University Press, 2002.

Bolander T., and T. Braüner, “Tableau-based decision procedures for hybrid logic”, J. Log. Comput., 16 (2006): 737–763. DOI: 10.1093/logcom/exl008

Braüner, T., Hybrid Logic and its Proof-Theory, Springer, 2011.

Cerrito S., and M. Cialdea-Mayer, “An efficient approach to nominal equalities in hybrid logic tableaux”, JANCL, 20 (2010), 1–2: 39–61. DOI: 10.3166/jancl.20.39-61

Cerrito S., and M. Cialdea-Mayer, “Nominal substitution at work with the global and converse modalities”, pages 59–76 in: AiML 2010, College Publications, 2010.

Demri, S., “A simple tableau system for the logic of elsewhere”, pages 177–192 in TABLEAUX-6, LNAI, Springer, 1996. DOI: 10.1007/3-540-61208-4_12

Fitting, M., “Modal proof theory”, pages pp. 85–138 in: P. Blackburn et al (eds.), Handbook of Modal Logic, Elsevier B.V., 2007. DOI: 10.1016/S1570-2464(07)80005-X

Götzmann, D., M. Kaminski, and G. Smolka, “Spartacus: A tableau prover for hybrid logic”, Electron. Notes Ther. Comput. Sci., 262 (2010): 127–139. DOI: 10.1016/j.entcs.2010.04.010

Hoffmann, G., “Lightweight hybrid tableaux”, J. of Applied Logic, 8 (2010): 397–408. DOI: 10.1016/j.jal.2010.08.003

Kaminski, M., and G. Smolka, “Terminating tableau systems for hybrid logic with difference and converse”, J. Log. Lang. Inf., 18 (2009): 437–464. DOI: 10.1007/s10849-009-9087-8

Cialdea-Mayer, M., and S. Cerrito, “Herod and pilate: two tableau provers for basic hybrid logic. System Description”, pages 255–262in IJCAR 2010, LNCS, Springer, 2010. DOI: 10.1007/978-3-642-14203-1_22

Mundhenk, M., and T. Schneider, “Undecidability of multi-modal hybrid logics”, Electron. Notes Ther. Comput. Sci., 174 (2007): 29–43. DOI: 10.1016/j.entcs.2006.11.024

Myers, R.S.R., and D. Pattinson, “Hybrid logic with the difference modality for generalizations of graphs”, J. of Applied Logic, 8 (2010): 441–458. DOI: 10.1016/j.jal.2010.08.011

Negri S., and J. von Plato, Structural Proof Theory, Cambridge, 2001.

Schmidt, R.A., and D. Tishkovsky, “Automated synthesis of tableau calculi”, Log. Meth. Comput. Sci., 7 (2011), 2: 1–32. DOI: 10.2168/LMCS-7(2:6)2011

Schmidt R.A., and D. Tishkovsky, “Using tableau to decide description logics with full role negation and identity”, 2012. PDF

Tzakova, M., “Tableau calculi for hybrid logics”, LNCS, 1617 (1999): 278–292. DOI: 10.1007/3-540-48754-9_24

Logic and Logical Philosophy

Pobrania

  • PDF (English)

Opublikowane

29.08.2013

Jak cytować

1.
INDRZEJCZAK, Andrzej & ZAWIDZKI, Michał. Decision procedures for some strong hybrid logics. Logic and Logical Philosophy [online]. 29 sierpień 2013, T. 22, nr 4, s. 389–409. [udostępniono 4.7.2025]. DOI 10.12775/LLP.2013.022.
  • PN-ISO 690 (Polski)
  • ACM
  • ACS
  • APA
  • ABNT
  • Chicago
  • Harvard
  • IEEE
  • MLA
  • Turabian
  • Vancouver
Pobierz cytowania
  • Endnote/Zotero/Mendeley (RIS)
  • BibTeX

Numer

Tom 22 Nr 4 (2013): December

Dział

Artykuły

Statystyki

Liczba wyświetleń i pobrań: 722
Liczba cytowań: 2

Crossref
Scopus
Google Scholar
Europe PMC

Wyszukiwanie

Wyszukiwanie

Przeglądaj

  • Indeks autorów
  • Lista archiwalnych numerów

Użytkownik

Użytkownik

Aktualny numer

  • Logo Atom
  • Logo RSS2
  • Logo RSS1

Informacje

  • dla czytelników
  • dla autorów
  • dla bibliotekarzy

Newsletter

Zapisz się Wypisz się

Język / Language

  • English
  • Język Polski

Tagi

Szukaj przy pomocy tagu:

hybrid logics, modal logics, tableau calculi, sequent calculi, decision procedures, automated reasoning
W górę

Akademicka Platforma Czasopism

Najlepsze czasopisma naukowe i akademickie w jednym miejscu

apcz.umk.pl

Partnerzy platformy czasopism

  • Akademia Ignatianum w Krakowie
  • Akademickie Towarzystwo Andragogiczne
  • Fundacja Copernicus na rzecz Rozwoju Badań Naukowych
  • Instytut Historii im. Tadeusza Manteuffla Polskiej Akademii Nauk
  • Instytut Kultur Śródziemnomorskich i Orientalnych PAN
  • Instytut Tomistyczny
  • Karmelitański Instytut Duchowości w Krakowie
  • Ministerstwo Kultury i Dziedzictwa Narodowego
  • Państwowa Akademia Nauk Stosowanych w Krośnie
  • Państwowa Akademia Nauk Stosowanych we Włocławku
  • Państwowa Wyższa Szkoła Zawodowa im. Stanisława Pigonia w Krośnie
  • Polska Fundacja Przemysłu Kosmicznego
  • Polskie Towarzystwo Ekonomiczne
  • Polskie Towarzystwo Ludoznawcze
  • Towarzystwo Miłośników Torunia
  • Towarzystwo Naukowe w Toruniu
  • Uniwersytet im. Adama Mickiewicza w Poznaniu
  • Uniwersytet Komisji Edukacji Narodowej w Krakowie
  • Uniwersytet Mikołaja Kopernika
  • Uniwersytet w Białymstoku
  • Uniwersytet Warszawski
  • Wojewódzka Biblioteka Publiczna - Książnica Kopernikańska
  • Wyższe Seminarium Duchowne w Pelplinie / Wydawnictwo Diecezjalne „Bernardinum" w Pelplinie

© 2021- Uniwersytet Mikołaja Kopernika w Toruniu Deklaracja dostępności Sklep wydawnictwa