NuITP · MANUAL · EXAMPLES · DOWNLOAD · TEAM · LICENSE


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




Download


The latest NuITP public releases can be found here:

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 later versions.


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


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.



© 2021-2024 · ELP Group · Valencian Research Institute for Artificial Intelligence · Universitat Politècnica de València