논리적 추론 및 정리 증명

논리적 추론 및 정리 증명은 지식 표현을 위한 형식 논리의 사용과 전제 집합에서 필연적으로 도출되는 결론을 이끌어내는 추론의 자동화와 관련이 있습니다.

Definition

정리 증명은 일반적으로 목표가 도출되거나 모순에 도달할 때까지 건전한 추론 규칙으로 공식을 조작하여, 논리적 공식이 공리 집합에서 도출되는지 여부를 자동적으로 도출하는 것입니다.

Scope

이 주제는 명제 논리 및 1차 논리에서의 추론과 이를 자동화하는 알고리즘을 다룹니다: 명제 논리의 진리표 및 DPLL 기반 만족성 검사, 1차 논리의 단일화 및 해상도 원리, 전향 및 후향 연쇄 추론, 그리고 논리 프로그래밍의 기초. 추론 절차의 건전성, 완전성, 결정성을 다룹니다. 불확실성이나 기본값을 허용하는 추론은 불확실성 하에서의 추론 및 비단조 추론 관련 주제에서 다룹니다.

Core questions

• 결론이 일련의 전제에 의해 함축된다는 것은 무엇을 의미하며, 함축은 기계적으로 어떻게 확인됩니까?
• 단일화와 함께 해상도 원리가 1차 논리에 대한 단일하고 완전한 추론 규칙을 어떻게 제공합니까?
• 전향 및 후향 연쇄 추론은 추론 전략으로서 어떻게 다릅니까?
• 1차 타당성이 준결정적이라는 점을 고려할 때, 자동화된 추론의 한계는 무엇입니까?

Key concepts

• 명제 및 1차 논리
• 함축 및 타당성
• 단일화
• 해상도 및 반박
• DPLL 및 SAT 해결
• 전향 및 후향 연쇄 추론
• 혼 절 및 논리 프로그래밍
• 건전성 및 완전성

Key theories

해상도 원리

Robinson의 해상도는 절에 대한 단일 추론 규칙으로, 단일화와 결합하여 1차 논리에 대해 반박-완전합니다. 즉, 만족할 수 없는 절 집합은 빈 절을 도출함으로써 만족할 수 없음을 보일 수 있습니다.

DPLL 및 명제 만족성

Davis-Putnam 절차와 그 DPLL 개선은 단위 전파 및 순수 리터럴 제거를 통한 체계적인 사례 분할로 명제 만족성을 결정하며, 현대 SAT 해결사의 기초를 형성합니다.

논리 프로그래밍 및 후향 연쇄 추론

1차 논리를 혼 절로 제한하고 목표를 역방향으로 해결하면 논리 프로그래밍이 생성됩니다. 여기서 계산은 증명 탐색이며, 추론 방법과 프로그래밍 패러다임을 모두 제공합니다.

Clinical relevance

자동 정리 증명 및 SAT/SMT 해결은 하드웨어 및 소프트웨어 검증, 프로그램 분석, 계획 및 수학에서 사용되며, Prolog와 같은 논리 프로그래밍 언어는 데이터베이스, 구문 분석 및 규칙 기반 시스템에 후향 연쇄 추론을 적용합니다.

History

Gilmore, Davis 및 Putnam(1960)의 초기 증명 절차는 명제 및 양화 추론을 자동화했으며, Robinson의 해상도 원리(1965)는 1차 추론을 하나의 규칙으로 통합했습니다. 1970년대에는 해상도가 논리 프로그래밍 및 Prolog로 정제되었고, SAT 및 SMT 해결은 나중에 주요 실용 기술로 발전했습니다.

Key figures

• John Alan Robinson
• Martin Davis
• Hilary Putnam
• Robert Kowalski
• Alan Robinson

Seminal works

• robinson1965
• davis1960
• kowalski1979

Frequently asked questions

해상도 원리란 무엇입니까?

해상도는 상보적인 리터럴을 포함하는 두 절을 취하여 나머지를 결합하는 새로운 절을 생성하는 단일 추론 규칙입니다. 단일화와 함께 반복적으로 적용하면 1차 절 집합이 만족할 수 없음을 보일 수 있으며, 이는 반박을 통한 정리 증명의 기초가 됩니다.

자동화된 정리 증명은 종료가 보장됩니까?

명제 논리의 경우 타당성은 결정 가능하므로 절차는 종료됩니다. 완전한 1차 논리의 경우 타당성은 준결정적일 뿐입니다. 완전한 증명기는 유효한 공식을 결국 확인할 수 있지만, 유효하지 않은 공식에서는 영원히 실행될 수 있으므로 일반적으로 종료가 보장되지 않습니다.