On the Size Complexity and Decidability of First-Order Progression
Progression, the task of updating a knowledge base to reflect action effects, generally requires second-order logic. Identifying first-order special cases, by restricting either the knowledge base or action effects, has long been a central topic in reasoning about actions. It is known that local-effect, normal, and acyclic actions, three increasingly expressive classes, admit first-order progression. However, a systematic analysis of the size of such progressions, crucial for practical applications, has been missing. In this paper, using the framework of Situation Calculus, we show that under reasonable assumptions, first-order progression for these action classes grows only polynomially. Moreover, we show that when the KB belongs to decidable fragments such as two-variable first-order logic or universal theories with constants, the progression remains within the same fragment, ensuring decidability and practical applicability.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Decidability of Sample Complexity of PAC Learning in finite setting
In this short note we observe that the sample complexity of PAC machine learning of various concepts, including learning the maximum (EMX), can be exactly determined when the support of the probability measures considere…
BIG-bench Machine LearningPAC learningTrakhtenbrot's Theorem in Coq, A Constructive Approach to Finite Model Theory
We study finite first-order satisfiability (FSAT) in the constructive setting of dependent type theory. Employing synthetic accounts of enumerability and decidability, we give a full classification of FSAT depending on t…
RelationVerification of Inconsistency-Aware Knowledge and Action Bases (Extended Version)
Description Logic Knowledge and Action Bases (KABs) have been recently introduced as a mechanism that provides a semantically rich representation of the information on the domain of interest in terms of a DL KB and a set…
Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens
We study finite first-order satisfiability (FSAT) in the constructive setting of dependent type theory. Employing synthetic accounts of enumerability and decidability, we give a full classification of FSAT depending on t…
RelationVerification of Relational Multiagent Systems with Data Types (Extended Version)
We study the extension of relational multiagent systems (RMASs), where agents manipulate full-fledged relational databases, with data types and facets equipped with domain-specific, rigid relations (such as total orders)…