A modular order-sorted equational generalization algorithm

DOI10.1016/j.ic.2014.01.006zbMath1314.68169WikidataQ57978120 ScholiaQ57978120MaRDI QIDQ2437800

José Meseguer, Santiago Escobar, Javier Espert, María Alpuente

Publication date: 13 March 2014

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2014.01.006

zbMATH Keywords

equational theories; anti-unification; generalization algorithm; least general generalizations; order-sorted theories

Mathematics Subject Classification ID

03B70: Logic in computer science

68Q42: Grammars and rewriting systems

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Related Items

Assertion-based analysis via slicing withABETS(system description), Unnamed Item, Term-Graph Anti-Unification, Higher-order pattern generalization modulo equational theories, A Generic Framework for Higher-Order Generalizations., Symbolic Specialization of Rewriting Logic Theories with Presto, Variant-based equational anti-unification, Optimizing Maude programs via program specialization, Debugging Maude programs via runtime assertion checking and trace slicing, Symbolic computation in Maude: some tapas, A complete semantics of \(\mathbb{K}\) and its translation to Isabelle, Order-sorted equational generalization algorithm revisited, Anti-unification and the theory of semirings, Fuzzy lattice operations on first-order terms over signatures with similar constructors: a constraint-based approach, Programming and symbolic computation in Maude, A partial evaluation framework for order-sorted equational programs modulo axioms, Higher-order pattern anti-unification in linear time, Unranked second-order anti-unification, Equational formulas and pattern operations in initial order-sorted algebras, Optimization of rewrite theories by equational partial evaluation, A Library of Anti-unification Algorithms, ACUOS: A System for Modular ACU Generalization with Subtyping and Inheritance, Combining Runtime Checking and Slicing to Improve Maude Error Diagnosis

Uses Software

• OBJ3
• CafeOBJ
• Maude
• ITP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Order-sorted unification
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Inheritance hierarchies: Semantics and unifications
• Unification theory
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• Incremental constraint satisfaction for equational logic programming
• Bottom-up induction of feature terms
• Higher order generalization and its application in program verification
• ELAN from a rewriting logic point of view
• A structural approach to operational semantics
• Inductive Logic Programming: Issues, results and the challenge of Learning Language in Logic
• E-generalization using grammars
• Specialization of inductively sequential functional logic programs
• Anti-unification Algorithms and Their Applications in Program Analysis
• A Modular Equational Generalization Algorithm
• An Efficient Unification Algorithm
• Order-Sorted Generalization
• Unification, weak unification, upper bound, lower bound, and generalization problems
• Anti-Unification for Unranked Terms and Hedges