Computational aspects of an order-sorted logic with term declarations
From MaRDI portal
Publication:1801289
zbMath0689.68001MaRDI QIDQ1801289
Publication date: 5 June 1993
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Abstract data types; algebraic specification (68Q65) Mechanization of proofs and logical operations (03B35) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Thue and Post systems, etc. (03D03)
Related Items
A resolution principle for constrained logics, Unique-sort order-sorted theories : A description as monad morphisms, Higher-order unification, polymorphism, and subsorts, Reduction and unification in lambda calculi with a general notion of subtype, Another look at parameterization for oder-sorted algebraic specifications, Regular substitution sets: A means of controlling E-unification, A simple abstract semantics for equational theories, A note on assumptions about Skolem functions, Automatic synthesis of logical models for order-sorted first-order theories, On Skolemization in constrained logics, Unification in sort theories and its applications, Equality and disequality constraints on direct subterms in tree automata, An order-sorted resolution in theory and practice, Currying of order-sorted term rewriting systems, Projection: A unification procedure for tableaux in Conceptual Graphs, The calculus of context relations, Unnamed Item, A rewrite-based type discipline for a subset of computer algebra, Dynamically-typed computations for order-sorted equational presentations, The substitutional framework for sorted deduction: Fundamental results on hybrid reasoning, Semantics of order-sorted specifications, An order-sorted logic for knowledge representation systems, Unification in pseudo-linear sort theories is decidable, Strict coherence of conditional rewriting modulo axioms, Solving divergence in Knuth--Bendix completion by enriching signatures, A framework for the transfer of proofs, lemmas and strategies from classical to non classical logics, Tableau methods for a logic with term declarations, Unification in a combination of arbitrary disjoint equational theories, A mechanization of strong Kleene logic for partial functions, Unification in an extensional lambda calculus with ordered function sorts and constant overloading, Regular expression order-sorted unification and matching, Order-Sorted Rewriting and Congruence Closure, Fuzzy types: A framework for handling uncertainty about types of objects, A typed resolution principle for deduction with conditional typing theory, Order-sorted logic programming with predicate hierarchy, An algebraic semantics of higher-order types with subtypes, Symbolic computation in Maude: some tapas
