Distilling from a knowledge base only the part that is relevant to a subset of alphabet, which is recognized as forgetting, has attracted extensive interests in AI community. In standard propositional logic, a general algorithm of forgetting and its computation-oriented investigation in various fragments whose satisfiability are tractable are still lacking. The paper aims at filling the gap. After exploring some basic properties of forgetting in propositional logic, we present a resolution-based algorithm of forgetting for CNF fragment, and some complexity results about forgetting in Horn, renamable Horn, q-Horn, Krom, DNF and CNF fragments of propositional logic.
Dependence is an important concept for many tasks in artificial intelligence. A task can be executed more efficiently by discarding something independent from the task. In this paper, we propose two novel notions of dependence in propositional logic: formula-formula dependence and formula forgetting. The first is a relation between formulas capturing whether a formula depends on another one, while the second is an operation that returns the strongest consequence independent of a formula. We also apply these two notions in two well-known issues: belief update and conservative extension. Firstly…
Four algorithms for propositional forgetting are compared. The first performs all possible resolutions and deletes the clauses containing a variable to forget. The second forgets a variable at time by resolving and then deleting all clauses that resolve on that variable. The third outputs the result of all possible linear resolutions on the variables to forget. The fourth generates a clause from the points of contradiction during a backtracking search. The latter emerges as the winner, with the second and first having some role in specific cases. The linear resolution algorithm performs poorly…
Independence -- the study of what is relevant to a given problem of reasoning -- has received an increasing attention from the AI community. In this paper, we consider two basic forms of independence, namely, a syntactic one and a semantic one. We show features and drawbacks of them. In particular, while the syntactic form of independence is computationally easy to check, there are cases in which things that intuitively are not relevant are not recognized as such. We also consider the problem of forgetting, i.e., distilling from a knowledge base only the part that is relevant to the set of que…
Aix Marseille Université（艾克斯-马赛大学）；CNRS（法国国家科学研究中心）；Vienna University of Technology（维也纳工业大学）
Recently, belief change within the framework of fragments of propositional logic has gained increasing attention. Previous works focused on belief contraction and belief revision on the Horn fragment. However, the problem of belief merging within fragments of propositional logic has been neglected so far. This paper presents a general approach to define new merging operators derived from existing ones such that the result of merging remains in the fragment under consideration. Our approach is not limited to the case of Horn fragment but applicable to any fragment of propositional logic charact…
Forgetting is removing variables from a logical formula while preserving the constraints on the other variables. In spite of being a form of reduction, it does not always decrease the size of the formula and may sometimes increase it. This article discusses the implications of such an increase and analyzes the computational properties of the phenomenon. Given a propositional Horn formula, a set of variables and a maximum allowed size, deciding whether forgetting the variables from the formula can be expressed in that size is $D^p$-hard in $Σ^p_2$. The same problem for unrestricted propositiona…
This paper presents a soundness and completeness proof for propositional intuitionistic calculus with respect to the semantics of computability logic. The latter interprets formulas as interactive computational problems, formalized as games between a machine and its environment. Intuitionistic implication is understood as algorithmic reduction in the weakest possible -- and hence most natural -- sense, disjunction and conjunction as deterministic-choice combinations of problems (disjunction = machine's choice, conjunction = environment's choice), and "absurd" as a computational problem of univ…
King’s College London（伦敦国王学院）；Universidad Politécnica de Madrid（马德里理工大学）；Universidad de Málaga（马拉加大学）
Interpolation is an important property of classical and many non classical logics that has been shown to have interesting applications in computer science and AI. Here we study the Interpolation Property for the propositional version of the non-monotonic system of equilibrium logic, establishing weaker or stronger forms of interpolation depending on the precise interpretation of the inference relation. These results also yield a form of interpolation for ground logic programs under the answer sets semantics. For disjunctive logic programs we also study the property of uniform interpolation tha…
We investigate the problem of reasoning in the propositional fragment of MBNF, the logic of minimal belief and negation as failure introduced by Lifschitz, which can be considered as a unifying framework for several nonmonotonic formalisms, including default logic, autoepistemic logic, circumscription, epistemic queries, and logic programming. We characterize the complexity and provide algorithms for reasoning in propositional MBNF. In particular, we show that entailment in propositional MBNF lies at the third level of the polynomial hierarchy, hence it is harder than reasoning in all the abov…
The logic FO(ID) uses ideas from the field of logic programming to extend first order logic with non-monotone inductive definitions. Such logic formally extends logic programming, abductive logic programming and datalog, and thus formalizes the view on these formalisms as logics of (generalized) inductive definitions. The goal of this paper is to study a deductive inference method for PC(ID), which is the propositional fragment of FO(ID). We introduce a formal proof system based on the sequent calculus (Gentzen-style deductive system) for this logic. As PC(ID) is an integration of classical pr…
Towards Non-Monotonic Entailment in Propositional Defeasible Standpoint Logic
University of Cape Town and CAIR, South Africa（开普敦大学和CAIR，南非）；Université Sorbonne Paris Nord, Inserm, Sorbonne Université, Limics, 93017 Bobigny, France（巴黎-索邦大学，Inserm，索邦大学，Limics，法国93017博比尼）；ISTI-CNR, Pisa, Italy（意大利比萨ISTI-CNR）
A General Framework of Epistemic Forgetting and its Instantiation by Ranking Functions
Faculty of Mathematics（数学系）；Computer Science, University of Hagen, 58084 Hagen, Germany（计算机科学，海因斯大学，德国）；Department of Computer Science, Technology Dortmund University, 44221 Dortmund, Germany（计算机科学系，多特蒙德技术大学，德国）
King’s College London（伦敦国王学院）；University of Liverpool（利物浦大学）
In this paper, we construct and investigate a hierarchy of spatio-temporal formalisms that result from various combinations of propositional spatial and temporal logics such as the propositional temporal logic PTL, the spatial logics RCC-8, BRCC-8, S4u and their fragments. The obtained results give a clear picture of the trade-off between expressiveness and computational realisability within the hierarchy. We demonstrate how different combining principles as well as spatial and temporal primitives can produce NP-, PSPACE-, EXPSPACE-, 2EXPSPACE-complete, and even undecidable spatio-temporal log…
A Fine-Grained Complexity View on Propositional Abduction -- Algorithms and Lower Bounds
Department of Computer and Information Science, Linköping University（链接öping大学计算机与信息科学系）；Department of Computer Science and Informatics, Jönköping University（约翰·索姆大学计算机科学与信息学系）
本文以知识库变量数 n 为参数研究命题溯因的细粒度复杂性，给出 Σ^P_2、NP 与 coNP 完全片段的改进算法，并在（强）指数时间假设下证明多个下界。
Centrale Supelec（中央理工-高等电力学院）；Université Paris-Saclay（巴黎萨克雷大学）；Université Paris-Dauphine（巴黎多芬大学）；CNRS（法国国家科学研究中心）；Télécom ParisTech（巴黎电信学院）
Belief revision of knowledge bases represented by a set of sentences in a given logic has been extensively studied but for specific logics, mainly propositional, and also recently Horn and description logics. Here, we propose to generalize this operation from a model-theoretic point of view, by defining revision in an abstract model theory known under the name of satisfaction systems. In this framework, we generalize to any satisfaction systems the characterization of the well known AGM postulates given by Katsuno and Mendelzon for propositional logic in terms of minimal change among interpret…
In this paper we show several similarities among logic systems that deal simultaneously with deductive and quantitative inference. We claim it is appropriate to call the tasks those systems perform as Quantitative Logic Reasoning. Analogous properties hold throughout that class, for whose members there exists a set of linear algebraic techniques applicable in the study of satisfiability decision problems. In this presentation, we consider as Quantitative Logic Reasoning the tasks performed by propositional Probabilistic Logic; first-order logic with counting quantifiers over a fragment contain…
Guizhou University（贵州大学）；Vrije Universiteit Amsterdam（阿姆斯特丹自由大学）；National University of Defense Technology（国防科技大学）
Computation Tree Logic (CTL) is one of the central formalisms in formal verification. As a specification language, it is used to express a property that the system at hand is expected to satisfy. From both the verification and the system design points of view, some information content of such property might become irrelevant for the system due to various reasons, e.g., it might become obsolete by time, or perhaps infeasible due to practical difficulties. Then, the problem arises on how to subtract such piece of information without altering the relevant system behaviour or violating the existin…
University of Calabria（卡拉布里亚大学）；Jerusalem College of Engineering（耶路撒冷工程学院）
In default theories, outliers denote sets of literals featuring unexpected properties. In previous papers, we have defined outliers in default logics and investigated their formal properties. Specifically, we have looked into the computational complexity of outlier detection problems and proved that while they are generally intractable, interesting tractable cases can be singled out. Following those results, we study here the tractability frontier in outlier detection problems, by analyzing it with respect to (i) the considered outlier detection problem, (ii) the reference default logic fragme…
