Order-sorted unification

DOI10.1016/S0747-7171(89)80036-7zbMATH Open0691.03002OpenAlexW2031327296MaRDI QIDQ582269FDOQ582269

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

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

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)

Cites Work

• A mechanical solution of Schubert's steamroller by many-sorted resolution
• Title not available (Why is that?)
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• An Efficient Unification Algorithm
• A Machine-Oriented Logic Based on the Resolution Principle
• Title not available (Why is that?)
• Title not available (Why is that?)
• Order-sorted algebra solves the constructor-selector, multiple representation, and coercion problems
• An Oxford survey of order sorted algebra
• Proofs by induction in equational theories with constructors
• Cost pass-through and inverse demand curvature in vertical relationships with upstream and downstream competition
• An algebraic semantics approach to the effective resolution of type equations
• Inheritance hierarchies: Semantics and unifications
• Unification theory
• Complete sets of unifiers and matchers in equational theories
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Equality, types, modules, and (why not?) generics for logic programming

Cited In (33)

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

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)