We introduce the notion of well-founded recursive order-sorted equational logic
(OS) theories modulo axioms. Such theories define functions by well-founded recursion and
are inherently terminating. Moreover, for well-founded recursive theories important properties such as confluence and sufficient completeness are modular for so-called fair extensions.
This enables us to incrementally check these properties for hierarchies of such theories that
occur naturally in modular rule-based functional programs. Well-founded recursive OS theories modulo axioms contain only commutativity and associativity-commutativity axioms.
In order to support arbitrary combinations of associativity, commutativity and identity axioms, we show how to eliminate identity and (under certain conditions) associativity (without
commutativity) axioms by theory transformations in the last part of the paper.
Use this login method if you
don't
have an
@illinois.edu
email address.
(Oops, I do have one)
IDEALS migrated to a new platform on June 23, 2022. If you created
your account prior to this date, you will have to reset your password
using the forgot-password link below.
