Verifying an Applicative ATP Using Multiset Relations

We present in this paper a formalization of multiset relations in the ACL2 theorem prover [6], and we show how multisets can be used to mechanically prove non-trivial termination properties. Every relation on a set A induces a relation on finite multisets over A; it can be shown that the multiset relation induced by a well-founded relation is also well-founded [3]. We have carried out a mechanical proof of this property in the ACL2 logic. This allows us to provide well-founded multiset relations in order to prove termination of recursive functions. Once termination is proved, the function definition is admitted as an axiom in the logic and formal mechanized reasoning about it is possible. As a major application of this tool, we show how multisets can be used to prove termination of a tableaux based theorem prover for propositional logic.