Build a Propositional Logic Theorem Prover

This challenge asks you to build a simple theorem prover for propositional logic in Python. You will implement a system that can determine whether a given propositional logic formula is a tautology (always true) using the truth-table method. This is a fundamental task in formal logic and artificial intelligence, with applications in areas like automated reasoning and verification.

Problem Description

Your task is to create a Python function, is_tautology(formula), that takes a propositional logic formula as a string and returns True if the formula is a tautology, and False otherwise.

A propositional logic formula is composed of:

• Propositional variables: Single uppercase letters (e.g., 'P', 'Q', 'R').
• Logical connectives:
  • Negation: ~ (e.g., ~P)
  • Conjunction: & (e.g., P & Q)
  • Disjunction: | (e.g., P | Q)
  • Implication: > (e.g., P > Q)
  • Biconditional: <> (e.g., P <> Q)
• Parentheses: () for grouping.

The is_tautology function should:

1. Parse the input formula: Convert the string representation into an internal, evaluable structure.
2. Identify all propositional variables: Extract all unique propositional variables present in the formula.
3. Generate all possible truth assignments: For n unique variables, there are 2^n possible combinations of truth values (True/False).
4. Evaluate the formula for each truth assignment: Substitute the truth values of the variables into the formula and compute its truth value.
5. Check for tautology: If the formula evaluates to True for all possible truth assignments, it is a tautology. Otherwise, it is not.

Key Requirements:

• Robust Parsing: The parser should handle nested parentheses and the order of operations correctly.
• Evaluation Logic: Implement the truth values for each logical connective.
• Truth Table Generation: Systematically generate all truth assignments.
• Clear Output: Return a boolean value.

Expected Behavior:

The function should correctly identify tautologies and non-tautologies. For example:

• P | ~P should be True.
• P & Q should be False.
• (P > Q) > ((Q > R) > (P > R)) should be True.

Edge Cases to Consider:

• Formulas with no variables (e.g., tautologies like True if we were to allow it, or contradictions). For this challenge, assume formulas will contain variables.
• Formulas with a single variable.
• Complex nested formulas.
• Formulas with only one type of connective.

Examples

Example 1:

Input: "P | ~P"
Output: True
Explanation: This is a tautology (Law of Excluded Middle). For P=True, True | ~True = True | False = True. For P=False, False | ~False = False | True = True. Since it's true for all assignments, it's a tautology.

Example 2:

Input: "P & Q"
Output: False
Explanation: This is not a tautology. If P=True and Q=False, the formula evaluates to True & False = False.

Example 3:

Input: "(P > Q) > ((Q > R) > (P > R))"
Output: True
Explanation: This is a tautology representing the transitivity of implication. It holds true for all possible truth assignments of P, Q, and R.

Example 4: (Edge Case - Single Variable)

Input: "~~P <> P"
Output: True
Explanation: This formula states that double negation is equivalent to the original proposition. It holds true for both P=True and P=False.

Constraints

• Formulas will be strings consisting of uppercase letters (A-Z), ~, &, |, >, <, (, ).
• The maximum number of unique propositional variables in a formula will not exceed 10.
• The maximum length of a formula string will not exceed 200 characters.
• The parsing and evaluation should be reasonably efficient, avoiding brute-force enumeration that is exponentially worse than necessary.

Notes

• You will need to implement a way to parse the string formula into a structure that can be evaluated. An Abstract Syntax Tree (AST) is a common and effective approach.
• Consider the standard order of operations: ~ (highest precedence), then &, then |, then >, and <>. Parentheses override this order.
• A good starting point for parsing might be a recursive descent parser or using Python's eval in a carefully sandboxed manner (though implementing your own parser is more educational).
• Remember that Python's boolean operators (and, or, not, ==, !=) can be mapped to your logical connectives. You might define a helper function for evaluating sub-expressions.