Horn clause
......... 일차논리 (First-order Predicate Calculus) 에서 사용되는 논리식 중에서 Horn 절 이라고 불리우는 특수한 형태의 절이 있다. Horn 절 은 한 개 이하의 긍정적 논리구 (Positive Literal) 만을 갖는 절을 의미하는데, 긍정적 논리구 (Literal) 는 부정부호가 없는 논리구 를 의미한다. 예를 들면 P, ¬P∨Q, P⇒Q 는 모두 Horn 절 의 형태를 갖고 있다. P⇒Q 문장은 두 개의 긍정적 논리구를 갖고 있는 형태인 것처럼 보이나, 절 형태로 변환할 경우에는 ¬P∨Q 가 되므로 Horn 절이 됨을 알 수 있다. PROLOG 에서 사용되는 문장은 모두 Horn절 형태를 갖고 있다 ............
논리학 특히 명제논리 (Propositional Calculus) 에서 Horn clause 는 다음과 같은 일반적 형태를 가진 명제이다
여기서 and 로 결합된 명제의 갯수는 각자가 좋아하는 대로이며 zero 일수도 있다. 이러한 형태는 보통의 전통적인 논리학 (Logic) 내에서 다시 표현될수 있다. 선언명제 (disjunction) 로서 논리적 조건 (logical condition) 의 보통의 표현은 다음과 동등한 경우이다.
는 다음과 같이 표현된다.
이것은 다음과 같은 일반적인 Horn clause 표현과 동등한것으로 일반화된다.
이러한 형태는 Horn clause 이 연언명제의 일반적형태 (conjunctive normal form) 의 부분집합이라는 것을 보여준다. 즉 conjunctive normal form 에서는 용어중의 한개만 긍적적논리구 (positive literal) 이며 나머지는 부정 (negated) 이다. Horn clause 들은 논리프로그래밍 (logic programming) 에서 기초적인 역할을 하며 구조적논리 (constructive logic) 에서도 중요하다.
first-order resolution 에 의한 정리증명 (Theorem Proving) 에 Horn clauses 이 타당한 것은 두개의 Horn clauses 의 resolution 이 하나의 Horn clause 이라는 것이다. 자동정리증명 (automated theorem proving) 에서 이것은 컴퓨터에서 그 절 (clauses) 들을 표현할때 크게 효율적이 될수있다는 것이다. 사실 PROLOG 는 전적으로 Horn clauses 로 만들어진 프로그래밍 언어이다.
Horn clauses 은 계산복잡도 (Computational Complexity) 에서 매우 중요한데, 그것은 conjunction of Horn clauses 을 참으로 만드는 다양한 변수할당의 집합을 찾는 문제는 P-complete problem 이기 때문이며, 그러한 문제는 때때로 HORNSAT 라고 불린다. 이것은 중심이 되는 비결정 완전 (NP-complete) 문제로 알려진 boolean satisfiability problem 의 P 버전이다.
Horn clause 라는 이름은 1951 년 그 절의 중요성을 최초로 지적해낸 논리학자 Alfred Horn 의 이름에서 따온것이다 ............. (Wikipedia : Horn clause)
term :
PROLOG 논리학 (Logic) 명제논리 (Propositional Logic) 연결사 (Connective) 술어논리 (Predicate Logic) 기호 논리학 (Symbolic Logic) 일차논리 (First-order Predicate Calculus) 전문가시스템 (Expert System) 계산복잡도 이론 (Computational Complexity Theory) 정리증명 (Theorem Proving) 조건명제 (Implication) 비결정 완전 (NP-complete) Horn 절 (Horn clause)
paper :
On sentences which are true of direct unions of algebras : Alfred Horn, Journal of Symbolic Logic, 1951