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
Download the latest version of the NuITP User Manual in PDF format for detailed execution and usage instructions.
Examples
Below you can find some examples of NuITP in use.
- Gilbreath Verification of the Gilbreath shuffle principle.
- Examples collection 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.
Download
Here you will find all published versions of NuITP, listed from most recent to oldest.
- Jul 14, 2026 NuITP Alpha 38 Requires Maude Nightly build Apr 9, 2026 or later.
- May 5, 2026 NuITP Alpha 37 Requires Maude Nightly build Apr 9, 2026 or later.
- Mar 9, 2026 NuITP Alpha 36 Requires Maude Nightly build Nov 10, 2025 or later.
- 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 Requires Maude 3.4 or later.
- Oct 13, 2023 NuITP Alpha 23 Requires Maude Alpha 150 or later.
- Jul 6, 2023 NuITP Alpha 21 Requires Maude Alpha 149 or later.
We recommend always using the latest version. If you have any questions about which one to use, please refer to the Manual or contact the team.
Team
Francisco Durán
Full Professor at the University of Málaga
Santiago Escobar
Full Professor at the Universitat Politècnica de València
José Meseguer
Full Professor at the University of Illinois in Urbana-Champaign
Julia Sapiña
Assistant Professor at the Universitat Politècnica de València
License
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.