Symbolic Logic Mechanization

Polish notation is the prefix symbolic-logic notation developed by Jan Łukasiewicz in 1929. (Because it is prefix notation, postfix notation is called Reverse Polish Notation, or RPN.) In this notation (referred to as PN below), logic operators are written as upper-case letters and logic variables as lower-case letters; each variable is either true or false. Because prefix notation is self-grouping, there is no need for precedence, associativity, or parentheses.

The PN operators and their meanings are:

(The operator J is taken from A. N. Prior's treatment rather than Łukasiewicz's original work.)

For the operators that have no exact C/C++/Java equivalent, the truth tables are (1 = true, 0 = false):

A string of PN operators and variables is a well-formed formula (WFF) if and only if it is a single variable, or a PN operator followed by the required number of operands, each of which is itself a WFF. N takes one operand; C, K, A, D, E, and J each take two.

A string fails to be a WFF if:

• it uses an invalid character — an upper-case letter that is not one of the operators above, or any non-alphabetic character; or
• it has insufficient operands for its operators; or
• it is a valid WFF followed by extraneous text.

For an invalid string, report the first error found in a left-to-right scan. An invalid character is reported as soon as it is reached. However, if a valid WFF is followed by extraneous text, report the extraneous text as the error, even if that trailing text also contains an invalid character.

Every WFF is exactly one of:

• a tautology — true for every assignment of its variables;
• a contradiction — false for every assignment; or
• a contingent expression — true for some assignments and false for others.

For example, p is contingent, KpNp (p and not-p) is a contradiction, ApNp (p or not-p) is a tautology, and EDpqANpNq (one form of De Morgan's law) is a tautology.

Read lines until an empty line is read. Each line contains only alphanumeric characters (no spaces or punctuation) and is to be parsed as a candidate WFF. Each line has fewer than 256 characters and uses at most 10 distinct variables. There are at most 32 non-empty lines before the terminating empty line.

For each input line, echo the line, then state whether it is a valid WFF. If it is valid, also state its category (tautology, contradiction, or contingent). Use exactly this format:

• <line> is valid: <category> for a WFF, or
• <line> is invalid: <reason> otherwise, where <reason> is invalid character, insufficient operands, or extraneous text.

While scanning a line, stop and report it as not a WFF as soon as you reach an unrecognized operator or character (even if it also fails to be well-formed in some other way). If a WFF is followed by extraneous text, report extraneous text; if there are too few operands, report insufficient operands.