Compressing Propositional Proofs by Common Subproof Extraction
Compressing Propositional Proofs by Common Subproof Extraction
复制标题
通过公共子证明提取来压缩命题证明
DOI：
--
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
C. Sinz
中科院分区：
文献类型：
--
作者：
C. Sinz
命题逻辑决策过程[1，2，3，4，5，6]是硬件和软件验证、人工智能和自动定理证明[7，8，9，10，11，12]中许多应用的核心。它们已被用来成功地解决相当大的问题。然而，在许多实际应用中，仅仅从决策过程中得到是/否的答案是不够的。需要一个代表样本解决方案的模型，或者一个理由，为什么公式没有。因此，例如在声明式建模或产品配置[9，10]中，客户给出的不一致规范对应于不可满足的问题实例。为了指导客户纠正他的规范，解释为什么它是错误的可能会有很大的帮助。在模型检查的上下文中，使用证明，例如，用于抽象细化[11]，或通过插值的近似图像计算[13]。一般来说，证明对于通过证明检查进行认证也很重要[14]。
Propositional logic decision procedures [1,2,3,4,5,6] lie at the heart of many applications in hard- and software verification, artificial intelligence and automatic theorem proving [7,8,9,10,11,12]. They have been used to successfully solve problems of considerable size. In many practical applications, however, it is not sufficient to obtain a yes/no answer from the decision procedure. Either a model, representing a sample solution, or a justification, why the formula possesses none is required. So, e.g. in declarative modeling or product configuration [9,10] an inconsistent specification given by a customer corresponds to an unsatisfiable problem instance. To guide the customer in correcting his specification, a justification why it is erroneous can be of great help. In the context of model checking proofs are used, e.g., for abstraction refinement [11], or approximative image computations through interpolants [13]. In general, proofs are also important for certification through proof checking [14].