ClaVa · Clausal forms for Vague information processing

Clausal forms for Vague information processing

The issue being addressed in this project is the understanding of closed classes of formulas in the context of substructural logics, which we denote clausal-form-systems as inherited from the classical logic case. These classes of formulas might offer equivalent computational strength to the full logic for what concerns certain problems (e.g., SAT, MAX-SAT, or other computational questions), but keep a lower complexity or at least, be solvable more efficiently in practical cases. The importance to society might be long-term, since this is a basic-research project, but it is related to the increase in the exploitation in practical and industrial context of substructural and non-classical logics, which are the better suited to model graded and vague information, or even to be defined ad-hoc according to complex problem management. This increase in potential use is linked to the achievement of lower complexity of classes of formulas of equivalent strength for the problems under study. The main objective of this project is to study clausal-form systems for real and rational-valued events, facing the questions of their general definition, usage and solvable problems (SAT and optimality) from the point of view of their complexity, algorithmic design and applicability. It is focused on studying in full generality the definition of clausal form in non-classical logics for their use in vague knowledge representation. At the most general level, it is planned to reach a definition based on n-ary- level subsets of literals and using symmetric term-definable operations of arbitrary arity to combine each level, over Mathematical Fuzzy Logics and over some other Substructural Logics. We * introduce definitions of general clausal forms over some of the above logical systems, study their possible equivalences and their logical properties (axiomatization of fragments, admissible rules, etc); * design and test efficient solving procedures for three natural questions: SAT (evaluation sending the clause to 1), Max-SAT (evaluation maximizing the number of satisfied clauses) and optimality with respect to an objective (evaluation maximizing/minimizing the clause) * do complexity classification of some of the clausal form classes, and study their normality (i.e., if any formula is equivalent to one in the desired form for the problems above).

Текст от CORDIS, на английски · Данни: CORDIS, © Европейски съюз