경적절

Horn clause

수학 논리 프로그래밍과 논리 프로그래밍에서 Horn 절은 논리 프로그래밍, 형식 명세서 및 모델 이론에 사용하기 위한 유용한 속성을 제공하는 특정한 규칙과 같은 형태의 논리 공식이다. 경적절은 1951년 처음 그 중요성을 지적한 논리학자 알프레드 혼의 이름을 따서 명명되었다.[1]

정의

경음기 조항은 (문자의 분리) 최소한 하나의 양(+)을 가지는 조항이다. 즉, 불순수, 문자 그대로의 조항이다.

반대로, 문자가 하나라도 부정된 문자로 문자를 분리하는 것을 이중 경음절이라고 한다.

정확히 하나의 양의 리터럴을 가진 경음기 절은 확정 절 또는 엄격한 경음기 절이며,[2] 음의 리터럴이 없는 확정 절은 단위 절이며,[3] 변수가 없는 단위 절은 사실이다.[4] 긍정적인 리터럴이 없는 혼 절은 목표 절이다. 리터럴이 없는 빈 절(거짓에 해당하는)은 목표 절이라는 점에 유의한다. 이 세 가지 종류의 혼 절은 다음과 같은 명제적 예에 설명되어 있다.

경음기 유형 절 분리형 함축성형식 로 직관적으로 읽는다.
확정조항 ¬p ∨q qq ... ... ∨ t u u u u u u u ← p q ... ... ∧ t 라고 가정하다
만약 p와 q와 ...와 t가 모두 버텨준다면, 너도 버텨라.
팩트 u u ← true 라고 가정하다
유 holds
목표조항 ¬p ∨q qq ... ... ∨ t 거짓 p p q q ... ... ∧ t 라는 것을 보여주다
p와 q와 ...와 t는 모두[note 1] 지탱하고 있다.

한 절의 모든 변수는 전체 절이 되는 범위와 함께 암묵적으로 보편적으로 정량화된다. 따라서 예를 들면 다음과 같다.

인간(X) 인간(X) 인간(X) 인간(X)

다음을 나타낸다.

∀X(인간(X) ∨ 인간(X) ∨ 인간(X) ∨ 인간(X) )

이는 논리적으로 다음과 같다.

∀X (인간 (X) → 인간 (X) )

의의

경적절은 건설적 논리와 계산적 논리에서 기본적인 역할을 한다. 그들은 1차 분해능에 의해 증명되는 자동화된 정리에서 중요하다. 왜냐하면 두 개의 Horn 절의 분해능은 그 자체로 Horn 절이며, 목표 절과 확정 절의 분해능은 목표 절이기 때문이다. Horn 절의 이러한 특성은 정리를 증명하는 데 더 큰 효율을 가져올 수 있다: 목표 절은 이 정리의 부정이다; 위 표의 목표 절을 참조한다. 직관적으로 prove을 증명하고자 한다면 ¬φ(목표)를 상정하고 그러한 가정이 모순으로 이어지는지를 확인한다. 그렇다면 쳉은 참아야 한다. 이렇게 하면 기계적인 증명 도구는 두 세트(가정 및 (하위) 골격)가 아니라 하나의 공식(가정)만을 유지할 필요가 있다.

Proposal Horn 조항도 계산 복잡성에 관심이 있다. 명제적인 Horn 절의 결합을 진실로 만들기 위해 진실-가치 과제를 찾는 문제를 HONESAT라고 한다. 이 문제는 P-완전하며 선형 시간으로 해결할 수 있다.[5] 제한되지 않은 부울 만족도 문제는 NP 완료 문제라는 점에 유의하십시오.

논리 프로그래밍

경적절은 또한 논리 프로그래밍의 기본이며, 여기서 다음과 같은 함축적 형태로 명확한 절을 작성하는 것이 일반적이다.

(p ∧ q ... … ∧ t) → u

실제로 새로운 목표 조항을 생성하기 위한 명확한 조항이 있는 목표 조항의 해결은 논리 프로그래밍 언어 Prolog의 구현에 사용되는 SLD 해결 추론 규칙의 기초가 된다.

논리 프로그래밍에서, 명확한 조항은 목표 감소 절차로 작용한다. 예를 들어 위에 쓰여진 경음기 절은 다음과 같은 절차로 작용한다.

보여드리려면 p를 보여주고 q와 ...를 보여주고 t를 보여줘라.

이 조항의 역활용을 강조하기 위해 역활용 형식으로 기재하는 경우가 많다.

u (p q ∧ … ∧ t)

프롤로그에서 이것은 다음과 같이 기록된다. 

u :- p, q, ..., t.

로직 프로그래밍에서, 연산 및 질의 평가는 해결되어야 할 문제의 부정을 목표 조항으로 나타냄으로써 수행된다. 예를 들어, 실존적으로 정량화된 양의 문맹의 결합을 푸는 문제는 다음과 같다.

∃X (p q q ∧ … ∧ t)

문제를 부정하고(해결책이 있다는 것을 의미함), 논리적으로 동등한 형태의 목표 조항으로 표현함으로써 다음과 같이 표현된다.

∀X (거짓말 p ∧ q ... … ... t)

프롤로그에서 이것은 다음과 같이 기록된다. 

:- p, q, ..., t.

문제를 해결하는 것은 모순을 도출하는 것으로, 이는 빈 절(또는 "거짓말")으로 표현된다. 문제의 해결은 목표절의 변수에 대한 용어 대체로, 모순의 증거에서 추출할 수 있다. 이런 식으로 사용되는 목표절은 관계형 데이터베이스의 결벽 질의와 유사하며, Horn 절 논리학은 범용 튜링 기계와 계산력이 동등하다.

프롤로그 표기법은 사실 모호하며, 골절이라는 용어도 모호하게 쓰이기도 한다. 목표 조항의 변수는 보편적으로 또는 실존적으로 수량화하여 읽을 수 있으며, "거짓말"을 도출하는 것은 모순을 도출하는 것으로 해석하거나 해결할 문제의 성공적인 해결책을 도출하는 것으로 해석할 수 있다.[further explanation needed]

판 엠덴과 코왈스키(1976)는 로직 프로그래밍의 맥락에서 혼 절의 모델-이론적 특성을 조사했는데, 모든 확정 조항 D의 세트에는 고유한 최소 모델 M이 있음을 보여주었다. 원자 공식 A는 A가 M에서 참인 경우에만 D에 의해 논리적으로 암시된다. 실존적으로 정량화된 양의 리터럴들의 결합으로 대표되는 문제 P는 만약 P가 M에서 사실이라면 D에 의해 논리적으로 암시된다. Horn 절의 최소 모델 의미론은 논리 프로그램의 안정적인 모델 의미론의 기초가 된다.[6]

메모들

  1. ^ 해상도 정리 증명에서처럼, "show φ"과 "assume ¬¬"은 동의어(간접적인 증거)이다; 둘 다 같은 공식인 viz에 해당한다. ¬φ.

참조

  1. ^ Horn, Alfred (1951). "On sentences which are true of direct unions of algebras". Journal of Symbolic Logic. 16 (1): 14–21. doi:10.2307/2268661. JSTOR 2268661.
  2. ^ Makowsky (1987). "Why Horn Formulas Matter in Computer Science: Initial Structures and Generic Examples" (PDF). Journal of Computer and System Sciences. 34 (2–3): 266–292. doi:10.1016/0022-0000(87)90027-4.
  3. ^ Buss, Samuel R. (1998). "An Introduction to Proof Theory". In Samuel R. Buss (ed.). Handbook of Proof Theory. Studies in Logic and the Foundations of Mathematics. Vol. 137. Elsevier B.V. pp. 1–78. doi:10.1016/S0049-237X(98)80016-5. ISBN 978-0-444-89840-1. ISSN 0049-237X.
  4. ^ Lau & Ornaghi (2004). "Specifying Compositional Units for Correct Program Development in Computational Logic". Lecture Notes in Computer Science. 3049: 1–29. doi:10.1007/978-3-540-25951-0_1. ISBN 978-3-540-22152-4.
  5. ^ Dowling, William F.; Gallier, Jean H. (1984). "Linear-time algorithms for testing the satisfiability of propositional Horn formulae". Journal of Logic Programming. 1 (3): 267–284. doi:10.1016/0743-1066(84)90014-1.
  6. ^ van Emden, M. H.; Kowalski, R. A. (1976). "The semantics of predicate logic as a programming language" (PDF). Journal of the ACM. 23 (4): 733–742. CiteSeerX 10.1.1.64.9246. doi:10.1145/321978.321991.