NuITP: Accelerating the inductive verification of equational programs through symbolic simplification

NuITP is an inductive theorem prover that combines advanced symbolic techniques such as narrowing, equality predicates, variant unification, variant satisfiability, order-sorted congruence closure, ordered rewriting, and strategy-based rewriting (all applied modulo axioms) to verify equational programs with expressive features such as sorts and subsorts, conditional equations and rewriting modulo axioms in Maude and in other equational languages. This paper presents the tool, explains its inference rules, and illustrates their use in proving several examples with substantial levels of automated proof simplification based on symbolic techniques.