Recognition with Quantified Refutational Universal System for Many-Valued Logic
摘要
A new quantified refutational proof system is introduced such that every quantified many-valued unsatisfiable formula for each version of many-valued logic can be refuted in the described system. This proof system is based on the splitting method of variables. It is “weak” system with a “simple” proof construction strategy. However the preference for such systems lies in the possibility of proof simplification by choosing the order of splinted variables. It is also shown that the variant of this system for two-valued quantified formulas is much better by proof complexities of some formula classes than any quantified resolution systems. The introduced system can be used by recognition in such fields as Formal Verification, Artificial Intelligence, Operations Research, Cryptography, Computational Biology, and Medical Diagnosis.