This program takes user-inputted lists of formalized sentences and tells you whether the sentences are consistent or form a valid argument in Propositional Modal Logic (S5 Axiom System). The decision procedure for modal formulas is original. (The implementation for the non-modal formulas is based on the pen-and-pencil decision procedure from Richard Jeffrey's 1990 book.) Coded in Python.
This project should especially be considered for Most Polished Hack, since it takes sentences in infix notation and converts them to Polish notation (a prefix notation with letters for logical operators) for easier parsing and manipulating, before returning the result.