Higher-order modal logics: Automation and applications

Christoph Benzmüller; Bruno Woltzenlogel Paleo

doi:10.1007/978-3-319-21768-0_2

Higher-order modal logics: Automation and applications

Christoph Benzmüller^*, Bruno Woltzenlogel Paleo

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

14 Citations (Scopus)

Abstract

These are the lecture notes of a tutorial on higher-order modal logics held at the 11th Reasoning Web Summer School. After defining the syntax and (possible worlds) semantics of some higherorder modal logics, we show that they can be embedded into classical higher-order logic by systematically lifting the types of propositions, making them depend on a new atomic type for possible worlds. This approach allows several well-established automated and interactive reasoning tools for classical higher-order logic to be applied also to modal higherorder logic problems. Moreover, also meta reasoning about the embedded modal logics becomes possible. Finally, we illustrate how our approach can be useful for reasoning with web logics and expressive ontologies, and we also sketch a possible solution for handling inconsistent data.

Original language	English
Title of host publication	Reasoning Web
Subtitle of host publication	Web Logic Rules - 11th International Summer School 2015, Tutorial Lectures
Editors	Wolfgang Faber, Adrian Paschke
Publisher	Springer Verlag
Pages	32-74
Number of pages	43
ISBN (Print)	9783319217673
DOIs	https://doi.org/10.1007/978-3-319-21768-0_2
Publication status	Published - 2015
Externally published	Yes
Event	11th International Reasoning Web Summer School, RW 2015 - Berlin, Germany Duration: 31 Jul 2015 → 4 Aug 2015

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	9203
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	11th International Reasoning Web Summer School, RW 2015
Country/Territory	Germany
City	Berlin
Period	31/07/15 → 4/08/15

Access to Document

10.1007/978-3-319-21768-0_2

Cite this

Benzmüller, C., & Woltzenlogel Paleo, B. (2015). Higher-order modal logics: Automation and applications. In W. Faber, & A. Paschke (Eds.), Reasoning Web: Web Logic Rules - 11th International Summer School 2015, Tutorial Lectures (pp. 32-74). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9203). Springer Verlag. https://doi.org/10.1007/978-3-319-21768-0_2

Benzmüller, Christoph ; Woltzenlogel Paleo, Bruno. / Higher-order modal logics : Automation and applications. Reasoning Web: Web Logic Rules - 11th International Summer School 2015, Tutorial Lectures. editor / Wolfgang Faber ; Adrian Paschke. Springer Verlag, 2015. pp. 32-74 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{5b57774dc52242ff9cda4d65dda303bc,

title = "Higher-order modal logics: Automation and applications",

abstract = "These are the lecture notes of a tutorial on higher-order modal logics held at the 11th Reasoning Web Summer School. After defining the syntax and (possible worlds) semantics of some higherorder modal logics, we show that they can be embedded into classical higher-order logic by systematically lifting the types of propositions, making them depend on a new atomic type for possible worlds. This approach allows several well-established automated and interactive reasoning tools for classical higher-order logic to be applied also to modal higherorder logic problems. Moreover, also meta reasoning about the embedded modal logics becomes possible. Finally, we illustrate how our approach can be useful for reasoning with web logics and expressive ontologies, and we also sketch a possible solution for handling inconsistent data.",

author = "Christoph Benzm{\"u}ller and {Woltzenlogel Paleo}, Bruno",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2015.; 11th International Reasoning Web Summer School, RW 2015 ; Conference date: 31-07-2015 Through 04-08-2015",

year = "2015",

doi = "10.1007/978-3-319-21768-0_2",

language = "English",

isbn = "9783319217673",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "32--74",

editor = "Wolfgang Faber and Adrian Paschke",

booktitle = "Reasoning Web",

address = "Germany",

}

Benzmüller, C & Woltzenlogel Paleo, B 2015, Higher-order modal logics: Automation and applications. in W Faber & A Paschke (eds), Reasoning Web: Web Logic Rules - 11th International Summer School 2015, Tutorial Lectures. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9203, Springer Verlag, pp. 32-74, 11th International Reasoning Web Summer School, RW 2015, Berlin, Germany, 31/07/15. https://doi.org/10.1007/978-3-319-21768-0_2

Higher-order modal logics: Automation and applications. / Benzmüller, Christoph; Woltzenlogel Paleo, Bruno.
Reasoning Web: Web Logic Rules - 11th International Summer School 2015, Tutorial Lectures. ed. / Wolfgang Faber; Adrian Paschke. Springer Verlag, 2015. p. 32-74 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9203).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Higher-order modal logics

T2 - 11th International Reasoning Web Summer School, RW 2015

AU - Benzmüller, Christoph

AU - Woltzenlogel Paleo, Bruno

PY - 2015

Y1 - 2015

N2 - These are the lecture notes of a tutorial on higher-order modal logics held at the 11th Reasoning Web Summer School. After defining the syntax and (possible worlds) semantics of some higherorder modal logics, we show that they can be embedded into classical higher-order logic by systematically lifting the types of propositions, making them depend on a new atomic type for possible worlds. This approach allows several well-established automated and interactive reasoning tools for classical higher-order logic to be applied also to modal higherorder logic problems. Moreover, also meta reasoning about the embedded modal logics becomes possible. Finally, we illustrate how our approach can be useful for reasoning with web logics and expressive ontologies, and we also sketch a possible solution for handling inconsistent data.

AB - These are the lecture notes of a tutorial on higher-order modal logics held at the 11th Reasoning Web Summer School. After defining the syntax and (possible worlds) semantics of some higherorder modal logics, we show that they can be embedded into classical higher-order logic by systematically lifting the types of propositions, making them depend on a new atomic type for possible worlds. This approach allows several well-established automated and interactive reasoning tools for classical higher-order logic to be applied also to modal higherorder logic problems. Moreover, also meta reasoning about the embedded modal logics becomes possible. Finally, we illustrate how our approach can be useful for reasoning with web logics and expressive ontologies, and we also sketch a possible solution for handling inconsistent data.

UR - http://www.scopus.com/inward/record.url?scp=84950158914&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-21768-0_2

DO - 10.1007/978-3-319-21768-0_2

M3 - Conference contribution

AN - SCOPUS:84950158914

SN - 9783319217673

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 32

EP - 74

BT - Reasoning Web

A2 - Faber, Wolfgang

A2 - Paschke, Adrian

PB - Springer Verlag

Y2 - 31 July 2015 through 4 August 2015

ER -

Benzmüller C, Woltzenlogel Paleo B. Higher-order modal logics: Automation and applications. In Faber W, Paschke A, editors, Reasoning Web: Web Logic Rules - 11th International Summer School 2015, Tutorial Lectures. Springer Verlag. 2015. p. 32-74. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-21768-0_2

Higher-order modal logics: Automation and applications

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this