We give a purely model-theoretic characterization of the semantics of logic programs with negation-as-failure allowed in clause bodies. In our semantics the meaning of a program is, as in the classical case, the unique minimum model in a program-independent ordering. We use an expanded truth domain that has an uncountable linearly ordered set of truth values between False (the minimum element) and True (the maximum), with a Zero element in the middle. The truth values below Zero are ordered like the countable ordinals. The values above Zero have exactly the reverse order. Negation is interpreted as reflection about Zero followed by a step towards Zero; the only truth value that remains unaffected by negation is Zero. We show that every program has a unique minimum model M_P, and that this model can be constructed with a T_P iteration which proceeds through the countable ordinals. Furthermore, we demonstrate that M_P can also be obtained through a model intersection construction which generalizes the well-known model intersection theorem for classical logic programming. Finally, we show that by collapsing the true and false values of the infinite-valued model M_P to (the classical) True and False, we obtain a three-valued model identical to the well-founded one.
In this paper we consider Epistemic Logic Programs, which extend Answer Set Programming (ASP) with "epistemic operators" and "epistemic negation", and a recent approach to the semantics of such programs in terms of World Views. We propose some observations on the existence and number of world views. We show how to exploit an extended ASP semantics in order to: (i) provide a characterization of world views, different from existing ones; (ii) query world views and query the whole set of world views.
Universidade da Coruña（拉科鲁尼亚大学）；University of Toulouse（图卢兹大学）；CNRS（法国国家科学研究中心）；Universität Potsdam（波茨坦大学）；Universidad Politécnica de Madrid（马德里理工大学）
A common feature in Answer Set Programming is the use of a second negation, stronger than default negation and sometimes called explicit, strong or classical negation. This explicit negation is normally used in front of atoms, rather than allowing its use as a regular operator. In this paper we consider the arbitrary combination of explicit negation with nested expressions, as those defined by Lifschitz, Tang and Turner. We extend the concept of reduct for this new syntax and then prove that it can be captured by an extension of Equilibrium Logic with this second negation. We study some proper…
Answering logical queries over incomplete knowledge bases is challenging because: 1) it calls for implicit link prediction, and 2) brute force answering of existential first-order logic queries is exponential in the number of existential variables. Recent work of query embeddings provides fast querying, but most approaches model set logic with closed regions, so lack negation. Query embeddings that do support negation use densities that suffer drawbacks: 1) only improvise logic, 2) use expensive distributions, and 3) poorly model answer uncertainty. In this paper, we propose Logic Embeddings, …
There has recently been an increasing interest in declarative data analysis, where analytic tasks are specified using a logical language, and their implementation and optimisation are delegated to a general-purpose query engine. Existing declarative languages for data analysis can be formalised as variants of logic programming equipped with arithmetic function symbols and/or aggregation, and are typically undecidable. In prior work, the language of $\mathit{limit\ programs}$ was proposed, which is sufficiently powerful to capture many analysis tasks and has decidable entailment problem. Rules …
Towards a unified theory of logic programming semantics: Level mapping characterizations of selector generated models
目前，针对带否定的逻辑程序所创建的各种表达扩展和不同语义是多样的、异质的，并且缺乏全面的比较研究，从而以统一的方式描绘出众多的视角。然而，最近，新的方法已经提出，它允许一个得到不同的声明性语义的逻辑程序与否定的统一表征。在本文中，我们研究了其中两种方法之间的关系，即[Hitzler and Wendt 2005]的水平映射特征和[Schwarz 2004]的选择器生成模型。我们将表明，后者可以被捕获的手段，前者，从而支持声称，层次映射提供了一个非常灵活的框架，这是适用于非常dilibrium定义的语义。
我们扩展答案集语义处理不一致的程序（包含经典否定），通过找到一个“最佳”的答案集。在不一致的程序中，规则的偏序是很自然的，表示满足某些规则的偏好，可能以违反不太重要的规则为代价。我们表明，这样的规则顺序诱导一个自然的顺序扩展的答案集，我们称之为首选答案集的最小元素。我们描述了所得到的语义的表达性，并表明它可以模拟否定失败，析取和其他一些形式主义，如逻辑程序有序析取。该方法被证明是有用的，在几个应用领域，例如修复数据库，其中最小的维修对应于首选的答案集。逻辑程序设计理论与实践（Theory and Practice of Logic Programming，TPLP）
Nowadays, the success of neural networks as reasoning systems is doubtless. Nonetheless, one of the drawbacks of such reasoning systems is that they work as black-boxes and the acquired knowledge is not human readable. In this paper, we present a new step in order to close the gap between connectionist and logic based reasoning systems. We show that two of the most used inference rules for obtaining negative information in rule based reasoning systems, the so-called Closed World Assumption and Negation as Finite Failure can be characterized by means of spiking neural P systems, a formal model …
We consider an example of four valued semantics partially inspired by quantum computations and negation-like operations occurred therein. In particular we consider a representation of so called square root of negation within this four valued semantics as an operation which acts like a cycling negation. We define two variants of logical matrices performing different orders over the set of truth values. Purely formal logical result of our study consists in axiomatizing the logics of defined matrices as the systems of binary consequence relation and proving correctness and completeness theorems f…
Proof-theoretic semantics (P-tS) is the paradigm of semantics in which meaning in logic is based on proof (as opposed to truth). A particular instance of P-tS for intuitionistic propositional logic (IPL) is its base-extension semantics (B-eS). This semantics is given by a relation called support, explaining the meaning of the logical constants, which is parameterized by systems of rules called bases that provide the semantics of atomic propositions. In this paper, we interpret bases as collections of definite formulae and use the operational view of the latter as provided by uniform proof-sear…
We show that the finite satisfiability problem for the unary negation fragment with arbitrary number of transitive relations is decidable and 2-ExpTime-complete. Our result actually holds for a more general setting in which one can require that some binary symbols are interpreted as arbitrary transitive relations, some as partial orders and some as equivalences. We also consider finite satisfiability of various extensions of our primary logic, in particular capturing the concepts of nominals and role hierarchies known from description logic. As the unary negation fragment can express unions of…
Paraconsistent Semantics for Extended Fuzzy Logic Programs via Approximation Fixpoint Theory [Extended Version]
TU Dresden（德累斯顿工业大学）；Open Universiteit（荷兰开放大学）；University of Cape Town（开普敦大学）；ScaDS.AI Center for Scalable Data Analytics and Artificial Intelligence, Dresden/Leipzig（萨克森可扩展数据分析和人工智能中心）
This paper focuses on order-preserving logics defined from varieties of distributive lattices with negation, and in particular on the problem of whether these can be axiomatized by means of finite Hilbert calculi. On the side of negative results, we provide a syntactic condition on the equational presentation of a variety that entails failure of finite axiomatizability for the corresponding logic. An application of this result is that the logic of all distributive lattices with negation is not finitely axiomatizable; likewise, we establish that the order-preserving logic of the variety of all …
We consider an extension of the unary negation fragment of first-order logic in which arbitrarily many binary symbols may be required to be interpreted as equivalence relations. We show that this extension has the finite model property. More specifically, we show that every satisfiable formula has a model of at most doubly exponential size. We argue that the satisfiability (= finite satisfiability) problem for this logic is TwoExpTime-complete. We also transfer our results to a restricted variant of the guarded negation fragment with equivalence relations.
In this paper we study the solvability of the equality negation task in a simple wait-free model where processes communicate by reading and writing shared variables or exchanging messages. In this task, two processes start with a private input value in the set {0,1,2}, and after communicating, each one must decide a binary output value, so that the outputs of the processes are the same if and only if the input values of the processes are different. This task is already known to be unsolvable; our goal here is to prove this result using the dynamic epistemic logic (DEL) approach introduced by G…
The Guarded Negation Fragment (GNFO) is a fragment of first-order logic that contains all positive existential formulas, can express the first-order translations of basic modal logic and of many description logics, along with many sentences that arise in databases. It has been shown that the syntax of GNFO is restrictive enough so that computational problems such as validity and satisfiability are still decidable. This suggests that, in spite of its expressive power, GNFO formulas are amenable to novel optimizations. In this paper we study the model theory of GNFO formulas. Our results include…
