A First Polynomial Non-Clausal Class in Many-Valued Logic

TL;DR

This paper introduces a new polynomial-time, many-valued, non-clausal class called RH, which extends Horn logic and supports efficient reasoning, potentially improving non-classical logic applications.

Contribution

It defines the RH class, proves its semantic equivalence with Horn logic, and introduces RUR-NC for polynomial satisfiability checking, advancing non-clausal reasoning.

Findings

RH subsumes the Horn class syntactically but is semantically equivalent.

RUR-NC is complete for RH and checks satisfiability in polynomial time.

RH and RUR-NC can extend efficient DPLL-based reasoning to non-classical logics.

Abstract

The relevance of polynomial formula classes to deductive efficiency motivated their search, and currently, a great number of such classes is known. Nonetheless, they have been exclusively sought in the setting of clausal form and propositional logic, which is of course expressively limiting for real applications. As a consequence, a first polynomial propositional class in non-clausal (NC) form has recently been proposed. Along these lines and towards making NC tractability applicable beyond propositional logic, firstly, we define the Regular many-valued Horn Non-Clausal class, or RH, obtained by suitably amalgamating both regular classes: Horn and NC. Secondly, we demonstrate that the relationship between (1) RH and the regular Horn class is that syntactically RH subsumes the Horn class but that both classes are equivalent semantically; and between (2) RH and the regular non-clausal class is that RH contains all NC formulas whose clausal form is Horn. Thirdly, we define Regular Non-Clausal Unit-Resolution, or RUR-NC , and prove both that it is complete for RH and that checks its satisfiability in polynomial time. The latter fact shows that our intended goal is reached since RH is many-valued, non-clausal and tractable. As RH and RUR-NC are, both, basic in the DPLL scheme, the most efficient in propositional logic, and can be extended to some other non-classical logics, we argue that they pave the way for efficient non-clausal DPLL-based approximate reasoning.