SGER: Path Dissolution in Propositional Logic

SGER：命题逻辑中的路径消解

• 批准号: 0229339
• 负责人: Erik Rosenthal
• 金额: --
• 依托单位: University of New Haven
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2002
• 资助国家: 美国
• 起止时间: 2002-10-01 至 2004-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0229339&HistoricalAwards=false
• 关键词: SGER; Path; Dissolution; Propositional; Logic

ABSTRACT0229339Erik Rosenthal U of New HavenThe problem SAT determining whether a formula in propositional logic is satisfiable hasa long history in computer science. It is important in complexity theory and has myriad applicationsin fields such as robotics, optical character recognition, database systems, computerarchitecture, circuit design, and verification, to name but a few.The traditional view of much of the mechanical theorem proving community has been thatinteresting applications of automated deduction require first-order rather than propositionallogic. That view has begun to change in light of recent successes with propositional logic.Propositional logic is of course intractiable (unless NP = P). One approach to this problemwith knowledge representaion and database systems is knowledge compilation preprocessingthe underlying propositional theory. The idea is to do as much computation as possible in anoffline phase. Then queries in the online phase can be handled quickly. Horn clauses, orderedbinary decision diagrams, sets of prime implicates/implicants, and decomposable negationnormal form (DNNF) have all been proposed as targets of such compilation.Path dissolution is an inference mechanism that works naturally with formulas in NNF. Itis strongly complete in the sense that any sequence of link activations will eventually terminate,producing a linkless formula called the full dissolvent. The paths that remain are models of theoriginal formula. Full dissolvents have been used effectively for computing the prime implicantsand implicates of a formula.Decomposable negation normal form was first introduced in 1998 and is currently beingstudied for application to knowledge representation and database systems. A formula in DNNFis a full dissolvent, and it appears that many of the advantages of DNNF exist with full dissolvents.It also appears that a full dissolvent of a formula can be obtained more effciently thana DNNF representation of the formula. The main thrust of this project will be to examine therelationship of DNNF and full dissolvents.

[0229339]在计算机科学中，SAT判定命题逻辑中的公式是否可满足的问题由来已久。它在复杂性理论中很重要，在机器人、光学字符识别、数据库系统、计算机体系结构、电路设计和验证等领域有无数的应用，仅举几例。许多力学定理证明界的传统观点是，自动演绎的有趣应用需要一阶逻辑，而不是命题逻辑。鉴于最近命题逻辑的成功，这种观点已经开始改变。命题逻辑当然是难以处理的（除非NP = P）。知识表示和数据库系统解决这个问题的一种方法是知识编译预处理，这是基础命题理论。其思想是在离线阶段进行尽可能多的计算。然后在线阶段的查询可以快速处理。角子句、有序二元决策图、素数蕴涵/蕴涵集和可分解的负范式（DNNF）都被提出作为这种编译的目标。路径分解是一种自然适用于NNF公式的推理机制。从某种意义上说，它是强完备的，任何链的激活序列最终都会终止，产生一个称为全溶剂的无链公式。剩下的路径是原始公式的模型。全溶剂已被有效地用于计算公式的主隐含式和隐含式。可分解否定范式于1998年首次提出，目前正在研究其在知识表示和数据库系统中的应用。DNNF中的一个公式是一个全溶剂，并且DNNF的许多优点似乎存在于全溶剂中。它还表明，一个公式的完全溶剂可以比该公式的DNNF表示更有效地获得。这个项目的主要目的是研究DNNF和全溶剂的关系。