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:
- 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
- Postdoc Researcher at the Universitat Politècnica de València
License
Copyright 2021-2024 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.