Order-sorted unification

DOI10.1016/S0747-7171(89)80036-7MaRDI QIDQ582269zbMATHOpenAlexFDO

Authors José Meseguer, Joseph Goguen, Gert Smolka

Publication date 1989

Published in Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s0747-7171(89)80036-7

zbMATH Keywords

categorical treatment of unificationOrder-sorted equational logic

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Equational logic, Mal'tsev conditions (08B05)

Recommendations

• Order-sorted feature theory unification
• An ordering linear unification algorithm
• Unification in sort theories and its applications
• Order-sorted generalization
• Order-Sorted Unification with Regular Expression Sorts.
• Ordering based on uninorms
• scientific article; zbMATH DE number 1759378
• AC unification through order-sorted AC1 unification
• AC unification through order-sorted AC1 unification
• Order-sorted equational unification revisited

Cites work

• scientific article; zbMATH DE number 4018380 (Why is no real title available?)
• scientific article; zbMATH DE number 3911679 (Why is no real title available?)
• scientific article; zbMATH DE number 3949706 (Why is no real title available?)
• scientific article; zbMATH DE number 4028891 (Why is no real title available?)
• scientific article; zbMATH DE number 4049131 (Why is no real title available?)
• scientific article; zbMATH DE number 4049132 (Why is no real title available?)
• scientific article; zbMATH DE number 4060701 (Why is no real title available?)
• scientific article; zbMATH DE number 3684925 (Why is no real title available?)
• scientific article; zbMATH DE number 3784848 (Why is no real title available?)
• scientific article; zbMATH DE number 43017 (Why is no real title available?)
• scientific article; zbMATH DE number 1088220 (Why is no real title available?)
• scientific article; zbMATH DE number 1442964 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• scientific article; zbMATH DE number 3367095 (Why is no real title available?)
• scientific article; zbMATH DE number 3413831 (Why is no real title available?)
• A Machine-Oriented Logic Based on the Resolution Principle
• A mechanical solution of Schubert's steamroller by many-sorted resolution
• An Efficient Unification Algorithm
• An Oxford survey of order sorted algebra
• An algebraic semantics approach to the effective resolution of type equations
• Complete sets of unifiers and matchers in equational theories
• Cost pass-through and inverse demand curvature in vertical relationships with upstream and downstream competition
• Equality, types, modules, and (why not?) generics for logic programming
• Inheritance hierarchies: Semantics and unifications
• Order-sorted algebra solves the constructor-selector, multiple representation, and coercion problems
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• Proofs by induction in equational theories with constructors
• Unification theory

Cited in

(33)

• Order-Sorted Parameterization and Induction
• scientific article; zbMATH DE number 2085285 (Why is no real title available?)
• Unique-sort order-sorted theories : A description as monad morphisms
• A higher-order calculus of computational fields
• The calculus of context relations
• Soft typing for ordered resolution
• Semantics of order-sorted specifications
• Computational aspects of an order-sorted logic with term declarations
• A complete semantics of \(\mathbb{K}\) and its translation to Isabelle
• scientific article; zbMATH DE number 1231543 (Why is no real title available?)
• Programming and symbolic computation in Maude
• scientific article; zbMATH DE number 4049131 (Why is no real title available?)
• scientific article; zbMATH DE number 4049132 (Why is no real title available?)
• Order-sorted equational unification revisited
• An ordering linear unification algorithm
• AC unification through order-sorted AC1 unification
• On notions of inductive validity for first-order equational clauses
• Order-sorted generalization
• scientific article; zbMATH DE number 1552530 (Why is no real title available?)
• On First-Order Model-Based Reasoning
• scientific article; zbMATH DE number 517007 (Why is no real title available?)
• Regular expression order-sorted unification and matching
• Equational formulas and pattern operations in initial order-sorted algebras
• Completion of rewrite systems with membership constraints
• Strict coherence of conditional rewriting modulo axioms
• Equational formulas and pattern operations in initial order-sorted algebras
• Unification in sort theories and its applications
• A modular order-sorted equational generalization algorithm
• Term Rewriting and Applications
• Unification in an extensional lambda calculus with ordered function sorts and constant overloading
• Higher-order unification, polymorphism, and subsorts
• Symbolic computation in Maude: some tapas
• Order-Sorted Unification with Regular Expression Sorts.

This page was built for publication: Order-sorted unification

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