Core Concepts
약한 K4와 차이 논리는 Craig 보간 속성을 가지지 않는다. 이 논문에서는 주어진 함축이 이러한 논리에서 보간자를 가지는지 여부를 결정하는 문제를 다룬다.
Abstract
이 논문은 약한 K4와 차이 논리에서 보간자 존재 문제를 다룬다.
약한 K4는 모달 논리 K에 33p → (p ∨ 3p) 공리를 추가하여 얻어진다. 차이 논리 DL은 약한 K4에 p → 23p 브루워 공리를 추가하여 얻어진다.
약한 K4와 DL은 Craig 보간 속성을 가지지 않는다. 즉, 이 논리들에서 유효한 함축 ϕ → ψ에 대해 공통 변수로 구성된 보간자 ι가 항상 존재하지는 않는다.
이 논문에서는 주어진 ϕ와 ψ에 대해 ϕ → ψ가 약한 K4와 DL에서 보간자를 가지는지 여부를 결정하는 문제를 다룬다.
약한 K4의 경우, 보간자 부재를 다항식 크기의 쌍대 모델로 증명할 수 있으며, 이를 통해 보간자 존재 문제가 coN3ExpTime에서 결정 가능함을 보인다. 또한 이 문제가 coNExpTime-hard임을 보인다.
차이 논리 DL의 경우, 보간자 부재를 다항식 크기의 쌍대 모델로 증명할 수 있으며, 이를 통해 보간자 존재 문제가 coNP-complete임을 보인다.
Stats
약한 K4 프레임 F = (W, R)은 모든 x, y, z ∈ W에 대해 xRyRz → (x = z) ∨ xRz를 만족한다.
차이 논리 DL 프레임 F = (W, R)은 대칭적이고 약하게 추이적이다.
Quotes
"약한 K4와 차이 논리 DL은 Craig 보간 속성을 가지지 않는다."
"우리의 관심사는 이러한 논리에서 주어진 함축이 보간자를 가지는지 여부를 결정하는 문제이다."