Abstract

I have developed an Automated Theorem Prover for propositional and quantified, classical and non-classical logics. The software implements and adapts the tableaux proof systems theorized / presented by renowned philosopher and logician Graham Priest in his 2008 book "An Introduction to Non-Classical Logic. From If to Is (2nd edition)". I have extended the software with Łukasiewicz’s fuzzy logic by implementing the tableaux proof system of Olivetti. I have also developed an alternative counter-model finder algorithm for first-order normal modal logics. The software is free and open source.