NuITP is an inductive theorem prover for Maude equational specifications that combines powerful state-of-the-art techniques such as narrowing, equality predicates, constructor variant unification, order-sorted congruence closure, ordered rewriting, strategy-based rewriting, and several others in order to reason about Maude equational programs. The tool is written in Maude and thus requires the Maude System to run.
Manual
The latest version of the NuITP manual is available here.
Examples
- A collection of NuITP examples can be found here, which includes -among others- proofs of properties such as left and right associativity for natural numbers, distributivity of multiplication over addition, asociativity of concatenation of lists, etc.
- A detailed proof of the Gilbreath Card Trick can be found here.
Download
The latest NuITP public releases can be found here:
- Feb 16, 2026 - NuITP Alpha 35 (requires Maude Nightly build Nov 10, 2025 or later)
- May 23, 2024 - NuITP Alpha 30 (requires Maude Alpha 160 or later)
- Apr 5, 2024 - NuITP Alpha 28
- Oct 13, 2023 - NuITP Alpha 23
- Jul 6, 2023 - NuITP Alpha 21
Team
- Ph.D. in Computer Science
- Full Professor at the Universitat Politècnica de València
- Ph.D. in Computer Science
- Assistant Professor at the Universitat Politècnica de València
License
Copyright 2021-2026 Universitat Politècnica de València, Spain.
NuITP is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version.
NuITP is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
See the GNU General Public License at www.gnu.org/licenses for more details.