A Strategy Language for Controlled Proof Search

기술 요약: 제어된 증명 탐색을 위한 전략 언어

문제 정의
자동 추론(automated reasoning)에서 논리적 계산법의 정적 완전성(임의의 정리에 대해 증명이 존재함)이 증명기(prover)의 동적 완전성(실제로 그 증명을 찾아내는 능력)을 보장하지는 않는다. 반결정적(semi-decidable) 논리에서 추론 규칙은 무한히 많은 후속 상태를 생성할 수 있다. 만약 증명 탐색 전략이 편향된 탐색(예: 특정 브랜치를 무한히 우선시하는 단순 깊이 우선 탐사 방식)을 채택한다면, 관련 추론을 영원히 미루게 되어 유효한 증명이 존재함에도 불구하고 이를 발견하지 못할 수 있다. 이러한 문제는 추론 규칙과 증명 탐색 전략을 분리하는 Pgeon과 같은 프레임워크에서 특히 중요하며, 탐색 정책의 설계가 성공 여부를 결정짓는 핵심 요소가 된다.

방법론
본 논문은 선언적 논리 계산법의 명세를 실행 가능한 증명기로 컴파일하는 메타 증명기 프레임워크인 Pgeon을 위한 정식 전략 언어를 소개한다. 핵심적인 방법론적 변화는 증명 탐색을 상태 간의 관계로 모델링하는 것이 아니라, 스트림(stream)을 통한 증명 상태의 열거로 모델링하는 것이다.

1. 형식적 의미론: 증명 상태($\Sigma$)는 부분적으로 구성된 증명 트리의 역할을 한다. 전략은 상태 $\Sigma$에서 후속 상태들의 스트림(유한 또는 무한)으로 매핑되는 함수 $s: \Sigma \to \text{Str}(\Sigma)$로 정의된다. 이를 통해 비결정성을 명시적으로 표현한다:

   • 빈 스트림은 실패를 나타낸다.
   • 단일 요소 스트림은 결정론적 성공을 나타낸다.
   • 여러 요소를 가진 스트림은 비결정적 분기를 나타낸다.
   • 무한 스트림은 무제한의 후속 상태를 생성할 수 있는 규칙을 나타낸다.

2. 조합자(Combinators): 이 언어는 이러한 전략들을 합성하기 위한 일련의 연산자를 제공하며, 편향된(깊이 우선) 탐색과 공정한(인터리빙) 탐색을 구분한다:

   • 순차 합성 ($;$): 다른 전략의 결과에 하나의 전략을 적용한다.
   • 좌편향 선택 ($\parallel$): 첫 번째 전략을 시도하며, 만약 실패(빈 스트림)할 경우 두 번째 전략으로 회귀한다.
   • 공정 순차 합성 ($\&;$): 대각선 논법($\triangle$)을 사용하여 순차적 적용의 결과들을 인터리빙함으로써, 결과가 유한한 단계 내에 도달 가능하다면 반드시 탐색되도록 보장한다.
   • 공정 선택 ($\&|$): 두 가지 대안적 전략의 결과를 공정하게 인터리빙한다.
   • 반복 ($*$): 공정 순차 합성($\mu X. \text{id} \&; (s \&; X)$)을 최소 고정점(least fixpoint)으로 정의하여, 모든 유한 반복 깊이가 엄격한 깊이 우선 방식이 아닌 방식으로 탐색되도록 보장한다.

3. 기본 연산: 언어에는 기본 규칙($r$)과 모든 허용 가능한 매칭에 규칙을 적용하는 완전 적용 연산자($r!$)가 포함된다.

주요 기여

• 합성 가능한 스트림 의미론: 본 논문은 탐색 공간이 제1급 객체(스트림)로 구체화되는 전략 조합자의 합성 가능한 대수를 제공한다. 이를 통해 스택 규율이나 컨티뉴에이션과 같은 구현 세부 사항과 독립적으로 공정성과 열거에 대해 추론할 수 있다.
• 공정성 메커니즘: 대각선 기반의 인터리빙 연산자($\&;$ 및 $\&|$)를 도입함으로써, 무한한 브랜치가 유한한 증명의 발견을 방해하는 "기아(starvation)" 문제를 해결한다.
• Pgeon을 위한 정식 전략 언어: 본 연구는 Pgeon 프레임워크의 전략 구성 요소를 정형화하여, 증명 탐색의 제어 흐름을 선언적 언어로 추상화한다.

결과 및 사례 연구
본 논문은 다음 두 가지 사례 연구를 통해 접근 방식의 표현력과 효과를 입증한다:

1. 1차 논리 (LK): 저자들은 폐쇄(closure, unification)와 규칙 포화(rule saturation) 사이의 상호작용을 다룬다. 단순한 반복 규칙 적용 전략은 특정 인스턴스화를 너무 일찍 확정해 버리기 때문에 증명을 찾는 데 실패하는 경우가 많다. 제안된 전략 $(\odot^* \&; (\alpha \parallel \delta \parallel \beta \parallel \gamma!)^*)^*$는 공정 합성을 사용하여 폐쇄 시도와 규칙 포화를 인터리빙한다. 이는 서로 다른 유니피케이션 선택들이 모든 탐색 깊이에 걸쳐 탐색되도록 보장하여, 시스템이 유한한 유도 과정을 놓치면서 무한한 인스턴스화 루프에 빠지는 것을 방지한다.

2. 양상 논리 (S4): S4에서는 S4 규칙 적용을 가능하게 하기 위해 임의로 공식을 제거하는 비결정적 규칙 $\theta$가 필요하지만, 이는 폐쇄에 필요한 공식을 버릴 위험이 있다. 통제되지 않은 $\theta$의 사용은 막다른 길(dead end)로 이어진다. 저자들은 $\theta^* \&; \text{S4}$라는 결합 전략을 제안하여, S4 적용을 가능하게 하는 모든 공식 제거 방식을 공정하게 탐색한다. 이는 더 큰 전략 $((\alpha \parallel \beta \parallel T)^*; (\theta^* \&; \text{S4}))^*$에 통합되어, 만약 S4의 성공적인 적용이 특정 부분 집합의 공식 제거를 요구하더라도 기아 현상 없이 해당 구성에 도달할 수 있도록 보장한다.

의의
본 논문은 이 접근 방식이 증명 탐색 절차를 명세하고 분석하기 위한 원칙적이고 모듈화된 기반을 제공한다고 주장한다. 증명 규칙과 탐색 전략을 분리하고 합성 가능한 의미론을 가진 정식 언어를 제공함으로써, 프레임워크는 반결정적 논리에서의 탐색 공간을 체계적으로 탐색할 수 있게 한다. 이는 단순한 깊이 우선 전략이 실패하는 상황에서도 스트림 인터리빙을 통해 공정성을 명시적으로 관리함으로써 동적 완전성을 달로할 수 있음을 보여준다. 본 연구는 특정 증명기의 구현과 독립적으로 추상적인 수준에서 증명 탐색 절차를 추론할 수 있게 한다.