Source-linked AI summary
Inclusion and Exclusion Dependencies in Team Semantics: On Some Logics of Imperfect Information
Pietro Galliani
TL;DR
이 논문은 open formula에 대한 independence logic의 표현력을 규명하는 미해결 문제를 다룬다. game-theoretic semantics를 갖춘 inclusion logic과 exclusion logic을 개발하고, dependence logic과 exclusion logic이 동등한 표현력을 가지며 independence logic에서는 더 폭넓은 dependency 표현이 가능함을 보인다.
문제
open formula에 대한 independence logic의 표현력은 여전히 미해결 문제로 남아 있어, 이를 imperfect information의 logic으로 규명하는 데 한계가 있었다.
방법
first-order logic에 inclusion 및 exclusion dependency atom을 추가하고, 그 결과로 얻어지는 logic들을 연구하며, 이에 대한 game-theoretic semantics를 개발한다.
결과
dependence logic은 team definability와 sentence definability 모두에서 exclusion logic과 정확히 동등한 표현력을 갖는다.
시사점 및 한계
이 결과는 independence logic이 database theory에서 연구되는 일반적인 dependency 형식을 표현하기 위한 이론적 framework를 제공함을 시사한다.
시사점 및 한계
논문은 inclusion logic의 표현적 성질에 대해서는 상대적으로 알려진 바가 적다고 지적한다.
Abstract
from arXiv · showhide
We introduce some new logics of imperfect information by adding atomic formulas corresponding to inclusion and exclusion dependencies to the language of first order logic. The properties of these logics and their relationships with other logics of imperfect information are then studied. Furthermore, a game theoretic semantics for these logics is developed. As a corollary of these results, we characterize the expressive power of independence logic, thus answering an open problem posed in (Grädel and Väänänen, 2010).
1. 서론
이 논문은 inclusion 및 exclusion atom을 일차 논리에 추가하여 불완전 정보 논리에서 나타나는 추가적인 dependency pattern을 연구한다. 이에 대응하는 team semantics와 game semantics 체계를 개발하고, 이를 통해 independence logic의 표현력을 규명한다.
- 동기: 불완전 정보 논리는 일차 논리로는 표현할 수 없는 dependence 및 independence pattern을 다루며, 특수한 atom을 추가하여 언어를 확장한다.Dependence logic은 dependence atom을 통해 functional dependence를 분리해 다루고, independence logic은 y ⊥x z atom을 통해 informational independence를 표현한다.
- 표현력: 결과는 database theory에서 연구된 가장 일반적인 dependency form 중 일부가 independence logic에서 표현 가능함을 보이며, open formula에 대한 independence logic의 표현력과 관련된 open problem에 답한다.서론은 이 표현력 문제가 open problem임을 밝히고, database dependency에 관한 귀결을 최종 결과로 제시한다.
- 기여: 이 논문은 inclusion 및 exclusion dependency를 추가적인 relational constraint로 도입하고, 이에 대응하는 logic을 개발한다.inclusion 및 exclusion logic을 연구하기에 앞서 이들의 정의와 기본 성질을 검토하며, equiextension dependency는 여기서 inclusion dependency와 동등한 것으로 취급한다.
- 기여: Exclusion logic은 강한 의미에서 dependence logic과 동등하며, 새로운 dependency formalism을 기존의 불완전 정보 논리와 연결한다.이 동치성은 논문의 주요 structural result 중 하나로 제시된다.
- Semantics: 이 논문은 team semantics와 함께 inclusion 및 exclusion logic을 위한 game-theoretic semantics를 개발한다.이 semantics는 semantic game을 통해, 대개 winning strategy의 존재를 통해 진리를 부여하며, team semantics는 유용한 보완적 formalism으로 남는다.
2. 의존성과 독립성 논리
의존성 논리는 함수적 의존성을 표현하는 원자를 추가해 일차 논리를 확장하며, team 위에서 해석되고 데이터베이스 이론의 의존성과 밀접하게 대응한다. 이 절에서는 독립성 논리도 소개하고, 논문이 제시하는 열린 표현력 문제의 해답을 정식화한다.
- 의존성 논리: 의존성 논리 는 마지막 항이 앞선 항들에 의해 함수적으로 결정됨을 주장하는 의존성 원자를 추가해 일차 논리를 확장한다.이는 의존성 패턴을 양화와 분리하며, 일차 논리로 표현할 수 없는 의존 관계를 다룰 수 있게 한다.
- 의존성 논리: 팀 의미론에서 팀은 정보 상태를 나타내며, 만족한다는 것은 Verifier가 팀의 모든 할당에서 승리하는 전략을 갖는다는 뜻이다.이 의미론은 IF 논리에 대한 Hodges의 조합적 의미론을 변형한 것이다.
- 의존성 논리: 의존성 원자식의 만족은 팀이 유도하는 관계 위에서의 데이터베이스 의존성 {t1 . . . tn−1} →tn과 동치다.따라서 tn의 값은 t1 . . . tn−1의 값들의 함수다.
- 독립성 논리: 독립성 논리 는 의존성 원자식을 독립성 원자식으로 대체해, 불완전 정보에 대한 별개의 논리를 도입한다.이 절은 이 논리를 독립성 논리로 정의 가능한 팀의 NP 성질을 특성화하는 미해결 문제와 연관지어 위치시킨다.
- 독립성 논리: 이 논문은 새로운 논리에 대한 유사한 결과의 따름정리로서, 독립성 논리로 정의 가능한 팀의 NP 성질을 특성화하는 미해결 문제에 답한다.이 결과는 불완전 정보의 새로운 논리들을 폭넓게 전개한 논문의 귀결로 제시된다.
3. 팀 의미론
Section 3에서는 first-order 및 dependence-related logic에 대한 team semantics를 도입하고, team과 그 relational interpretation, logical operator의 satisfaction rule을 정의한다. 또한 singleton team에서 Tarski semantics와의 일치, first-order formula의 flatness, dependency atom과 대안적 semantic rule이 초래하는 더 높은 expressive complexity를 확립한다.
- 3.1 Team semantics: team은 model 위의 assignment 집합이며, 이에 대한 제약과 관련 relation이 team semantics의 기본 객체를 이룬다.이 절에서는 team을 공통 variable domain을 갖는 assignment 집합으로 정의하고, team에서 relation을 추출하고 assignment를 restriction하기 위한 표기를 도입한다.
- 3.1 Team semantics: 일阶 논리의 team semantics는 pointwise literal, team-splitting disjunction, shared conjunction, supplemented existential quantification, duplicated universal quantification을 사용한다.dependence logic에서는 negation이 semantic operation이 아니므로 공식은 negation normal form이라고 가정한다.
- 3.1 Team semantics: singleton team에서는 일阶 team semantics가 통상적인 Tarski semantics와 일치하고, 임의의 team에서는 모든 assignment에서 성립할 때 정확히 일阶 공식이 성립한다.이는 고전적 semantics와의 일치 및 일阶 공식의 flatness property를 모두 확립한다.
- 3.1 Team semantics: dependency atom은 constancy와 같은 조건이 assignment를 독립적으로 평가하는 대신 여러 assignment를 비교해야 할 수 있으므로 team을 의미론적으로 필수적인 것으로 만든다.이 절에서는 dependence atom을 추가한 결과가 dependence logic임을 밝히고, team satisfaction이 더 이상 singleton satisfaction으로 환원되지 않음을 지적한다.
- 3.1 Team semantics: dependence logic에서 동치인 rule이 새로운 논리에서는 달라질 수 있으므로 disjunction과 existential quantification에 대한 대안적 strict rule을 도입한다. 다만 일阶 논리와 dependence logic에서는 lax semantics와 strict semantics가 일치한다.strict disjunction은 서로소인 subteam을 요구하고, strict existential quantification은 single-valued supplementation을 사용한다.
- 3.2 Constancy logic: constancy logic은 dependence logic에 포함되며, open formula에서는 일阶 논리보다 표현력이 높지만, sentence에서는 일阶 논리와 표현력이 정확히 같으므로 dependence logic보다 엄밀히 약하다.이 절에서는 이들 논리의 표현력 비교에서 sentence 수준과 formula 수준 사이에 차이가 있음도 지적한다.
4. 논리에서의 inclusion과 exclusion
이 절에서는 team semantics 내에서 inclusion, exclusion, equiextension logic을 전개하고, 이들의 의미론적 성질과 표현력 관계를 확립한다. 특정 의미론하에서 exclusion logic이 dependence logic과 일치하고, inclusion/exclusion logic이 independence logic과 일치함을 보인다.
- 동기와 dependency theory: 이 절에서는 확립된 dependency theory를 바탕으로 dependence atom을 다른 database-theoretic dependencies로 대체할 근거를 제시하고, inclusion, exclusion 및 이들의 함의 체계에 대한 soundness와 completeness를 증명한다.저자들은 non-functional dependencies가 지식 상태와 관련된다고 보고, database 결과가 이에 대응하는 logics에 정보를 제공할 것으로 기대한다.
- Inclusion logic: lax semantics를 사용하는 inclusion logic은 local이고 union closed이지만 not downward closed이며, strict semantics에서는 locality가 성립하지 않는다.따라서 strict와 lax disjunction 및 existential quantification 중 무엇을 선택하는지가 inclusion logic에서 본질적이다.
- Inclusion logic: 문장에 대한 inclusion logic의 표현력은 first-order logic보다 엄밀히 크지만, 여전히 independence logic에 proper하게 포함된다.inclusion logic은 finite linear orders에서 parity를 정의할 수 있는데, 이는 first-order logic으로 표현할 수 없는 성질이다. 또한 inclusion atom은 independence logic으로 표현할 수 있다.
- Equiextension logic: inclusion logic과 equiextension logic은 정확히 동일한 표현력을 가지며, 각 논리의 모든 formula는 다른 논리의 formula와 동치이다.먼저 equiextension logic이 inclusion logic에 포함됨을 보이고, 이어서 inclusion atom을 equiextension formula로 변환한다.
- Exclusion logic: exclusion logic은 team의 definability와 문장 모두에서 dependence logic과 정확히 동일한 표현력을 갖는다.dependence atom은 exclusion logic으로 표현할 수 있고, exclusion atom은 dependence-logic formula로 변환할 수 있다.
5. 게임 이론적 의미론
이 절에서는 inclusion/exclusion logic의 게임 이론적 의미론을 전개하며, uniform strategy를 통해 inclusion 및 exclusion atom과 team semantics를 연결한다. lax semantics와의 동치, 그리고 inclusion logic에서는 deterministic strategy 아래 strict semantics와의 동치를 증명하여, nondeterministic/lax semantics가 imperfect-information logic에 자연스러운 선택임을 뒷받침한다.
- 의미론적 게임: 게임은 team의 assignment에서 시작하여 logical connective와 quantifier에 따라 subformula를 거쳐 진행되며, 지정된 조건에서 terminal literal과 dependency atom이 Player II의 승리로 판정된다.Player I과 Player II는 position (ψ,s)을 차지한다. disjunction과 existential quantification은 II가, conjunction과 universal quantification은 I가 통제하며, inclusion 및 exclusion atom은 항상 II에게 국소적으로 승리이다.
- Uniform strategy: Uniformity는 Player II의 strategy를 제한하여 inclusion atom이 다른 호환 가능한 play에서 일치하는 값을 요구하도록 하는 반면, exclusion atom은 관련 play들 사이에서 term value가 서로 다르도록 요구한다.이 atom들은 II에게 국소적으로 승리이지만 허용 가능한 strategy의 집합을 제약한다. inclusion uniformity는 nondeterministic strategy와 deterministic strategy가 다른 이유도 설명한다.
- Team semantics와의 동치: Uniform winning strategy는 inclusion logic에 대한 lax team semantics를 특징짓는다.Theorem 5.10은 Player II가 uniform winning strategy를 가질 조건이 정확히 lax semantics에서 M |=X φ인 조건과 같다고 말한다. inclusion 및 exclusion logic의 game semantics도 이에 따라 제한된다.
- Team semantics와의 동치: Uniform deterministic winning strategy는 inclusion logic에 대한 strict team semantics를 특징짓는다.Theorem 5.11은 deterministic game strategy와 strict semantics 사이의 대응하는 동치를 확립한다.
- 해석적 귀결: Inclusion logic 및 그 확장에서 lax semantics와 strict semantics는 동치가 아니므로, 결과는 nondeterministic, equivalently lax, semantics를 imperfect-information semantics의 자연스러운 의미론으로 채택하는 것을 뒷받침한다.이 구별은 Axiom of Choice가 있어도 유지되지만, 인용된 결과에서 lax semantics는 Locality를 만족한다.
6. I/E logic에서의 정의 가능성 (및 independence logic에서의 정의 가능성)
이 절에서는 I/E logic이 team relation에 대한 existential second-order logic과 정확히 동일한 표현력을 가짐을 보이고, 이 특성화를 independence logic으로 확장한다. 따라서 모든 NP team property가 independence logic으로 표현 가능하며, independence logic은 existential-second-order fragment 안에서 가장 표현력이 높은 imperfect-information logic이다.
- 6. I/E logic에서의 정의 가능성 (및 independence logic에서의 정의 가능성): I/E logic 공식은 team이 나타내는 relation에 대한 existential second-order formula로 변환된다.이 변환은 I/E 공식에 대한 귀납법으로 증명된다.
- 6. I/E logic에서의 정의 가능성 (및 independence logic에서의 정의 가능성): 반대로, 하나의 free relation variable을 갖는 모든 existential second-order formula는 team 위의 I/E logic 공식으로 정의 가능하다.이 구성에서는 existentially quantified function을 dependence condition으로 대체하고, inclusion/exclusion atom을 사용해 team relation의 membership을 부호화한다.
- 6. I/E logic에서의 정의 가능성 (및 independence logic에서의 정의 가능성): I/E logic과 independence logic은 동일한 표현력을 가지므로, 모든 existential second-order team property는 independence logic으로 표현 가능하다.이 결과는 앞선 특성화와 Corollary 4.23에서 직접 따른다.
- 6. I/E logic에서의 정의 가능성 (및 independence logic에서의 정의 가능성): 모든 NP team property는 independence logic으로 표현 가능하다.이는 existential-second-order 특성화와 Fagin’s Theorem [10]에서 따른다.
- 6. I/E logic에서의 정의 가능성 (및 independence logic에서의 정의 가능성): Independence logic, 즉 I/E logic은 그 property가 existential second-order logic 안에 남는 imperfect-information logic 중 가장 표현력이 높다.확장은 existential second order가 아닌 property를 표현하는 경우에만 이 경계를 넘어선다.
7. 동치 생성 의존성, 튜플 생성 의존성 및 independence logic
이 절은 database 이론의 튜플 생성 의존성과 동치 생성 의존성을 dependence atom 및 independence atom과 연결한 뒤, I/E logic이—and 따라서 independence logic이—이러한 모든 의존성을 표현할 수 있음을 보인다. 이러한 표현력은 높은 계산 비용에도 불구하고 knowledge-base reasoning에 independence logic을 활용할 근거를 제공한다.
- Database 의존성: 튜플 생성 의존성은 ∀x1 . . . xn(φ(x1 . . . xn) →∃z1 . . . zkψ(x1 . . . xn, z1 . . . zk))의 형식을 가지며, φ와 ψ는 관계 atom 또는 동치 atom의 conjunction이다.관계 기호 A의 arity는 database 관계 R의 arity와 같고, 항은 empty vocabulary를 사용하며 free variable은 x1 . . . xn 가운데서 선택된다.
- Database 의존성: 동치 생성 의존성은 ψ가 단일 동치 atom이어야 한다는 점에서 다르며, satisfaction은 관계 R 위에서 통상적인 first-order 의미론으로 평가된다.이는 database 이론에서 dependence를 나타내는 두 가지 일반적 개념으로 제시된다.
- Atom 대응: Dependence atom은 동치 생성 의존성에 대응하고, independence atom은 튜플 생성 의존성에 대응한다.이 절은 이러한 대응을 튜플 생성 의존성과 동치 생성 의존성의 표현력을 보여주는 예로 제시한다.
- 표현력: I/E logic은, 결과적으로 independence logic도, 모든 튜플 생성 의존성과 동치 생성 의존성을 표현한다.Proposition 7.1은 이러한 각 의존성이 동등한 I/E-logic formula를 가진다고 진술하며, proof는 Theorem 6.2와 Corollary 4.23을 통해 independence-logic의 표현 가능성을 도출한다.
- 함의: 이러한 표현력은 independence logic이 다양한 database 이론적 성질을 나타내고 일반적인 knowledge-base reasoning을 잠재적으로 지원하게 하지만, 계산 비용은 매우 높다.저자는 이 응용을 independence logic 및 더 일반적으로 imperfect information logic을 연구하는 동기로 제시한다.