Well-formed formula (wff)
well-formed formula (약자로 wff) 는 정합논리식(整合論理式), 판명문, 또는 그냥 논리식 등등으로 불리운다.
우리가 대수연산에서 변수, 상수, 연산자 등을 이용하여 대수식을 구성하는 것과 마찬가지로, 논리연산을 위하여 명제와 연결사 (Connectives) 를 이용하여 논리식(wff) 을 만들 수 있다.
이 때, 명제는 특정명제와 명제변수를 모두 포함한다. 명제변수란 임의의 명제를 지칭하는 것으로서, 정해진 진리값을 갖는 특정명제를 대입하여 진리값을 부여할 수 있다. 명제식은 이러한 명제변수, 연결사 및 괄호로 구성되는 문자열로서, 다음의 규칙에 의거하여 생성되는 정합논리식에 의해 정형화될 수 있다.
(1) 모든 명제변수와 상수(참, 거짓)는 논리식이다.
(2) 만일 A와 B가 논리식이면 다음도 논리식이다.
~A, ~B, (A ∨ B), (A ∧ B), (A → B), (A ↔ B)
(3) 위의 (1), (2) 항을 유한 회 반복 적용하여 만든 식만이 논리식이다.
예) 논리식의 예를 들면 다음과 같다.
(1) P ∨ Q, (P ∧ Q)
(2) (P ∧ Q) ∧ R → S ∧ ~S
(3) (P ↔ Q) ∨ (R ↔~ S) ∧ (~T ↔ R)
단, 실제 사용하는 데 있어 괄호는 편의상 생략할 수 있다. 이 때, 괄호를 생략하더라도 그 논리식의 의미는 바뀌지 말아야 한다.
... 논리 기호를 사용하여 사실을 표기할 수 있는데, 논리 형식론에서는, 수학적 연역 추론 기법을 이용하여 이미 존재하는 사실로부터 새로운 사실을 이끌어낸다........ 이미 참으로 인정된 명제들로부터 새로운 참인 명제를 연역 추론하며 증명하는 이 방법은 단지 수학에서만이 아니라, 문제에 대한 풀이를 얻고자 하는 인공 지능 분야에서도 사용될 수 있다. 정수론이나 기하학과 같은 수학적인 문제를 증명하는 것은 초기 인공 지능 분야의 관심이었으며, 현재에도 여전히 이 분야에서 중추적인 부분이 되고 있다. 그러나 이러한 수학적 기법을 수학의 범위를 벗어나, 일반적인 문제에까지 이용할 수 있다. 어려운 탐색 문제를 제어하기 위해서는, 연역 추론 기법과 경험적으로 얻은 지식의 사용이 필요한데, 이러한 측면에서 볼 때 탐색의 제어 문제와 수학의 여러 복잡한 문제는 서로 다를 바가 없다 ....... 명제 논리는 다루기 쉽고, 또한 이에 대한 결정 과정 (decision procedure) 이 존재하기 때문에 지식을 표기하는데 사용된다. 명제 논리에서의 잘 구성된 공식 (well-formed formulas : wffs) 으로 쓰여진 논리적 명제 형태로 현실 세계의 사실을 표기하는데 ........지식을 표기하는 방법으로 서술 논리가 많이 사용되는데, 이것은 명제 논리로 표기하기에 부적합한 것들을 서술 논리로 적절히 표기할 수 있기 때문이다. 서술 논리에서 현실 세계의 사실은 wff 로 쓰여진 언명 (statement) 으로 표기된다. 그러나 사실을 표기하는데 서술 논리를 사용하는 가장 중요한 이유는 지식의 표기 방법으로 논리적 언명을 사용할 경우 이 지식으로부터의 추론이 가능하기 때문이다 .... (Elaine Rich, 1983)
term :
기호 논리학 (Symbolic Logic) 논리식(wff) 논리학 (Logic) 명제논리 (Propositional Logic) 술어논리 (Predicate Logic) 연결사 (Connective) 인공지능 (Artificial Intelligence) 추론 규칙 (Inference Rule) Prolog
site :
Well-Formed Formula for First Order Predicate Logic--- Syntax Rules
paper :
논리 기호에 의한 사실의 표기 : Elaine Rich