NuITP

NuITP

Inductive Theorem Prover for Maude Equational Specifications

Download Alpha 39 User Manual Maude System

Overview

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

Documentation

NuITP User Manual

Detailed execution and usage instructions, in PDF.

Download PDF

Examples

Below you can find some examples of NuITP in use.

  • Gilbreath

    html

    Verification of the Gilbreath shuffle principle, walked through step by step.

  • Examples collection

    zip

    A collection of NuITP examples, which includes —among others— proofs of properties such as left and right associativity for natural numbers, distributivity of multiplication over addition, and associativity of list concatenation.

Download

Latest release

NuITP Alpha 39

Released Jul 31, 2026 · requires Maude Alpha 165 or later.

Download

All published versions, listed from most recent to oldest.

  • Jul 31, 2026 NuITP Alpha 39 Latest Requires Maude Alpha 165 or later.
  • 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

University of Málaga

Santiago Escobar

Full Professor

Universitat Politècnica de València

José Meseguer

Full Professor

University of Illinois Urbana-Champaign

Julia Sapiña

Assistant Professor

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.