Please help me automate my discrete mathematics homework. Given a valid propositional formula, check if it is an instance of one of Łukasiewicz's axioms. Here's how it works.
A term can be defined inductively as follows:
- Single lower-case letters of the Latin alphabet (
c, etcetera) are terms.
- Given a term
¬ϕ is also a term.
- Given terms
(ϕ→ψ) is also a term.
A formula is itself a term, usually made up of smaller terms. An example of a formula is
Now, these are the three axioms. They are formula templates; some formulae are instances of an axiom. You make an instance by replacing all the variables (the Greek letters) with terms.
Same Greek letters have to be substituted with the same terms. Thus, one instance of the axiom A is
(b→¬c)→(c→(b→¬c)). In this case
ϕ has been substituted with
c. Key to solving problems or making proofs in propositional logic is recognising when formulae are instances of axioms.
Thus, the goal of the program is to take as input a valid formula in string or character array format, and output A, B or C (upper or lower case is fine) if it is an instance of the respective axiom, and do something else (output zero, output nothing, basically do anything except throwing an error) if it is not. The question is code-golf; the shortest code wins!
If you want to stick with printable ascii characters, you can use > for → and ! for ¬: