Equational problems and disunification

DOI10.1016/S0747-7171(89)80017-3zbMath0678.68093OpenAlexW2033074970MaRDI QIDQ1124372

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)80017-3

zbMATH Keywords

completeness unification termination equational problem transformation of equations systems

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) Mechanization of proofs and logical operations (03B35) Thue and Post systems, etc. (03D03)

Related Items

Completion for constrained term rewriting systems, The first order theory of primal grammars is decidable, Equational formulas and pattern operations in initial order-sorted algebras, What is failure? An approach to constructive negation, Encompassment properties and automata with constraints, Combination of constraint solving techniques: An algebraic point of view, On the cooperation of the constraint domains ℋ, ℛ, and ℱ in CFLP, Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories, Generalizing DPLL and satisfiability for equalities, Combination of constraint solvers for free and quasi-free structures, On inductive inference of cyclic structures, An equivalence preserving first order unfold/fold transformation system, A matching process modulo a theory of categorical products, First order data types and first order logic, Higher order disunification: Some decidable cases, Negation elimination in equational formulae, The first-order theory of lexicographic path orderings is undecidable, Unification of infinite sets of terms schematized by primal grammars, Extracting models from clause sets saturated under semantic refinements of the resolution rule., Model building with ordered resolution: Extracting models from saturated clause sets, On the complexity of equational problems in CNF, Decision procedures for term algebras with integer constraints, Semantically-guided goal-sensitive reasoning: inference system and completeness, Simplifying and generalizing formulae in tableaux. Pruning the search space and building models, Extending Unification in $\mathcal{EL}$ to Disunification: The Case of Dismatching and Local Disunification, Unnamed Item, Deducibility constraints and blind signatures, On solving nominal disunification constraints, Accepting/rejecting propositions from accepted/rejected propositions: A unifying overview, Superposition for Fixed Domains, Nominal equational problems, An improved lower bound for the elementary theories of trees, Rewrite semantics for production rule systems: Theory and applications, A method for simultaneous search for refutations and models by equational constraint solving, Complete axiomatizations of some quotient term algebras, Proof methods of declarative properties of definite programs, Equivalence-preserving first-order unfold/fold transformation systems, Combining enumeration and deductive techniques in order to increase the class of constructible infinite models, Speeding up algorithms on atomic representations of Herbrand models via new redundancy criteria, A new method for undecidability proofs of first order theories, Anti-patterns for rule-based languages, Analogy in Automated Deduction: A Survey, Redundancy criteria for constrained completion, AC complement problems: Satisfiability and negation elimination, Equational Formulas and Pattern Operations in Initial Order-Sorted Algebras, A procedure for deciding symbolic equivalence between sets of constraint systems, On deciding subsumption problems, Decidability Results for Saturation-Based Model Building, Matching - a special case of unification?, Tools for proving inductive equalities, relative completeness, and $\omega$-completeness, Variant-Based Satisfiability in Initial Algebras, Predicate Completion for non-Horn Clause Sets, System Description: SPASS-FD, A method for building models automatically. Experiments with an extension of OTTER, Combining induction and saturation-based theorem proving, Quantifier elimination for infinite terms, How to win a game with features, How to win a game with features, Deciding the Inductive Validity of ∀ ∃ * Queries, Partial matching for analogy discovery in proofs and counter-examples, Building proofs or counterexamples by analogy in a resolution framework, Explicit versus implicit representations of subsets of the Herbrand universe., Working with ARMs: Complexity results on atomic representations of Herbrand models, Weighted systems of equations

Cites Work