BSc Project: Decision procedures for the modal logic ALT

ALT is the modal logic whose tautologies are precisely the formulas which are valid in all frames whose accessibility relations are partial functions. In temporal reasoning its modal operator can be used to model the properties of `tomorrow' or `next'. It is known that ALT has the same computational complexity as propositional logic (coNP-complete). So, ALT is a fragment of standard temporal logic (LTL) of reasonable computational complexity. The objective of this project is to implement two decision procedures for ALT in the programming language JAVA and compare the performance of the resulting systems. (Lot's of decision procedures for ALT are known. It is not the objective of this project to design a new procedure.)