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
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Journal of Automated Reasoning
Erschienen in: Journal of Automated Reasoning 1/2020

01.01.2019

Automating Free Logic in HOL, with an Experimental Application in Category Theory

verfasst von: Christoph Benzmüller, Dana S. Scott

Erschienen in: Journal of Automated Reasoning | Ausgabe 1/2020

Einloggen

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

search-config
loading …

Abstract

A shallow semantical embedding of free logic in classical higher-order logic is presented, which enables the off-the-shelf application of higher-order interactive and automated theorem provers for the formalisation and verification of free logic theories. Subsequently, this approach is applied to a selected domain of mathematics: starting from a generalization of the standard axioms for a monoid we present a stepwise development of various, mutually equivalent foundational axiom systems for category theory. As a side-effect of this work some (minor) issues in a prominent category theory textbook have been revealed. The purpose of this article is not to claim any novel results in category theory, but to demonstrate an elegant way to “implement” and utilize interactive and automated reasoning in free logic, and to present illustrative experiments.
Vorheriger Artikel ExpTime Tableaux with Global Caching for Hybrid PDL
Nächster Artikel Priority Inheritance Protocol Proved Correct

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 "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

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
Anhänge
Nur mit Berechtigung zugänglich
Fußnoten
1
Cf. Sect. 4.4 for further information.
 
2
Calculi for free logic are presented in [30]; see also the references therein.
 
3
The predication \( E x\) represents that x is a member of E.
 
4
The \(\star \) symbol is not to be confused with any other symbol in Isabelle/HOL.
 
5
It is well known that we could work with a much smaller set of logical connectives, see e.g. Sect. 1.4 of Andrews’s overview article [2]. The choice here closely reflects the set of primitive connectives as chosen in higher-order automated theorem provers such as LEO-II [13], Leo-III [12], and Satallax [18].
 
6
Similar soundness and completeness proofs for shallow semantical embeddings have been presented in [4] and [5].
 
7
In fact, it may be safely assumed that there are no other constant symbols given in a HOL signature, except for the symbols in \(\widehat{F}\) and \(\widehat{P}\), the symbols https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-09507-7/MediaObjects/10817_2018_9507_IEq328_HTML.gif and \(\varvec{\star _{i}}\) and the logical connectives.
 
8
The fixings introduced in \(\widehat{M}\) are not in conflict with any of the requirements regarding frames and interpretations. The existence of a valuation function V for an HOL interpretation crucially depends on how sparse the function spaces have been chosen in frame \(\{D_\alpha \}_{\alpha \in {T}}\). Andrews [1] discusses criteria that are sufficient to ensure the existence of a valuation function; in \(\widehat{M}\) these requirements are met.
 
9
In the remainder of this article, and inline with our text so far, we present the formulas of \({\text {FFOL}} \) in non-boldface font. These formulas have been encoded in Isabelle/HOL using the abbreviations as introduced in Fig. 2. In the actual source encoding, however, the usage of boldface and non-boldface is (for technical reasons) reversed.
 
10
Technical remark: We have selected CVC4 in our experiments as the default SMT solver, since we did run into errors when working with Z3. These errors can easily be reconstructed in the provided source files when switching back to Z3 as default.
 
11
An expert reviewer of this article, to whom we are very grateful, provided alternative proofs which can be fully replayed in the kernel of Isabelle.
 
12
A recipe for this translation is as follows: (i) replace all \(x \circ y\) by \(y \cdot x\), (ii) rename the variables to get them again in alphabetical order, (iii) replace \(\varphi \Box \) by \(\textit{cod }\varphi \) and \(\Box \varphi \) by \(\textit{dom }\varphi \), and finally (iv) replace \(\textit{cod }y \cong \textit{dom }x\) (resp. \(\textit{cod }y \simeq \textit{dom }x\)) by \(\textit{dom }x \cong \textit{cod }y\) (resp. \(\textit{dom }x \simeq \textit{cod }y\)).
 
13
Def. 1.11 in Freyd Scedrov: “The ordinary equality sign \(=\) [i.e., our \(\cong \)] will be used in the symmetric sense, to wit: if either side is defined then so is the other and they are equal. ...”
 
14
This could perhaps be an oversight, or it could indicate that Freyd and Scedrov actually mean the Axioms Set discussed in Sect. 5.2 below.
 
15
For this we have to inactivate the axiom that postulates that \(\star \) is an undefined/non-existing object.
 
16
The discussion in our releated conference paper [9] was before the discovery of the above constricted inconsistency issue, which tells us that the system (in our setting) can even be reduced to axioms A1, A2a, and A3a (when we assume undefined objects).
 
17
This minimal set of axioms has also been mentioned by Freyd in a note [22] and attributed to Martin Knopman. However, the proof sketch presented there seems to fail when the adapted version of A1 (with \(\simeq \)) is employed.
 
Literatur
1.
2.
3.
Barendregt, H., Dekkers, W., Statman, R.: Lambda Calculus with Types. Perspectives in Logic. Cambridge University Press, Cambridge (2013)CrossRef
4.
Benzmüller, C.: Automating quantified conditional logics in HOL. In: Rossi, F. (ed.) Proceedings of IJCAI-23. Beijing, China (2013)
5.
6.
Benzmüller, C., Brown, C., Kohlhase, M.: Higher-order semantics and extensionality. J. Symb. Log. 69(4), 1027–1088 (2004)MathSciNetCrossRef
7.
Benzmüller, C., Brown, C., Kohlhase, M.: Cut-simulation and impredicativity. Log. Methods Comput. Sci. 5(1:6), 1–21 (2009)MathSciNetMATH
8.
Benzmüller, C., Miller, D.: Automation of higher-order logic. In: Siekmann, J., Gabbay, D., Woods, J. (eds.) Handbook of the History of Logic, Volume 9—Logic and Computation. Elsevier, Amsterdam (2014)
9.
Benzmüller, C., Scott, D.: Automating free logic in Isabelle/HOL. In: Greuel, G.M., Koch, T., Paule, P., Sommese, A. (eds.) Mathematical Software—ICMS 2016, 5th International Congress, Proceedings, LNCS, vol. 9725, pp. 43–50. Springer, Berlin, Germany (2016)CrossRef
10.
11.
12.
Benzmüller, C., Steen, A., Wisniewski, M.: Leo-III version 1.1 (system description). In: Eiter, T., Sands, D. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)—Short Papers, Kalpa Puplications. EasyChair, Maun, Botswana (2017) (to appear)
13.
Benzmüller, C., Sultana, N., Paulson, L.C., Theiss, F.: The higher-order prover Leo-II. J. Autom. Reason. 55(4), 389–404 (2015)MathSciNetCrossRef
14.
15.
Blanchette, J.C., Böhme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. J. Autom. Reason. 51(1), 109–128 (2013)MathSciNetCrossRef
16.
Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11–14, 2010. Proceedings, Lecture Notes in Computer Science, vol. 6172, pp. 131–146. Springer (2010)
17.
Blanchette, J.C., Popescu, A., Wand, D., Weidenbach, C.: More SPASS with Isabelle—superposition with hard sorts and configurable simplification. In: Beringer, L., Felty, A.P. (eds.) Interactive Theorem Proving—Third International Conference, ITP 2012, Princeton, NJ, USA, August 13–15, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7406, pp. 345–360. Springer (2012)
18.
Brown, C.E.: Satallax: an automatic higher-order prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) Automated Reasoning—6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26–29, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7364, pp. 111–117. Springer (2012)
19.
20.
Deters, M., Reynolds, A., King, T., Barrett, C.W., Tinelli, C.: A tour of CVC4: How it works, and how to use it. In: Claessen, K., Kuncak, V. (eds.) Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, October 21–24, 2014, p. 7. IEEE (2014)
21.
de Moura, L.M., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29–April 6, 2008. Proceedings, Lecture Notes in Computer Science, vol. 4963, pp. 337–340. Springer (2008)
22.
23.
Freyd, P., Scedrov, A.: Categories. North Holland, Allegories (1990)MATH
24.
Kovács, L., Voronkov, A.: First-order theorem proving and vampire. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification—25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13–19, 2013. Proceedings, Lecture Notes in Computer Science, vol. 8044, pp. 1–35. Springer (2013)
25.
Lambert, K.: The definition of e(xistence)! in free logic. In: Abstracts: The International Congress for Logic, Methodology and Philosophy of Science. Stanford University Press, Stanford (1960)
26.
Lambert, K.: Free Logic: Selected Essays. Cambridge University Press, Cambridge (2002)CrossRef
27.
28.
Makarenko, I.: Automatisierung von Freier Logik in Logik Höherer Stufe. Bachelorarbeit. Freie Universität Berlin, Institut für Informatik (2016)
29.
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. No. 2283 in LNCS. Springer (2002)
30.
31.
Schulz, S.: System description: E 1.8. In: McMillan, K.L., Middeldorp, A., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning—19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14–19, 2013. Proceedings, Lecture Notes in Computer Science, vol. 8312, pp. 735–743. Springer (2013). http://​dx.​doi.​org/​10.​1007/​978-3-642-45221-5
32.
Scott, D.: Existence and description in formal logic. In: Schoenman, R. (ed.) Bertrand Russell: Philosopher of the Century, pp. 181–200. George Allen & Unwin, London (1967) (Reprinted with additions in: Philosophical Application of Free Logic, edited by K. Lambert. Oxford Universitry Press, 1991, pp. 28–48)
33.
Scott, D.: Identity and existence in intuitionistic logic. In: Fourman, M., Mulvey, C., Scott, D. (eds.) Applications of Sheaves: Proceedings of the Research Symposium on Applications of Sheaf Theory to Logic, Algebra, and Analysis, Durham, July 9–21, 1977, Lecture Notes in Mathematics, vol. 752, pp. 660–696. Springer, Berlin, Heidelberg (1979)
34.
Sutcliffe, G., Benzmüller, C.: Automated reasoning in higher-order logic using the TPTP THF infrastructure. J. Formaliz. Reason. 3(1), 1–27 (2010)MathSciNetMATH
35.
Wisniewski, M., Steen, A., Benzmüller, C.: TPTP and beyond: representation of quantified non-classical logics. In: Benzmüller, C., Otten, J. (eds.) ARQNL 2016. Automated Reasoning in Quantified Non-Classical Logics, vol. 1770, pp. 51–65. CEUR Workshop Proceedings. http://​ceur-ws.​org (2016)
Metadaten
Titel
Automating Free Logic in HOL, with an Experimental Application in Category Theory
verfasst von
Christoph Benzmüller
Dana S. Scott
Publikationsdatum
01.01.2019
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 1/2020
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-018-09507-7

Weitere Artikel der Ausgabe 1/2020

Journal of Automated Reasoning 1/2020 Zur Ausgabe

OriginalPaper

Politeness and Combination Methods for Theories with Bridging Functions

OriginalPaper

A Conflict-Driven Solving Procedure for Poly-Power Constraints

OriginalPaper

A Prover Dealing with Nominals, Binders, Transitivity and Relation Hierarchies

OriginalPaper

ExpTime Tableaux with Global Caching for Hybrid PDL

OriginalPaper

Priority Inheritance Protocol Proved Correct