Core Concepts
MAV 논리의 모든 증명은 컷 규칙과 다른 "비분석적" 규칙을 피하는 정규 형태로 축소될 수 있다.
Abstract
이 논문은 MAV 논리의 의미론적 모델과 정규화 증명을 제시한다.
MAV 논리는 선형 논리의 곱셈-덧셈 논리에 자기 이중 비가환 연산자를 추가한 논리이다. MAV 논리는 또한 덧셈 연산자가 추가된 BV 논리의 확장이다.
MAV 논리와 BV 논리는 깊이 추론 시스템으로, 추론 규칙을 구조 내부 어디에서나 적용할 수 있다. 이러한 깊이 추론 시스템에서 핵심 문제는 컷 제거 속성, 즉 원래 목표에 없던 구조를 도입하지 않고 증명을 정규 형태로 축소할 수 있는지 여부이다.
기존 연구에서는 복잡한 구문론적 추론과 종료 척도를 사용하여 BV, MAV 등의 깊이 추론 시스템에 대한 컷 제거를 증명했다.
이 논문에서는 의미론적 기법을 사용하여 MAV 증명의 정규화를 유도한다. MAV-대수와 MAV-프레임을 정의하고, MAV-프레임에서 MAV-대수를 구축하는 절차를 제시한다.
이를 통해 MAV의 모든 증명이 정규 증명으로 축소될 수 있음을 보인다. 또한 이 결과는 MAV 논리의 완전성을 보장한다.
저자들은 이 증명을 Agda 증명 보조기에서 기계화하였으며, 이를 통해 증명의 정확성을 검증하고 증명을 실행 가능한 프로그램으로 산출하였다.
Stats
MAV 논리는 선형 논리의 곱셈-덧셈 논리에 자기 이중 비가환 연산자를 추가한 논리이다.
MAV 논리는 BV 논리에 덧셈 연산자를 추가한 확장이다.
MAV 논리와 BV 논리는 깊이 추론 시스템으로, 추론 규칙을 구조 내부 어디에서나 적용할 수 있다.
컷 제거 속성은 깊이 추론 시스템에서 중요한 메타이론적 성질이다.
Quotes
"MAV 논리의 모든 증명은 컷 규칙과 다른 '비분석적' 규칙을 피하는 정규 형태로 축소될 수 있다."
"이 논문에서는 의미론적 기법을 사용하여 MAV 증명의 정규화를 유도한다."