Propositional Reasoning
Propositional Reasoning
复制标题
命题推理
DOI：
10.1007/3-540-45319-9_2
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
M. Fourman
中科院分区：
文献类型：
--
作者：
M. Fourman
命题（布尔）逻辑在概念上很简单。它为有限结构的表示提供了丰富的基础，但计算复杂。当前的许多验证技术都基于命题编码。命题表示会导致通常在计算上难以解决的问题。然而，用于表示命题公式的数据结构和用于推理命题公式的算法提供了可应用于各种计算问题的通用工具。自然问题实例通常可以通过这些通用方法有效地解决。关于命题推理算法的文献以及从密码学、约束满足和规划到系统设计、验证和验证等领域的任务命题表示技术的文献越来越多。我们提出了逻辑有效性问题的命题编码的模型理论解释。有效性是从模型理论上来表征的。对于受限逻辑，检查受限模型类别的有效性可能就足够了。有限域上的结构类可以编码为命题理论，并且此类中的有效性通过命题公式的句法翻译进行命题编码。这为生成适合使用 BDD 或 SAT 包进行分析的高效命题编码提供了统一的设置。
Propositional (Boolean) logic is conceptually simple. It provides a rich basis for the representation of finite structures, but is computationally complex. Many current verification techniques are based on propositional encodings.Propositional representations lead to problems that are, in general, computationally intractable. Nevertheless, datastructures for representing propositional formulae, and algorithms for reasoning about them, provide generic tools that can be applied to a wide variety of computational problems. Natural problem instances are often effectively solved by these generic approaches.There is a growing literature of algorithms for propositional reasoning, and of techniques for propositional representation of tasks in areas ranging from cryptography, constraint satisfaction and planning, to system design, validation and verification.We present a model-theoretic account of propositional encodings for questions of logical validity. Validity is characterised model-thoretically. For restricted logics, checking validity in a restricted class of models may suffce. Classes of structures on a finite domain can be encoded as propositional theories, and validity in such a class is encoded propositionally, by means of a syntactic translation to a propositional formula.This provides a unified setting for generating efficient propositional encodings suitable for analysis using BDD or SAT packages.