paper-with-me

Papers

Minimum Model Semantics for Extensional Higher-order Logic Programming with Negation

2014-05-15 · Angelos Charalambidis, Zoltán Ésik, Panos Rondogiannis

Extensional higher-order logic programming has been introduced as a generalization of classical logic programming. An important characteristic of this paradigm is that it preserves all the well-known properties of traditional logic programming. In this paper we consider the semantics of negation in the context of the new paradigm. Using some recent results from non-monotonic fixed-point theory, we demonstrate that every higher-order logic program with negation has a unique minimum infinite-valued model. In this way we obtain the first purely model-theoretic semantics for negation in extensional higher-order logic programming. Using our approach, we resolve an old paradox that was introduced by W. W. Wadge in order to demonstrate the semantic difficulties of higher-order logic programming.

📄 PDF Abstract BibTeX arXiv:1405.3792

Code (0)

등록된 구현이 없습니다.

Tasks

Negation

Similar Papers 제목 키워드 기반

Extensional Higher-Order Paramodulation in Leo-III

2019-07-26 · Alexander Steen, Christoph Benzmüller

Leo-III is an automated theorem prover for extensional type theory with Henkin semantics and choice. Reasoning with primitive equality is enabled by adapting paramodulation-based proof search to higher-order logic. The p…

The Higher-Order Prover Leo-III (Extended Version)

2018-02-08 · Alexander Steen, Christoph Benzmüller

The automated theorem prover Leo-III for classical higher-order logic with Henkin semantics and choice is presented. Leo-III is based on extensional higher-order paramodulation and accepts every common TPTP dialect (FOF,…

Optimistic Higher-Order Superposition

2025-10-21 · Alexander Bentkamp, Jasmin Blanchette, Matthias Hetzenberger, Uwe Waldmann arxiv

The $λ$-superposition calculus is a successful approach to proving higher-order formulas. However, some parts of the calculus are extremely explosive, notably due to the higher-order unifier enumeration and the functiona…

Hyperintensional Reasoning based on Natural Language Knowledge Base

2019-06-18 · Marie Duží, Aleš Horák

The success of automated reasoning techniques over large natural-language texts heavily relies on a fine-grained analysis of natural language assumptions. While there is a common agreement that the analysis should be hyp…

Stable Models for Infinitary Formulas with Extensional Atoms

2016-08-04 · Amelia Harrison, Vladimir Lifschitz

The definition of stable models for propositional formulas with infinite conjunctions and disjunctions can be used to describe the semantics of answer set programming languages. In this note, we enhance that definition b…