AI 中文总结
研究关联Ciao断言与LPTP定理，提出系统翻译方案，根据逻辑可编码性描述断言类，为不可译情况提策略与构造，分析权衡，实现Ciao断言检查与LPTP演绎验证紧密集成，发挥互补能力。
AI 中文摘要
基于抽象解释的验证是Ciao Prolog系统的核心组件，能对程序、谓词和执行状态的属性进行富有表现力的规范。独立地，LPTP（逻辑编程定理证明）框架提供了一种一阶逻辑形式来表达和证明谓词的属性。本文解决了关联这两个框架的一个基本问题：研究将Ciao断言翻译成LPTP公式，并确定基于断言和基于逻辑的规范之间的部分对应关系。我们引入了一个系统的翻译方案，根据逻辑可编码性对断言类进行了特征描述，为不可翻译的情况提出了近似策略和辅助构造，最后分析了由此产生的稳健性和完整性权衡。我们认为，我们的提议能够将Ciao的断言检查与基于LPTP的演绎验证紧密集成，从而利用它们的互补能力。
英文摘要
Abstract interpretation-based verification is a central component of the Ciao Prolog system, enabling expressive specifications of properties of programs, predicates, and execution states. Independently, the LPTP (Logic Programming Theorem Proving) framework offers a first-order logical formalism for expressing and proving properties of predicates. In this paper, we address a fundamental issue in relating these two frameworks: studying the translation of Ciao assertions into LPTP formulae and identifying a partial correspondence between assertion-based and logic-based specifications. We introduce a systematic translation scheme, characterize assertion classes according to their logical encodability, and propose approximation strategies and auxiliary constructs for non-translatable cases, and finally analyze the resulting soundness and completeness trade-offs. We argue that our proposal enables a tight integration of Ciao's assertion checking with LPTP-based deductive verification, thereby leveraging their complementary capabilities.
CommentsIn Proceedings ICLP 2026, arXiv:2607.17707
Journal refEPTCS 450, 2026, pp. 223-235
