[ US ] [ CCIA ] [ Teaching ] [ SLC ] [e-mail]
Multiset relations: a tool for proving termination (in ACL2)

Computational Logic Group, CCIA, Universidad de Sevilla, Spain


Here are the books we developed to implement well-founded multiset extension of a given well-founded ACL2 relation.

The main books:

Examples using defmul:


e-mail
Dpto. de Ciencias de la Computación e Inteligencia Artificial
Facultad de Informática y Estadística
Universidad de Sevilla

Multiset relations: a tool for proving termination (in ACL2)