An automated theorem prover on first order modal logic, fuzzy logic and other non-classical logics, written in Rust. Implements the algorithm theorized by renowned philosopher and logician Graham Priest in his 2008 book "An Introduction to Non-Classical Logic. From If to Is (second edition)".
| Chapter | Status | |
|---|---|---|
| 1 | Classical logic | ✅ Propositional logic fully implemented. |
| 2 | Basic modal logic | ✅ K modal logic fully implemented. |
| 3 | Normal modal logics | ✅ T,B,S4,S5 modal logics fully implemented. K tense modal logic partially implemented: for temporal convergence rule, multiple graphs per problem are needed, right now there is a single graph per problem. |
| 4 | Non-normal modal logics | ✅ S0.5,N,S2,S3,S3.5 modal logics fully implemented. |
| 5 | Conditional logics | ✅ C fully implemented. C+ partially implemented, multiple graphs per problem are needed. |
| 6 | Intuitionist logic | ✅ Fully implemented. |
| 7 | Many-valued logics | ✅ Skip, no tableaux on this chapter. |
| 8 | First degree entailment | ✅ Regular FDE fully implemented. Routley star FDE variant not implemented. |
| 9 | Logics with gaps, gluts and worlds | ✅ K4,N4,I4,I3,W logics fully implemented. |
| 10 | Relevant logics | ❌ Skip, this is really difficult to implement. |
| 11 | Fuzzy logics | ✅ Lukasiewicz fuzzy logic fully implemented based on this article, although the book does not provide a tableaux method on this chapter. |
| 11a | Many-valued modal logics | ✅ Lukasiewicz logic, Kleene logic, Logic of Paradox, RMingle3 logic fully implemented. |
| 12 | Classical first-order logic | ✅ Fully implemented. |
| 13 | Free logics | ✅ Implemented only with negativity constraint. Positive free logic is not implemented. |
| 14 | Constant domain modal logics | ✅ Fully implemented. |
| 15 | Variable domain modal logics | ✅ Implemented only with negativity constraint. |
| 16 | Necessary identity in modal logic | ✅ Fully implemented. |
| 17 | Contingent identity in modal logic | ✅ Fully implemented. |
| 18 | Non-normal modal logics | ✅ Fully implemented. |
| 19 | Conditional logics | ✅ C fully implemented. C+ partially implemented. |
| 20 | Intuitionist logic | ✅ First kind of tableaux implemented. Second kind of tableaux not implemented. |
| 21 | Many-valued logics | ✅ Fully implemented. |
| 22 | First degree entailment | ✅ Fully implemented. |
| 23 | Logics with gaps, gluts and worlds | ✅ Fully implemented. |
| 24 | Relevant logics | ❌ Skip, this is really difficult to implement. |
| 25 | Fuzzy logics | ✅ Fully implemented. |