模块化系统代数的传播器与求解器

将发表于 LPAR 21 会议论文集。求解复杂问题可能涉及不同知识库和问题求解器的非平凡组合。模块化系统代数是一种知识表示框架，提供了一种以纯语义术语形式化指定此类系统的方法。形式上，该代数的一个表达式定义了一类结构。实践中使用的许多高表达力形式化方法求解模型扩展任务，即在输入中给定一个结构，并在定义的结构类中搜索该结构的扩展（这种做法克服了高表达力逻辑常见的不可判定性问题）。在本文中，我们根据代数中的表达式以及用于原始模块的黑盒传播器或求解器，为复杂模块化系统构建了一个模型扩展任务求解器。为此，我们定义了配备解释机制的传播器的一般概念、代数向传播器的扩展，以及一种惰性冲突驱动学习算法。其结果是一个能够无缝结合来自不同领域的求解技术以生成组合系统求解器的框架。