Explicit Logic Trees ⇒ Core of Explainable AI (XAI)
First-Order & Propositional Interactive Symbolic Reasoning Engines,
built 2002–2004, now open-sourced.
Originally designed for teaching and learning mathematical logic.
⚠ It will work only if you have installed Java: Download recommended version
Don’t trust me, but scan downloaded JARs on: VirusTotal
Instructions
- Select any of the READY-MADE EXAMPLE formulas of First-Order Logic and press ENTER.
-
Try to FOLLOW THE PATTERN you observe in the example formulas.
Note: Predicate P may take two variables, while Q takes only one.
Valid examples: ∀x∃y Pxy, ∀y Qy, ∃x Qx
Invalid example: ∃x∀y Qxy
If you make a mistake, the INVALID part of the input will be automatically removed.
[Note on syntax: Logical grouping parentheses are intentionally omitted for practical simplicity. Predicates are written in compact form: Pxy instead of P(x,y).]
- Try the “−(formula)” button — it negates the entire formula. Then press ENTER again and observe the changes in the calculator window.
Technical & Working Explanation
Formulas are recursively decomposed into primitive connectives and transformed via De Morgan laws into a Negation Normal Form (NNF) Abstract Syntax Tree (AST), with negations pushed to the atomic level.
[ChatGPT observation: “This looks like the DNA of common sense.”]
👉 Full technical description: README on GitHub
IF THIS SEEMS TOO COMPLICATED AT FIRST, PLEASE PROCEED TO THE MUCH SIMPLER PROPOSITIONAL TREE BELOW (Beginner mode).
PROPOSITIONAL logic ⇒ MINIMAL NORMAL FORMS
🔄 Calculators last updated: 12. 1. 2026.
Licenced open-source project. Full source code and releases are maintained on GitHub.
View source on GitHub 🎓 Academic / Educational use: PMF, University of Zagreb (2002) · Public release: 2025Please contact the author for long-term or institutional use.
Dedicated to every child who dies from starvation — 1 every 10 seconds, around 10,000 each day.
❤️ So if you like this project, please consider supporting a meal for a child: https://marysmeals.org