Download PDFOpen PDF in browserCurrent version

Positive Free Higher-Order Logic and its Automation via a Semantical Embedding

EasyChair Preprint no. 3621, version 1

Versions: 12history
15 pagesDate: June 15, 2020


Free logics are a family of logics that are free of any existential assumptions. Unlike traditional classical and non-classical logics, they support an elegant modeling of nonexistent objects and partial functions as relevant for a wide range of applications in computer science, philosophy, mathematics, and natural language semantics. While free first-order logic has been addressed in the literature, free higher-order logic has not been studied thoroughly so far. Contributions of this paper include (i) the development of a notion and definition of free higher-order logic in terms of a positive semantics (partly inspired by Farmer’s partial functions version of Church’s simple type theory), (ii) the provision of a faithful shallow semantical embedding of positive free higher-order logic into classical higher-order logic, (iii) the implementation of this embedding in the Isabelle/HOL proof-assistant, and (iv) the exemplary application of our novel reasoning framework for an automated assessment of Prior’s paradox in positive free quantified propositional logics, i.e., a fragment of positive free higher-order logic.

Keyphrases: Free Higher-Order Logic, free logic, Interactive and Automated Theorem Proving, Knowledge Representation and Reasoning, Partiality and undefinedness, Philosophical foundations of AI, positive free logic, Prior’s paradox

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
  author = {Irina Makarenko and Christoph Benzmüller},
  title = {Positive Free Higher-Order Logic and its Automation via a Semantical Embedding},
  howpublished = {EasyChair Preprint no. 3621},

  year = {EasyChair, 2020}}
Download PDFOpen PDF in browserCurrent version