직관주의 양상 논리(Intuitionistic modal logic, IML)는 스테이징을 위한 양상 타입 시스템, 계산 효과(computational effects), 언어 기반 보안 등 프로그래밍 언어의 여러 발전을 촉발했습니다. IML은 일반적으로 Kripke 스타일 관계 의미론(Kripke-style relational semantics)을 사용하여 연구되는데, 이는 모델을 쉽게 구성할 수 있게 함으로써 완전성(completeness) 및 일관성(consistency)과 같은 메타 이론적 속성의 증명을 단순화합니다. 하지만 Kripke 스타일 관계 의미론은 고전적 추론 원리(classical reasoning principles)에 의존하기 때문에 계산적인 관점에서는 매력적이지 않고 구성적 타입 이론(constructive type theory)에서의 형식화에 부적합합니다. Goldblatt은 직관주의 명제 논리(intuitionistic propositional logic)의 Beth-Kripke-Joyal 스타일 '커버' 의미론을 관계(relations)로 확장하여 IML을 위한 대안적인 의미론을 제공합니다. Goldblatt의 '관계 커버'(relational cover) 의미론은 고전적 추론을 극복하지만, 새로운 제한 사항을 도입합니다: 이는 모델의 범위를 제한하고 모델 구성을 복잡하게 만드는 '양상 국소화(modal localization)' 조건에 의존한다는 것입니다. Goldblatt은 정교한 순서 이론적 완성 논증(order-theoretic completion arguments)을 사용하여 완전성을 증명함으로써 이 제한 사항을 우회합니다. 본 논문에서는 이러한 제한 사항을 완화하고 더 간단하며 표준적인 모델 구성 기법에 적용 가능한 관계 커버 의미론의 보수적 확장(conservative extension)을 제시합니다. 우리는 Agda에서 우리의 의미론을 형식화하고, 독립적인 박스($ox$) 및 다이아몬드 ($ riangle$) 양상을 특징으로 하는 다양한 IML에 대해 정상화 대 평가(Normalization by Evaluation) 스타일로 구성적으로 완전성을 증명합니다.