기술 요약: 상황 계산법(Situation Calculus)에서의 의무 생성 액션(Obligation-Producing Actions)

문제 정의

본 논문은 상황 계산법 내에서 의무 생성 액션의 맥락에서 발생하는 **프레임 문제(frame problem)**를 다룬다. 레이몬드 라이터(Raymond Reiter)의 기념비적인 연구가 일반적인 액션에 대한 프레임 문제의 해결책(후속 상태 공리 활용)을 제공했고, 셰를과 레베스크(Scherl and Levesque)가 이를 지식 생성 액션으로 확장했지만, 의무 생성 액션에 대한 완전한 프레임워크는 여전히 미비한 상태로 남아 있었다.

구체적으로, 저자들은 데몰롬베 등(Demolombe et al. [6])의 연구에서 발견된 간극을 지적한다. 그들은 상황 계산법에 의무론적 개념을 도입했으나, 이러한 액션들에 대해 추론하거나 명세를 구현할 수 있는 완전한 프레임워크를 개발하지는 못했다. 핵심 과제는 에이전트가 수행하는 액션에 의해 의무를 생성하는 액션(예: 문을 여는 행위는 나중에 문을 잠가야 한다는 의무를 생성함)을 정식화하고, 에이전트가 후속 액션을 수행함에 따라 이러한 의무가 어떻게 지속, 변화 또는 종료되는지를, 영향을 받지 않는 모든 법적 사실들을 일일이 나열하지 않고도 결정하는 것이다.

방법론

저자들은 이전의 공식화에서 사용되었던 상황의 "이상성(ideality)" 순서를 피하고, 라이터의 **기초 액션 이론(Basic Action Theories)**과 데온틱 논리(deontic logic)를 위한 **크립키 스타일의 가능한 세계 의미론(Kripke-style possible-world semantics)**에 기반한 해결책을 제안한다.

1. 정식 프레임워크

이 접근 방식은 액션, 상황, 시점, 객체를 위한 타입(sorts)을 갖춘 시간적 버전의 상황 계산법을 활용한다.

• 의무 플루언트($O$): 이진 관계 $O(s', s)$가 도입되며, 이는 상황 $s'$가 상황 $s$로부터 데온틱적으로 접근 가능하다는 것을 나타낸다.
• 의무 연산자: 의무 $Oblg(\phi, s)$는 접근 가능성 관계에 대한 필연성 연산자로 정의된다: $(\forall s'). O(s', s) \supset \phi[s']$. 이는 $\phi$가 상황 $s$에서 의무적이라는 것은, $\phi$가 모든 데온틱적으로 접근 가능한 상황들에서 성립함을 의미한다.
• 액션 분류: 액션은 의무에 미치는 영향에 따라 세 가지 유형으로 분류된다:
  1. 비의무 생성 액션: 의무를 생성하거나 해제하지 않는 일반적인 액션.
  2. 의무 해제 액션: 기존의 의무를 중단시키는 액션 (예: 문을 잠근 후 매니저에게 알림).
  3. 의무 생성 액션: 새로운 의무를 생성하는 액션 (예: 문을 여는 행위는 문을 잠가야 한다는 의무를 생성함).

2. $O$에 대한 후속 상태 공리(Successor State Axioms)

핵심적인 기술적 기여는 의무 플루언트 $O$에 대한 **후속 상태 공리(SSA)**를 도출하는 것이다. 이 공리는 액션 $a$가 상황 $s$에서 수행된 후, 데온틱적으로 접근 가능한 상황들의 집합이 어떻게 변하는지를 규정한다:

• 비의무 생성 액션의 경우: 현재 상태의 접근 가능한 상황들은 액션 $a$에 의한 이미지(image)로 구성된다.
• 의무 해제 액션의 경우: 이 공리는 의무의 조건(관련 플루언트)이 충족된 접근 가능한 상황들을 필터링하여, 데온틱 공간에서 해당 경로를 효과적으로 제거한다.
• 의무 생성 액션의 경우: 이 공리는 새로 생성된 의무가 충족되는 상황들로 접근 가능한 상황들을 제한한다. 구체적으로, 액션 $a$가 플루언트 $F$에 대한 의무를 생성한다면, 새로운 접근 가능한 상황들은 $F$가 참인 상황들이다.

3. 의무를 위한 회귀(Regression for Obligations)

본 논문은 의무 공식들을 처리하기 위해 라이터의 **회귀 연산자(regression operator)**를 확장한다. 이를 통해 미래 상황에서의 의무 문장의 진릿값을 초기 상황($S_0$)에 대한 추론으로 환원할 수 있다.

• 저자들은 $Oblg$술어를 처리하는 회귀 연산자$R$을 정의한다.
• 이 연산자는 후속 상황에서의 의무를 포함하는 공식들을, 일반 플루언트와 데온틱 플루언트 $O$에 대한 후속 상태 공리를 활용하여 초기 상황에서의 동등한 공식으로 재귀적으로 변환한다.
• **회귀 정리(Regression Theorem)**가 증명되는데, 이는 문장 $W$가 기초 액션 이론에 의해 함의된다는 것은 $W$의 완전히 회귀된 형태가 고유 이름 공리(unique name axioms)와 $O$ 관계의 특정 속성(연쇄성 및 반사성 등)으로 보강된 초기 상황 공리에 의해 함의된다는 것과 동치임을 명시한다.

주요 기여

1. 단순화된 정식화: 본 논문은 상황의 "이상성" 개념을 제거함으로써 접근 가능성 관계의 특징화를 단순화하였으며, 이를 통해 표준 데온틱 논리(Standard Deontic Logic)를 위한 표준 크립키 의미론과 더 밀접하게 일치시켰다.
2. 완전한 액션 이론: 라이터의 프레임워크를 의무 생성 액션까지 포함하도록 확장하는 기초, 전제 조건, 후속 상태, 고유 이름 공리들의 완전한 집합을 제공한다.
3. 정확성 증명: 저자들은 자신들의 정식화가 다음과 같은 직관적인 속성들을 산출함을 증명한다:
   • 생성: 의무 생성 액션을 수행하면 후속 상황에서 상응하는 의무가 생성된다.
   • 지속: 의무는 명시적으로 중단되지 않는 한 후속 상황에서도 지속된다.
   • 종료: 관련 플루언트가 참이 되거나(또는 특정 해제 액션이 수행될 때) 의무가 제거된다.
4. 회귀 확장: 회려 연산자를 의무 영역까지 확장하여, 법적 계약 및 스마트 계약에 대한 자동화된 추론을 가능하게 한다.

결과

본 논문은 제안된 정식화가 의무의 역학을 올바르게 모델링함을 입증한다. 문을 여는 시나리오(문을 열고, 잠그고, 매니저에게 알림)를 사용하는 실행 예제를 통해 저자들은 다음을 보여준다:

• 액션이 수행됨에 따라 접근 가능성 관계 $O$가 어떻게 진화하는지.
• 회귀 연산자가 미래 상황에서의 복잡한 의무 쿼리를 어떻게 성공적으로 검사 가능한 초기 상황의 조건으로 축소하는지.
• 시스템이 "만약 어떤 문장이 상황에서 의무적이라면, 의무가 명시적으로 중단되지 않는 한 후속 상황에서도 의무로 남는다"와 같은 속성을 검증할 수 있음을 보여준다.

의의 및 주장

저자들은 이 연구가 법적 문서 및 스마트 법적 계약의 명세와 자동화된 추론을 위한 엄격한 의미론적 토대를 제공한다고 주장한다. 상황 계산법 내에 의무를 직접 정식화함으로써, 이 접근 방식은 다음과 같은 이점을 가진다:

• 다른 접근 방식(예: 제약 기반 방법)에서 요구되는 추가적인 컴파일 단계가 필요하지 않다.
• 복잡한 액션을 정의하고 법적 합의를 검증하기 위해 GOLOG(상황 계산법 기반 프로그래밍 언어)와 같은 기존 도구를 활용할 수 있다.
• 데온틱 논리에 특화된 프레임 문제의 해결책을 제공하여, 법적 추론 에이전트가 무관한 법적 사실을 실수로 변경하지 않고 권리와 의무의 변화를 추적할 수 있도록 보장한다.

본 논문은 동적이고 분산된 환경에서 법적 계약의 일관성을 형식적으로 검증하고 신뢰할 수 있는 실행을 보장할 수 있는 스마트 법적 계약 구현을 위한 필수적인 단계로 자리매김한다. 향에 과제로는 이 프레임워크를 규범 위반 및 의무 불이행(contrary-to-duty) 의무를 다루도록 확장하는 것이 제시되었다.