Abstract <p>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.</p>

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Recognition with Quantified Refutational Universal System for Many-Valued Logic

  • Anahit Chubaryan

摘要

Abstract

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.