# The Possibilistic Horn Non-Clausal Knowledge Bases

arXiv: https://arxiv.org/abs/2111.07648 · HTML: https://mlsanity.com/paper/2111.07648/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 6 of its 84 references that are in the map.
- First posted on arXiv 15 Nov 2021.

## Builds on (most cited first, 6 of 6)

- [Mathematical Logic in Computer Science](https://mlsanity.com/paper/1802.03292/) (2018)
- [Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays](https://mlsanity.com/paper/1508.01288/) (2015)
- [A Complete Calculus for Possibilistic Logic Programming with Fuzzy Propositional Variables](https://mlsanity.com/paper/1301.3832/) (2013)
- [An Alternative Proof Method for Possibilistic Logic and its Application to Terminological Logics](https://mlsanity.com/paper/1302.6819/) (2013)
- [The Horn Non-Clausal Class and its Polynomiality](https://mlsanity.com/paper/2108.13744/) (2021)
- [A First Polynomial Non-Clausal Class in Many-Valued Logic](https://mlsanity.com/paper/2110.12901/) (2021)

## Abstract (arXiv)

Posibilistic logic is the most extended approach to handle uncertain and partially inconsistent information. Regarding normal forms, advances in possibilistic reasoning are mostly focused on clausal form. Yet, the encoding of real-world problems usually results in a non-clausal (NC) formula and NC-to-clausal translators produce severe drawbacks that heavily limit the practical performance of clausal reasoning. Thus, by computing formulas in its original NC form, we propose several contributions showing that notable advances are also possible in possibilistic non-clausal reasoning. em Firstly, we define the class of em Possibilistic Horn Non-Clausal Knowledge Bases, or mathcaloverlineH_Sigma, which subsumes the classes: possibilistic Horn and propositional Horn-NC. mathcaloverlineH_Sigma  is shown to be a kind of NC analogous of the standard Horn class. em Secondly, we define em Possibilistic Non-Clausal Unit-Resolution, or  UR_Sigma , and prove that  UR_Sigma  correctly computes the inconsistency degree of mathcaloverlineH_Sigma members. UR_Sigma  had not been proposed before and is formulated in a clausal-like manner, which eases its understanding, formal proofs and future extension towards non-clausal resolution. em Thirdly, we prove that computing the inconsistency degree of mathcaloverlineH_Sigma  members takes polynomial time. Although there already exist tractable classes in possibilistic logic, all of them are clausal, and thus, mathcaloverlineH_Sigma  turns out to be the first characterized polynomial non-clausal class within possibilistic reasoning.