4.7 Article

A first polynomial non-clausal class in many-valued logic

期刊

FUZZY SETS AND SYSTEMS
卷 456, 期 -, 页码 1-37

出版社

ELSEVIER
DOI: 10.1016/j.fss.2022.10.008

关键词

Regular many-valued logic; Horn; Non-clausal; Tractability; Resolution; DPLL; Satisfiability testing; Logic programming; Theorem proving

向作者/读者索取更多资源

This paper presents research on the relevance of polynomial classes of formulas to deductive efficiency. A new class, RH, is introduced by combining regular classes: Horn and NC. It is shown that RH can be recognized and solved polynomially and it is tractable. RH is also extended to other non-classical logics and can pave the way for efficient non-clausal approximate reasoning.
The relevance of polynomial classes of formulas to deductive efficiency motivated their further research, and currently, a great number of such classes is known. Nevertheless, they have been exclusively sought in the setting of propositional logic and clausal form, which is of course expressively limiting for real-world applications.Along these lines and towards making tractability applicable beyond propositional clausal logic, firstly, we define the Regular many-valued Horn Non-Clausal (NC) class, or RH, obtained by suitably amalgamating both regular classes: Horn and NC. Then we show that recognizing whether any NC formula is Horn-NC takes only linear time.Secondly, we demonstrate that the relationship between RH and: (1) its subclass of regular Horn formulas is that syntactically RH subsumes the Horn class but semantically both classes are equivalent; and (2) its superclass of regular non-clausal formulas is that RH contains all non-clausal formulas whose clausal form is Horn.Thirdly, we define Regular Non-Clausal Unit-Resolution, or RURNC, and prove that RURNC is complete for RH and also checks its satisfiability in polynomial time. Altogether, RH is a class recognized and solved polynomially, which shows that our intended goal is reached since RH is many-valued, non-clausal and tractable. Fourthly, based on RH, we characterize extensive classes of Horn-NC-like formulas, super-classes of RH, which are composed of formulas that are logically equivalent to some formula in RH. We furnish syntactical patterns of such Horn-NC-like formulas, being outside RH and whose satisfiability test is also decidable in polynomial time.As RH and RURNC 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.Field: Tractable Approximate Automated Reasoning.(c) 2022 Elsevier B.V. All rights reserved.

作者

我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。

评论

主要评分

4.7
评分不足

次要评分

新颖性
-
重要性
-
科学严谨性
-
评价这篇论文

推荐

暂无数据
暂无数据