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.

📋 한 줄 요약

**[지식 표현 · 행위 추론]** 일반적으로 2차 논리가 필요한 progression 문제에서 local-effect / normal / acyclic 액션 클래스의 1차 progression이 다항 크기로 유지되며 결정 가능 단편 안에 머무름을 증명한다.

🎯 핵심 기여도

Situation Calculus 틀에서 1차 progression이 가능한 세 가지 액션 클래스의 크기 복잡도를 체계적으로 분석
합리적 가정 아래 이들 클래스의 1차 progression이 다항 크기로 성장함을 증명
지식 베이스가 2변수 1차 논리나 상수를 포함한 보편 이론 같은 결정 가능 단편에 속할 때 progression이 같은 단편 안에 머묾을 보임
결정 가능성과 실용적 적용 가능성을 동시에 확보

💡 핵심 아이디어

progression의 표현력은 일반적으로 2차 논리를 요구하지만, 액션 효과의 구조적 제약(local-effect / normal / acyclic)과 KB의 결정 가능 단편을 동시에 활용하면 크기와 결정 가능성을 동시에 통제할 수 있다.

🔬 기술적 접근법

**모델/방법론**: Situation Calculus 기반의 1차 progression 분석
**핵심 기법**: 세 가지 액션 클래스에 대한 다항 크기 상한 증명과 2변수 1차 논리·보편 이론에 대한 단편 보존성 증명

📊 주요 결과

세 가지 액션 클래스 모두에서 1차 progression이 다항 크기로 유지됨을 증명
KB가 결정 가능 단편이면 progression 결과도 같은 단편에 속함
결과적으로 결정 가능성과 실용성 동시 확보

💭 의의 및 한계

**의의**: 행위 추론에서 progression을 실용적으로 사용하기 위한 이론적 기반을 제공하며 크기 폭증 위험을 정량적으로 차단한다. **한계**: 분석 대상이 local-effect / normal / acyclic 액션 클래스에 한정되며, 더 표현력 있는 액션 효과로의 일반화는 후속 과제로 남는다.

🚀 실용적 활용

결정 가능한 행위 추론 시스템(로봇 계획, 워크플로 진화) 설계
시간에 따라 변하는 지식 베이스의 실시간 업데이트 모듈
결정 가능 단편을 활용한 형식적 검증 도구