LoTREC is an automated theorem prover for modal and description logics using the tableau method. It enables students and researchers to define custom logics with Kripke semantics and verify formula properties (satisfiability, validity) through interactive proof visualization.
- 38 predefined logics including K, KT, S4, S5, and description logics
- Visual tableau construction with interactive graph display
- Custom logic definition via XML-based rule specification
- Step-by-step debugging with breakpoints on rules
- Model checking capabilities
Download the latest release, extract the ZIP, and run:
- Windows:
bin/LoTREC.bat - Linux/macOS:
bin/LoTREC
Requires Java 8 or later. Get it from Eclipse Adoptium.
On startup, select a predefined logic like Modal logic K or open your own logic file.
Enter a formula and click Build Premodels to see the tableau proof tree.
| Guide | Description |
|---|---|
| Getting Started | Installation and your first proof |
| User Guide | Complete interface reference |
| Defining Logics | Create custom logics with XML |
| Predefined Logics | List of 38 built-in logics |
Clone the repository and build with Gradle:
git clone https://github.com/bilals/lotrec.git
cd lotrec
./gradlew build # Build and test
./gradlew run # Run the applicationSee CLAUDE.md for detailed build commands and architecture overview.
For extensive debugging sessions or large proofs, increase memory allocation.
Edit bin/LoTREC.bat (Windows) or bin/LoTREC (Linux/macOS):
DEFAULT_JVM_OPTS="-Xmx512M" # 512MB (or -Xmx2048M for 2GB)
We welcome contributions! Please:
- Fork the repository
- Create a feature branch
- Submit a pull request
Report issues on GitHub Issues.
- Repository: https://github.com/bilals/lotrec
- Legacy Site: https://www.irit.fr/Lotrec/
LoTREC is released under the GPL-2.0 License.