Skip to main content
main-content

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

01.01.2019 | Ausgabe 1/2020

Journal of Automated Reasoning 1/2020

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

Zeitschrift:
Journal of Automated Reasoning > Ausgabe 1/2020
Autoren:
Christoph Benzmüller, Dana S. Scott
Wichtige Hinweise

Electronic supplementary material

The online version of this article (https://​doi.​org/​10.​1007/​s10817-018-09507-7) contains supplementary material, which is available to authorized users.
Benzmüller received funding from the German National Research Foundation DFG under Heisenberg grant Towards Computational Metaphysics (BE 2501/9-2) and from VolkswagenStiftung under grant Consistent Rational Argumentation in Politics (CRAP).

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

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.

Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

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

  • über 69.000 Bücher
  • über 500 Zeitschriften

aus folgenden Fachgebieten:

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

Testen Sie jetzt 30 Tage kostenlos.

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 58.000 Bücher
  • über 300 Zeitschriften

aus folgenden Fachgebieten:

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




Testen Sie jetzt 30 Tage kostenlos.

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 50.000 Bücher
  • über 380 Zeitschriften

aus folgenden Fachgebieten:

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




Testen Sie jetzt 30 Tage kostenlos.

Zusatzmaterial
Nur für berechtigte Nutzer zugänglich
Literatur
Über diesen Artikel

Weitere Artikel der Ausgabe 1/2020

Journal of Automated Reasoning 1/2020 Zur Ausgabe

Premium Partner

    Bildnachweise