Equational problems and disunification
From MaRDI portal
Publication:1124372
DOI10.1016/S0747-7171(89)80017-3zbMATH Open0678.68093OpenAlexW2033074970MaRDI QIDQ1124372FDOQ1124372
Authors: Hubert Comon, Pierre Lescanne 
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
Recommendations
Mechanization of proofs and logical operations (03B35) Thue and Post systems, etc. (03D03) Abstract data types; algebraic specification (68Q65)
Cites Work
- Proving termination with multiset orderings
- An Efficient Unification Algorithm
- A Machine-Oriented Logic Based on the Resolution Principle
- The algebraic specification of abstract data types
- Title not available (Why is that?)
- Automatic proofs by induction in theories without constructors
- Explicit representation of terms defined by counter examples
- 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?)
Cited In (74)
- Explicit versus implicit representations of subsets of the Herbrand universe.
- Speeding up algorithms on atomic representations of Herbrand models via new redundancy criteria
- On inductive inference of cyclic structures
- Equivalence-preserving first-order unfold/fold transformation systems
- Complete axiomatizations of some quotient term algebras
- On solving nominal disunification constraints
- Superposition for Fixed Domains
- Equational formulas and pattern operations in initial order-sorted algebras
- Encompassment properties and automata with constraints
- Building proofs or counterexamples by analogy in a resolution framework
- A new method for undecidability proofs of first order theories
- Extracting models from clause sets saturated under semantic refinements of the resolution rule.
- Generalizing DPLL and satisfiability for equalities
- Anti-patterns for rule-based languages
- On the complexity of equational problems in CNF
- Combination of constraint solving techniques: An algebraic point of view
- Rewrite semantics for production rule systems: Theory and applications
- How to win a game with features
- Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness
- The first-order theory of lexicographic path orderings is undecidable
- Nominal equational problems
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- Matching - a special case of unification?
- How to win a game with features
- Proof methods of declarative properties of definite programs
- Model building with ordered resolution: Extracting models from saturated clause sets
- First order data types and first order logic
- An improved lower bound for the elementary theories of trees
- Combination of constraint solvers for free and quasi-free structures
- Weighted systems of equations
- Deducibility constraints and blind signatures
- A procedure for deciding symbolic equivalence between sets of constraint systems
- Quantifier elimination for infinite terms
- An equivalence preserving first order unfold/fold transformation system
- What is failure? An approach to constructive negation
- Equational formulae with membership constraints
- Accepting/rejecting propositions from accepted/rejected propositions: A unifying overview
- Partial matching for analogy discovery in proofs and counter-examples
- Decision procedures for term algebras with integer constraints
- Higher order disunification: Some decidable cases
- Extending Unification in $\mathcal{EL}$ to Disunification: The Case of Dismatching and Local Disunification
- Title not available (Why is that?)
- On deciding subsumption problems
- Equational Formulas and Pattern Operations in Initial Order-Sorted Algebras
- Narrowing based procedures for equational disunification
- Deciding the Inductive Validity of ∀ ∃ * Queries
- Unification of infinite sets of terms schematized by primal grammars
- Foundations of Information and Knowledge Systems
- Decidability Results for Saturation-Based Model Building
- On solving equations and disequations
- A method for simultaneous search for refutations and models by equational constraint solving
- The first order theory of primal grammars is decidable
- Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories
- Completion for constrained term rewriting systems
- Title not available (Why is that?)
- Title not available (Why is that?)
- Variant-Based Satisfiability in Initial Algebras
- Title not available (Why is that?)
- Working with ARMs: Complexity results on atomic representations of Herbrand models
- A method for building models automatically. Experiments with an extension of OTTER
- Negation elimination in equational formulae
- Analogy in Automated Deduction: A Survey
- Combining enumeration and deductive techniques in order to increase the class of constructible infinite models
- Combining induction and saturation-based theorem proving
- A matching process modulo a theory of categorical products
- On the cooperation of the constraint domains ℋ, ℛ, and ℱ in CFLP
- Simplifying and generalizing formulae in tableaux. Pruning the search space and building models
- Title not available (Why is that?)
- Computation of non-ground disjunctive well-founded semantics with constraint logic programming
- System description: SPASS-FD
- Disunification for ultimately periodic interpretations
- Predicate Completion for non-Horn Clause Sets
- Redundancy criteria for constrained completion
- AC complement problems: Satisfiability and negation elimination
This page was built for publication: Equational problems and disunification
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1124372)
