基于抽象解释的逻辑程序验证研究

项目名称： 基于抽象解释的逻辑程序验证研究

项目编号： No.60803033

项目类型： 青年科学基金项目

立项/批准年度： 2009

项目学科： 轻工业、手工业

项目作者： 赵岭忠

作者单位： 桂林电子科技大学

项目金额： 20万元

中文摘要： 本项目给出了一种基于抽象解释理论的逻辑程序测试和调试框架，其中测试用例的生成、症状的发现和调试（包括诊断和改错）交叉进行，由同一个错误引发的症状只有一个可引发调试过程的执行，并以此方式避免了对调试过程不必要的调用。本项目首次提出并讨论了考虑用户授权的ASP知识库中子知识库相对于完整知识库的正确性问题。给出了一种多用户情况下ASP知识库管理的方法。在逻辑程序回答集存在性判定方面，根据划分和环的概念，对逻辑程序中与与判断无关的规则进行削减，将该问题转化为判断组成否定圈的规则是否一致的问题。在此基础上提出了一种判定规则是否一致的算法。为了能够在利用ASP求解问题过程中使用现有的以经典逻辑表示的知识，给出了一种把以谓词逻辑公式表示的约束型知识和定义型知识转化为ASP程序或知识库的新方法，并以实例说明了其有效性。把基于ASP的知识表示和推理技术应用于机械装配序列规划，提高了装配规划中信息的重用率。为了提高该方法的规划能力，提出并实现了一种基于ASP的子装配体识别技术。给出了一种基于ASP的WEB服务组合形式化描述和验证方法，将组合性质的验证问题转化为求解逻辑程序的回答集。

中文关键词： 逻辑程序验证；抽象解释；ASP知识库；回答集存在性；基于ASP的问题求解

英文摘要： This project proposes an integrated testing and debugging framework, in which the generation of test cases, discovering symptoms and the debugging (including the diagnosis and correction) of the Program Under Consideration are interleaved in such a way that only one of the symptoms with same-error-source relation between each other will lead to the execution of a debugging procedure. In this way unnecessary calls to the procedure are effectively avoided. This project, at the first time, puts forwards and considers the problem of the correctness of a sub knowledge base (KB) with respect to the whole KB represented by ASP (Answer Set Programs). A method is proposed for managing ASP KBs in a multi-user environment. In judging the existence of answer sets of logic programs, the conception of splitting sets and loop formulas are used to remove rules from a logic program that are irrelevant to the judgment of the existence of answer sets of the program. In this way the original problem is transformed to determine the consistency of the set of rules that form negative circles of a program. An algorithm is proposed to judge the consistency of the rules forming a negative circle. In order to make use of existing knowledge in classic logic in the process of using ASP for problem solving, a method is proposed for translating knowledge in classic logic formulas to an ASP program or ASP KB such that the models of the formulas and the answer sets of the ASP program are in one-to-one correspondence. Constraint knowledge and definition knowledge are distinguished in this paper. An attempt is made to apply ASP based knowledge representation and reasoning methods to Mechanical Assembly Sequence Planning (MASP) problems to improve the information reuse of the process. An ASP based solution to MASP is proposed, where information reuse is enhanced by using IDB of an ASP program. In order to improve the performance of the proposed method for solving large scale problems, an ASP based sub-assembly identification method is also presented. A method for describing and verifying web services composition is also proposed. The main idea of the method is to transform the problem of verifying the property of a services composition into the problem of computing the answer set of a logic program.

英文关键词： Verification of logic programs; Abstract interpretation; ASP knowledge base; Existence of answer sets; ASP-based problem solving