Regular substitution sets: A means of controlling E-unification

DOI10.1007/3-540-59200-8_71zbMATH Open1503.68093arXiv1404.1201OpenAlexW1482664385MaRDI QIDQ5055844FDOQ5055844

Authors: Jochen Burghardt 

Publication date: 9 December 2022

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

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.

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

Recommendations

• Publication:3490956
• scientific article; zbMATH DE number 3960989
• scientific article; zbMATH DE number 4060700
• scientific article; zbMATH DE number 4031035
• scientific article; zbMATH DE number 3921947

Mathematics Subject Classification ID

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

Cites Work

• Computational aspects of an order-sorted logic with term declarations
• Title not available (Why is that?)
• Foundations of equational logic programming
• Title not available (Why is that?)
• On restrictions of ordered paramodulation with simplification
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

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)