NuITP: An Inductive Theorem Prover for Equational Program Verification

Abstract

NuITP is an inductive equational 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. The present paper introduces the tool, explains its most commonly used inference rules, and illustrates their use in proving the card trick benchmark.