The possibilistic horn non-clausal knowledge bases

被引:1
作者
Imaz, Gonzalo E. [1 ]
机构
[1] Artificial Intelligence Res Inst IIIA CSIC, Barcelona, Spain
关键词
Possibilistic logic; Horn; Non-clausal; Inconsistency; Resolution; Satisfiability testing; LOGIC; SAT; PREFERENCES; UNCERTAINTY; COMPLEXITY; SEMANTICS; PROGRAMS; FORMULAS; SOLVER; QBFS;
D O I
10.1016/j.ijar.2022.11.002
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
Non-clausal deduction in classical logic is one of the oldest areas in artificial intelligence. It first appeared in the sixties and consequently a large body of research has been devoted to it. Within the last decades, computing with non-clausal formulas has been considered in several fields, and in particular, in answer set programming, wherein non-clausal or nested logic programs were conceived in 1999.Possibilistic logic is the most extended approach to handle uncertain and partially inconsistent information. Here, we generalize some well-known clausal outcomes in possibilistic reasoning to the non-clausal setting, concretely the objective of our proposal is: (i) to extend available insights from clausal to non-clausal form; (ii) to show that possibilistic reasoning admits feasible classes also at the non-clausal level; (iii) to combine the high expressiveness of non-clausal possibilistic logic with the highest efficient (polynomial) reasoning mechanisms; and (iii) to suggest that some meaningful subclasses of possibilistic nested programs can be efficiently processed.Firstly, we define the class of Possibilistic Horn Non-Clausal formulas, or HE, which covers the classes: possibilistic Horn and propositional Horn-NC. HE is shown to be non-clausal, analogous to the standard Horn class.Secondly, we define Possibilistic Non-Clausal Unit-Resolution, or URE, and prove that URE correctly computes the inconsistency degree of Horn-NC bases. URE is formulated in a clausal-like manner, which eases its understanding, formal proofs and future extension towards full non-clausal resolution.Thirdly, we prove that computing the inconsistency degree of Horn-NC bases takes polynomial time. Although there already exist tractable classes in possibilistic logic, all of them are clausal, and thus, HE turns out to be the first characterized polynomial non -clausal class within possibilistic reasoning.We discuss that our approach serves as a starting point to developing uncertain non-clausal reasoning on the basis of both methodologies: DPLL and resolution.(c) 2022 Elsevier Inc. All rights reserved.
引用
收藏
页码:357 / 389
页数:33
相关论文
共 84 条
  • [1] Aguilera G., 1997, MATHW SOFT COMPUT, V4, P99
  • [2] Alsinet T., 2002, ELECTRON NOTES THEOR, V66, P1
  • [3] Alsinet T., 2000, UAI 00 P 16 C UNCERT, P1
  • [4] A logic programming framework for possibilistic argumentation:: Formalization and logical properties
    Alsinet, Teresa
    Chesnevar, Carlos I.
    Godo, Lluis
    Simari, Guillermo R.
    [J]. FUZZY SETS AND SYSTEMS, 2008, 159 (10) : 1208 - 1228
  • [5] [Anonymous], 2005, AAAI Conference on Artificial Intelligence
  • [6] [Anonymous], 1994, Computational Complexity
  • [7] Bachmair L, 2001, HDB AUTOMATED REASON, P19
  • [8] Baral C., 2003, Knowledge Representation, Reasoning and Declarative Problem Solving
  • [9] Combining SAT Methods with Non-Clausal Decision Heuristics
    Barrett, Clark
    Donham, Jacob
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 125 (03) : 3 - 12
  • [10] Semantics for possibilistic answer set programs: Uncertain rules versus rules with uncertain conclusions
    Bauters, Kim
    Schockaert, Steven
    De Cock, Martine
    Vermeir, Dirk
    [J]. INTERNATIONAL JOURNAL OF APPROXIMATE REASONING, 2014, 55 (02) : 739 - 761