기호 논리 기계화

폴란드 표기법(Polish notation)은 얀 우카시에비치(Jan Łukasiewicz)가 1929년에 고안한 전위(prefix) 기호 논리 표기법입니다. (전위 표기법이므로, 후위 표기법은 역폴란드 표기법(Reverse Polish Notation, RPN)이라고 부릅니다.) 이 표기법(아래에서는 PN이라고 부릅니다)에서는 논리 연산자를 대문자로, 논리 변수를 소문자로 씁니다. 각 변수는 참 또는 거짓 중 하나의 값을 가집니다. 전위 표기법은 그 자체로 그룹이 나누어지므로 우선순위, 결합 법칙, 괄호가 필요하지 않습니다.

PN 연산자와 그 의미는 다음과 같습니다.

(연산자 J는 우카시에비치의 원래 연구에는 없고 A. N. Prior의 정리에서 가져온 것입니다.)

C/C++/Java에 정확히 대응하는 연산자가 없는 경우의 진리표는 다음과 같습니다 (1 = 참, 0 = 거짓).

PN 연산자와 변수로 이루어진 문자열이 올바른 논리식(WFF, well-formed formula) 이 되는 필요충분조건은, 그것이 하나의 변수이거나, 또는 하나의 PN 연산자 뒤에 필요한 개수만큼의 피연산자(각각이 다시 WFF)가 오는 경우입니다. N은 피연산자를 1개, C, K, A, D, E, J는 각각 2개를 받습니다.

다음 중 하나에 해당하면 문자열은 WFF가 아닙니다.

• 잘못된 문자(invalid character) 를 사용한 경우 — 위 표에 없는 대문자이거나, 알파벧이 아닌 문자.
• 연산자에 대해 피연산자가 부족한(insufficient operands) 경우.
• 올바른 WFF 뒤에 불필요한 텍스트(extraneous text) 가 붙은 경우.

WFF가 아닌 경우, 왼쪽에서 오른쪽으로 훑을 때 가장 먼저 발견되는 오류를 보고합니다. 잘못된 문자는 만나는 즉시 보고합니다. 다만 올바른 WFF 뒤에 불필요한 텍스트가 붙어 있으면, 그 뒤쪽 텍스트에 잘못된 문자가 있더라도 불필요한 텍스트를 오류로 보고합니다.

모든 WFF는 다음 중 정확히 하나입니다.

• 항진식(tautology) — 변수의 모든 값 조합에 대해 참.
• 모순식(contradiction) — 모든 값 조합에 대해 거짓.
• 가변식(contingent) — 어떤 조합에서는 참, 다른 조합에서는 거짓.

예를 들어 p는 가변식, KpNp(p 그리고 not-p)는 모순식, ApNp(p 또는 not-p)는 항진식, EDpqANpNq(드모르간 법칙의 한 형태)는 항진식입니다.

빈 줄을 읽을 때까지 여러 줄을 입력받습니다. 각 줄은 공백이나 문장 부호 없이 영문자와 숫자로만 이루어지며, WFF 후보로 파싱됩니다. 각 줄의 길이는 256자 미만이고, 서로 다른 변수를 최대 10개까지 사용합니다. 종료를 알리는 빈 줄 앞에는 비어 있지 않은 줄이 최대 32개까지 있습니다.

각 입력 줄에 대해, 먼저 그 줄을 그대로 다시 출력한 뒤 그것이 올바른 WFF인지 표시합니다. 올바른 WFF이면 그 분류(tautology, contradiction, contingent)도 함께 출력합니다. 형식은 정확히 다음과 같습니다.

• WFF인 경우: <줄> is valid: <분류>
• 아닌 경우: <줄> is invalid: <사유> (<사유>는 invalid character, insufficient operands, extraneous text 중 하나)

한 줄을 훑는 도중 인식할 수 없는 연산자나 문자를 만나면(다른 이유로도 WFF가 아니더라도) 즉시 WFF가 아니라고 보고합니다. WFF 뒤에 불필요한 텍스트가 있으면 extraneous text를, 피연산자가 부족하면 insufficient operands를 보고합니다.