资 源 简 介
LibModalLogic
LibModalLogic provides a JAVA implementation of Modal Logic K and Propositional Logic. Logic formulas can be build in memory, saved to and read from MathML and formatted human readable. Reasoning is implemented by the (modal) logic tableau algorithm, including dynamic backtracking for maximum performance.
Examples
Construction of formulas works similar to the usage of the OpenGL state machine, and combined with a factory design pattern. E.g. a disjunction of String literals (e.g. A∨B∨¬C) is created in the following way:
```
FormulaFactory factory = new FormulaFactory();
factory.openDisjunction();
factory.literal("A");
factory.literal("B");
factory.negation();
factory.literal("C");
factory.close();
Formula formula = factory.create();
```
For reasoning, the tableau algorithm can be used to find a satisfyin
