PDDL公理与最小不动点逻辑等价，突破传统限制。
PDDL Axioms Are Equivalent to Least Fixed Point Logic (Extended Version)
- 将PDDL公理映射为最小不动点逻辑，统一表达能力
- 证明两种公理形式可表达相同查询，超越分层Datalog
- 提出编译方法消除衍生谓词的负向出现，实用性强
PDDL中的公理可视为数据库查询语言（如Datalog）的推广。标准规定公理体中负向出现的谓词仅限于动作直接设定的，不可由其他公理推导。文献中常放宽为要求公理集可分层。本文证明这两种形式均能精确表达最小不动点逻辑的所有查询，因此严格强于分层Datalog。同时，我们提出一种编译方法，可消除公理中衍生谓词的负向出现，补全理论分析。
原文摘要 · Abstract (English)
Axioms are a feature of the Planning Domain Definition Language PDDL that can be considered as a generalization of database query languages such as Datalog. The PDDL standard restricts negative occurrences of predicates in axiom bodies to predicates that are directly set by actions and not derived by axioms. In the literature, authors often deviate from this limitation and only require that the set of axioms is stratifiable. We show that both variants can express exactly the same queries as least fixed point logic. They are thus strictly more expressive than stratified Datalog, which aligns with another restriction on axioms occasionally considered in the planning literature. Complementing this theoretical analysis, we also present a compilation that eliminates negative occurrences of derived predicates from PDDL axioms.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。