NuITP

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.

Download

The latest NuITP version can be found here:

Apr 5th, 2024 - NuITP Alpha 28

Note that, as the NuITP is in very early stages of development, scripts generated by older versions of NuITP may not be fully compatible with this version.

Team

Francisco Durán

Ph.D. in Computer Science
Full Professor at the University of Málaga

Santiago Escobar

Ph.D. in Computer Science
Full Professor at the Universitat Politècnica de València

José Meseguer

Ph.D. in Mathematics
Full Professor at the University of Illinois in Urbana-Champaign

Julia Sapiña

Ph.D. in Computer Science
Postdoc Researcher 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.