LoTREC is an automated theorem prover for modal and description logic. It allows students and researchers in logic to define well-known and new exotic logics with Kripke's semantics, and to check the properties of their formulas, i.e. their satisfiability or validity, as well as performing model checking.
The syntax of a logic is defined by providing a set of connectors names and syntactical rules, and the sematincs of the logic is defined by providing a set of graph rewriting rules. A formula can be then automatically tested with LoTREC, which applies the graph rewriting rules in order to decompose and analyze the formula.
To run LoTREC, download "LoTREC-distribution.zip", extract it and execute the "run.bat" file. In case the execution does not succeed, please refer to the "README.txt" that can be found besides the "run.bat" file.
Alternatively, fork then checkout LoTREC's code base from a NetBeans project, then build and run it. You may also download the source code directly from GitHub.
Please feel free to contact us here on GitHub, to fork the project, contribute to it and send us pull requests to integrate your contributions. [An official roadmap shall be defined soon, so that we do not make redundant development efforts]