带完整公式的多模态逻辑程序设计
Multimodal Logic Programming with Full Formulas
浏览论文内容
中文总结 AI 辅助
本文提出一阶多模态逻辑程序设计系统MMLP，其支持任意公式作为程序与查询，基于带模态原理的希尔伯特系统给出声明语义，采用嵌套证明演算，合一算法控制特征参数作用域，性能优于相关系统。
中文摘要 AI 辅助
本文提出了一种名为MMLP的一阶多模态逻辑程序设计系统。该系统接受任意公式作为程序和查询，不限制任何一方为Horn子句或单独的目标文法。其声明语义由所选的D、T、I、B、4和5模态原理的希尔伯特系统独立给出。执行使用带有模态传播有限文法证书的嵌套证明演算。证书可达性等价于相关的Horn闭包，证书存在性是可判定的，且该演算是无切完备的。对于量化答案计算，我们提出了一种基于权限集的合一算法，该算法控制特征参数的作用域，此算法始终终止，且仅在不存在可允许解时失败。成功运行返回一个本身可允许的合一子，所有可允许解都可通过该合一子分解。计算得到的答案在声明上是正确的，且每个声明上正确的答案都是计算得到的答案的普通输出实例。在证明搜索中，MMLP允许句法聚焦，以及对聚焦答案的公平且完备的枚举。在共同片段上，它表示的答案替换与Nguyen的纯逻辑KDI4s5-MPROLOG完全相同，同时支持严格更大的程序和查询语言。
英文摘要
This paper presents a first-order multimodal logic programming system called MMLP. The system accepts arbitrary formulas as both programs and queries, without restricting either side to Horn clauses or a separate goal grammar. Its declarative semantics is given independently by a Hilbert system for selected D, T, I, B, 4, and 5 modal principles. Execution uses a nested proof calculus with finite grammar certificates for modal propagation. Certificate reachability is equivalent to the associated Horn closure, certificate existence is decidable, and the calculus is cut-free complete. For quantified answer computation, we give a unification algorithm based on permission sets that controls eigenparameter scope. The algorithm always terminates and fails exactly when no admissible solution exists. A successful run returns a unifier that is itself admissible and through which all admissible solutions factor. Computed answers are declaratively correct, and each declaratively correct answer is an ordinary output instance of a computed answer. In proof search, MMLP admits syntactic focalization and a fair and complete enumeration of focused answers. It represents exactly the same answer substitutions as Nguyen's pure logical KDI4s5-MPROLOG on their common fragment, while admitting a strictly larger program and query language.
