Flat Domains and Recursive Equations in ACL2

摘要: Flat domains can be viewed as a “logic” of total functions in which every recursive equation has at least one function that satisfies it. One formalization flat ACL2 is presented some detail. are reviewed enough detail to make this paper self contained for those who never knew or don’t remember much about them.