带惩罚的溯因逻辑程序：语义、复杂性与实现

溯因（Abduction）最初在经典逻辑背景下提出，近年在逻辑编程领域受到日益增长的研究关注。本文研究逻辑编程框架中带惩罚的溯因。这种此前未在逻辑编程中分析过的溯因推理形式，可非常自然地表示若干相关问题，包括优化问题。我们定义了逻辑程序上带惩罚溯因的形式化模型，其扩展了 Kakas 与 Mancarella 提出的溯因框架。我们探讨知识表示问题，在我们的溯因框架中对若干问题进行了编码。特别地，我们考虑来自不同领域的一些相关问题，涵盖从优化理论到诊断与规划；它们的编码在我们的形式化中显得简洁优雅。我们深入分析了逻辑程序中带惩罚溯因所引发主要问题的计算复杂性。最后，我们在 DLV 引擎之上实现了一个支持所提溯因框架的系统。为此，我们设计了一种从带惩罚溯因问题到带弱约束逻辑程序的转换。我们证明该方法是可靠且完备的。