Regular substitution sets: A means of controlling E-unification

DOI10.1007/3-540-59200-8_71MaRDI QIDQ5055844zbMATH OpenOpenAlexFDO

Authors Jochen Burghardt

Publication date 9 December 2022

Published in Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1404.1201

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42)

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.

Cites work

• scientific article; zbMATH DE number 3870639 (Why is no real title available?)
• scientific article; zbMATH DE number 4053009 (Why is no real title available?)
• scientific article; zbMATH DE number 177848 (Why is no real title available?)
• scientific article; zbMATH DE number 1354167 (Why is no real title available?)
• scientific article; zbMATH DE number 512377 (Why is no real title available?)
• Computational aspects of an order-sorted logic with term declarations
• Foundations of equational logic programming
• On restrictions of ordered paramodulation with simplification

This page was built for publication: Regular substitution sets: A means of controlling E-unification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5055844)