Core Concepts
이 논문은 두 변수 논리에 궁극적으로 주기적인 집합을 나타내는 양화사를 추가한 확장된 논리 FO2Pres의 만족 가능성과 유한 만족 가능성이 결정 가능함을 보여준다.
Abstract
이 논문은 두 변수 논리 FO2에 궁극적으로 주기적인 집합을 나타내는 양화사를 추가한 확장된 논리 FO2Pres를 연구한다.
주요 내용은 다음과 같다:
FO2Pres의 만족 가능성과 유한 만족 가능성이 결정 가능함을 보인다. 이를 위해 이른바 "biregular graph 제약 Presburger 정의 가능성" 결과를 이용한다.
FO2Pres 문장의 스펙트럼(모델의 크기 집합)이 Presburger 산술로 정의 가능함을 보인다.
분석 과정에서 "biregular graph" 및 "regular digraph"에 대한 제약 문제를 다룬다. 이들 문제에 대한 Presburger 정의 가능성을 보이는 것이 핵심 기술적 기여이다.
제안된 방법론은 두 변수 논리에 대한 다른 확장들과 정규성 관계, 숲 구조 등을 다룬 기존 연구들과 직교적이다.
Stats
모든 1-유형 π에 대해, GA,π는 완전한 Mπ|←−Mπ-정규 digraph이다.
서로 다른 1-유형 π, π'에 대해, GA,π,π'는 완전한 Lπ'|←−Lπ-biregular graph이다.