Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
All About Fuzzy Description Logics and Applications Kapitel lesen Erstes Kapitel lesen

2015 | OriginalPaper | Buchkapitel

Higher-Order Modal Logics: Automation and Applications

verfasst von : Christoph Benzmüller, Bruno Woltzenlogel Paleo

Erschienen in: Reasoning Web. Web Logic Rules

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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 higher-order 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 higher-order 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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel All About Fuzzy Description Logics and Applications
Nächstes Kapitel Web Stream Reasoning: From Data Streams to Actionable Knowledge
Fußnoten
1
thf stands for typed higher-order form and it refers to a family of syntax formats for higher-order logic. So far only the fully developed thf0 format, for simple type theory, is in practical use.
 
2
In thf0, which is a concrete syntax for HOL, $i and $o represent the HOL base types i and o (Booleans). $i>$o encodes a function (predicate) type. Predicate application, as in A(X, W), is encoded as ((A@X)@W) or simply as (A@X@W), i.e., function/predicate application is represented by @; universal quantification and \(\lambda \)-abstraction as in https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-21768-0_2/340555_1_En_2_IEq260_HTML.gif and are represented as in ; comments begin with %.
 
3
The 3480 problems for logic S4 can be download from http://​christoph-benzmueller.​de/​papers/​THF-S4-ALL.​zip.
 
5
See file QML_var.thy at the github url from above.
 
6
The keyword indicates a lambda abstraction: (or ) denotes the function \(\lambda x:t.p\), which takes an argument x (of type t) and returns p.
 
7
The underlying proof system of Coq (the Calculus of Inductive Constructions (CIC) [57]) is actually more sophisticated and minimalistic than the calculus shown in Fig. 5. But the calculus shown here suffices for the purposes of this tutorial. This calculus is classical, because of the double negation elimination rule. Although CIC is intuitionistic, it can be made classical by importing Coq’s classical library, which adds the axiom of the excluded middle and the double negation elimination lemma.
 
8
The natural deduction calculus with the rules from Figs. 5 and 6 is sound and complete relatively to the calculus of Fig. 5 extended with a necessitation rule and the modal axiom K [67]. Starting from a sound and Henkin-complete natural deduction calculus for classical higher-order logic (cf. Fig. 5), the additional modal rules in Fig. 6 make it sound and Henkin-complete for the rigid higher-order modal logic K.
 
9
More elegantly, we could employ an \(@_{cw}\)-operator; for example, (A6) would then be encoded as \(@_{cw} (likes Mary Bill)\) (see also Sect. 5.4).
 
10
Fitting [36] (pp. 83ff) actually does not use a translation to higher-order logic, where worlds become part of the syntax. But what he does, using his style of syntax (which distinguishes extensional and intensional types), is essentially analogous to the translation described here.
 
Literatur
1.
Web semantics: Science, services and agents on the world wide web, special issue on reasoning with context in the semantic web, vol. 12–13, pp. 1–160 (2012)
2.
Adams, R.M.: Introductory Note to *1970. In: Feferman, S., et al. (eds.) Kurt Gödel, Collected Works, vol. III. Oxford University Press, New York (1995)
3.
Akman, V., Surav, M.: Steps toward formalizing context. AI Mag. 17(3), 55–72 (1996)
4.
Alama, J., Heskes, T., Kühlwein, D., Tsivtsivadze, E., Urban, J.: Premise selection for mathematics by corpus analysis and kernel methods. J. Autom. Reasoning 52(2), 191–213 (2014)MathSciNetCrossRefMATH
5.
Anderson, A.C., Gettings, M.: Gödel’s ontological proof revisited. In: Hájek, P. (ed.) Gödel ’96: Logical foundations of mathematics, computer science and physics. Lecture Notes in Logic, vol. 6, pp. 167–172. Springer, Berlin (1996)CrossRef
6.
7.
Andrews, P.B.: Church’s type theory. In: Zalta, E.N. (ed.), The Stanford Encyclopedia of Philosophy. Spring 2014 edition, 2014
8.
Andrews, P.B., Miller, D.A.: Eve Longini Cohen, and Frank Pfenning. Automating higher-order logic. In: Bledsoe, W.W., Loveland, D.W., et al., Automated Theorem Proving: After 25 Years, vol. 29 of Contemporary Mathematics series, pp. 169–192. American Mathematical Society (1984)
9.
Andrews, P.B., Bishop, M.: On sets, types, fixed points, and checkerboards. In: Miglioli, P., Moscato, U., Mundici, D., Ornaghi, D. (eds.) Theorem Proving with Analytic Tableaux and Related Methods. LNCS, vol. 1071, pp. 1–15. Springer, Heidelberg (1996)CrossRef
10.
Marcos, J.: Modality and paraconsistency. The Logica Yearbook, pp. 213–222 (2005)
11.
Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, New York (2003)MATH
12.
Benzmüller, C., Theiss, F., Paulson, L., Fietzke, A.: LEO-II - a cooperative automatic theorem prover for higher-order logic. In: Proceedings of IJCAR 2008, number 5195 in LNAI, pp. 162–170. Springer, Berlin (2008)
13.
Benzmüller, C., Woltzenlogel Paleo, B.: Formalization, Mechanization and Automation of Gödel’s Proof of God’s Existence. arXiv: 1308.​4526 (2013)
14.
Benzmüller, C.: Verifying the modal logic cube is an easy task (for higher-order automated reasoners). In: Siegler, S., Wasser, N. (eds.) Walther Festschrift. LNCS, vol. 6463, pp. 117–128. Springer, Heidelberg (2010) CrossRef
15.
Benzmüller, C., Brown, C.: The curious inference of Boolos in MIZAR and OMEGA. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof - Festschrift in Honour of Andrzej Trybulec. Studies in Logic, Grammar, and Rhetoric, vol. 10(23), pp. 299–388. The University of Bialystok, Polen (2007)
16.
Benzmüller, C., Brown, C.E., Kohlhase, M.: Higher-order semantics and extensionality. J. Symb. Logic 69(4), 1027–1088 (2004)MathSciNetCrossRefMATH
17.
Benzmüller, C., Otten, J., Raths, T.: Implementing and evaluating provers for first-order modal logics. In: Raedt, L.D., Bessiere, C., Dubois, D., Doherty, P., Frasconi, P., Heintz, F., Lucas, P. (eds.), ECAI 2012, Frontiers in Artificial Intelligence and Applications, vol. 242, pp. 163–168. IOS Press, Montpellier (2012)
18.
Benzmüller, C., Woltzenlogel Paleo, B.: Gödel’s God in Isabelle/HOL. Arch. Formal Proofs, 2013 (2013)
19.
Benzmüller, C., Woltzenlogel Paleo, B.: Automating Gödel’s ontological proof of God’s existence with higher-order automated theorem provers. In: Schaub, T., Friedrich, G., O’Sullivan, B., (eds.), ECAI 2014, Frontiers in Artificial Intelligence and Applications, vol. 263, pp. 93–98, IOS Press (2014)
20.
Benzmüller, C., Paulson, L.: Exploring properties of normal multimodal logics in simple type theory with LEO-II. In: Benzmüller, C., Brown, C., Siekmann, J., Statman, R. (eds.), Reasoning in Simple Type Theory – Festschrift in Honor of Peter B. Andrews on His 70th Birthday, Studies in Logic, Mathematical Logic and Foundations, pp. 386–406, College Publications (2008)
21.
Benzmüller, C., Paulson, L.: Quantified multimodal logics in simple type theory. Logic Univers. (Spec. Issue Multimodal Logics) 7(1), 7–20 (2013)MathSciNetCrossRefMATH
22.
Benzmüller, C., Pease, A.: Higher-order aspects and context in SUMO. J. Web Seman. (Spec. Issue Reasoning with context in the Semant. Web) 12–13, 104–117 (2012)
23.
Benzmüller, Christoph, Raths, Thomas: HOL based first-order modal logic provers. In: McMillan, Ken, Middeldorp, Aart, Voronkov, Andrei (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 127–136. Springer, Heidelberg (2013) CrossRef
24.
Benzmüller, C., Weber, L., Woltzenlogel Paleo, B.: Computer-assisted analysis of the Anderson-Hájek ontological controversy. In: Silvestre, R.S., Béziau, J.-Y. (eds.), Handbook of the 1st World Congress on Logic and Religion, Joao Pessoa, Brasil (2015)
25.
Beziau, J.Y., Carnielli, W., Gabbay, D.: Handbook of Paraconsistency. College Publications, London (2007)MATH
26.
Blackburn, P., van Benthem, J.F.A.K., Wolter, F.: Handbook of Modal Logic, Volume 3 (Studies in Logic and Practical Reasoning). Elsevier Science Inc., New York (2006)
27.
Blanchette, J.C., Böhme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. J. Autom. Reasoning 51(1), 109–128 (2013)MathSciNetCrossRefMATH
28.
Blanchette, Jasmin Christian, Nipkow, Tobias: Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, Matt, Paulson, Lawrence C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131–146. Springer, Heidelberg (2010) CrossRef
29.
30.
Brown, C.E.: Satallax: An automated higher-order prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) Automated Reasoning. LNCS, vol. 7364, pp. 111–117. Springer, Heidelberg (2012) CrossRef
31.
Bucav, S., Buvac, V., Mason, I.A.: Metamathematics of contexts. Fundamenta Informaticae 23(3), 263–301 (1995)MathSciNetMATH
32.
33.
34.
35.
Dunn, J.M., Restall, G.: Relevance logic. Handbook of Philosophical Logic 6, 1–136 (2002)CrossRef
36.
Fitting, M.: Types, Tableaux and Gödel’s God, Kluwer (2002)
37.
Fitting, M., Mendelsohn, R.L.: First-Order Modal Logic. Synthese Library. Kluwer, Netherlands (1998) CrossRefMATH
38.
Gabbay, D.M.: Labelled Deductive Systems. Clarendon Press, Oxford (1996) MATH
39.
Gallin, D.: Intensional and Higher-Order Modal Logic. North Holland, New York (1975)MATH
40.
Giunchiglia, F.: Contextual reasoning. Epistemologia (Special Issue on Languages and Machines) 16, 345–364 (1993)
41.
Giunchiglia, F., Serafini, L.: Multilanguage hierarchical logics or: How we can do without modal logics. Artif. Intell. 65(1), 29–70 (1994)MathSciNetCrossRefMATH
42.
Gödel, K.: Collected Works, Unpublished Essays and Letters. Ontological Proof, pp. 65–85. Oxford University Press, Oxford (1970)
43.
Gödel, K.: Appx.A: Notes in Kurt Gödel’s Hand. In: [70], pp. 144–145 (2004)
44.
Guha, R.V.: Context: A Formalization and Some Applications. Ph.D. thesis, Stanford University (1991)
45.
46.
Jaśkowski, S.: Rachunek zdań dla systemów dedukcyjnych sprzecznych. Stud. Soc. Scientiarun Torunesis 1(5), 55–77 (1948)
47.
48.
Kaliszyk, C., Urban, J.: Hol(y)hammer: online ATP service for HOL light. Math. Comput. Sci. 9(1), 5–22 (2015)CrossRefMATH
49.
50.
51.
52.
McCarthy, J.: Notes on formalizing context. In: Proceedings of IJCAI 1993, pp. 555–562 (1993)
53.
Muskens, R.: Higher order modal logic. In: Blackburn, P., et al. (eds.) Handbook of Modal Logic, pp. 621–653. Elsevier, Dordrecht (2006)
54.
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Berlin (2002)MATH
55.
Otten, J.: Mleancop: A connection prover for first-order modal logic. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) Automated Reasoning. LNCS, vol. 8562, pp. 269–276. Springer, Switzerland (2014)
56.
57.
Paulin-Mohring, C.: Introduction to the calculus of inductive constructions. In: Delahaye, D., Woltzenlogel Paleo, B. (eds.), All about Proofs, Proofs for All, Mathematical Logic and Foundations. College Publications, London (2015)
58.
Pease, A.: Ontology: A Practical Guide. Articulate Software Press, Angwin (2011)
59.
Pease, A., Sutcliffe, G.: First order reasoning on a large ontology. In: Sutcliffe, G., Urban, J., Schulz, S. (eds.), Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories (ESARLT), CEUR Workshop Proceedings, vol. 257, CEUR-WS.org (2007)
60.
61.
Priest, G., Sylvan, R.: Simplified semantics for basic relevant logics. J. Philos. Logic (1992)
62.
Ramachandran, D., Reagan, P., Goolsbey, K.: First-orderized ResearchCyc: Expressivity and efficiency in a common-sense ontology. In: Shvaiko P. (ed.), Papers from the AAAI Workshop on Contexts and Ontologies: Theory, Practice and Applications, Pittsburgh, Pennsylvania, USA, 2005. Technical report WS-05-01 published by The AAAI Press, Menlo Park, California, July 2005
63.
Raths, Thomas, Otten, Jens: The QMLTP problem library for first-order modal logics. In: Gramlich, Bernhard, Miller, Dale, Sattler, Uli (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 454–461. Springer, Heidelberg (2012) CrossRef
64.
Restall, G., Slaney, J.: Realistic belief revision. In: Proceedings of the Second World Conference in the Fundamentals of Artificial Intelligence, pp. 367–378 (1995)
65.
Scott, D.: Appx.B: Notes in Dana Scott’s Hand. In: [70], pp. 145–146 (2004)
66.
67.
68.
Sobel, J.H.: Gödel’s ontological proof. In On Being and Saying. Essays for Richard Cartwright, pp. 241–261, MIT Press (1987)
69.
Sobel, J.H.: Logic and Theism: Arguments for and Against Beliefs in God. Cambridge University Press, Cambridge (2004)
70.
Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reasoning 43(4), 337–362 (2009)CrossRefMATH
71.
Sutcliffe, G., Benzmüller, C.: Automated reasoning in higher-order logic using the TPTP THF infrastructure. J. Formalized Reasoning 3(1), 1–27 (2010)MathSciNetMATH
72.
73.
Metadaten
Titel
Higher-Order Modal Logics: Automation and Applications
verfasst von
Christoph Benzmüller
Bruno Woltzenlogel Paleo
Copyright-Jahr
2015
Buch
Reasoning Web. Web Logic Rules

Print ISBN: 978-3-319-21767-3

Electronic ISBN: 978-3-319-21768-0

Copyright-Jahr: 2015

DOI
https://doi.org/10.1007/978-3-319-21768-0_2

Premium Partner

    Bildnachweise