Regular Substitution Sets: A Means of Controlling E-Unification
Formal Languages and Automata Theory
2019-04-19 v2 Logic in Computer Science
Abstract
A method for selecting solution constructors in narrowing is presented. The method is based on a sort discipline that describes regular sets of ground constructor terms as sorts. It is extended to cope with regular sets of ground substitutions, thus allowing different sorts to be computed for terms with different variable bindings. An algorithm for computing signatures of equationally defined functions is given that allows potentially infinite overloading. Applications to formal program development are sketched.
Keywords
Cite
@article{arxiv.1404.1201,
title = {Regular Substitution Sets: A Means of Controlling E-Unification},
author = {Jochen Burghardt},
journal= {arXiv preprint arXiv:1404.1201},
year = {2019}
}
Comments
61 pages; 35 figures