Recommendations
Cites work
- scientific article; zbMATH DE number 4164129 (Why is no real title available?)
- scientific article; zbMATH DE number 4164137 (Why is no real title available?)
- scientific article; zbMATH DE number 4164142 (Why is no real title available?)
- scientific article; zbMATH DE number 3936507 (Why is no real title available?)
- scientific article; zbMATH DE number 4037164 (Why is no real title available?)
- scientific article; zbMATH DE number 4045129 (Why is no real title available?)
- scientific article; zbMATH DE number 4049024 (Why is no real title available?)
- scientific article; zbMATH DE number 4089518 (Why is no real title available?)
- scientific article; zbMATH DE number 3639170 (Why is no real title available?)
- A Machine-Oriented Logic Based on the Resolution Principle
- An Efficient Unification Algorithm
- Automatic proofs by induction in theories without constructors
- Explicit representation of terms defined by counter examples
- Proving termination with multiset orderings
- The algebraic specification of abstract data types
Cited in
(76)- Computation of non-ground disjunctive well-founded semantics with constraint logic programming
- Simplifying and generalizing formulae in tableaux. Pruning the search space and building models
- System description: SPASS-FD
- Redundancy criteria for constrained completion
- Decidability Results for Saturation-Based Model Building
- AC complement problems: Satisfiability and negation elimination
- Extending unification in \(\mathcal{EL}\) to disunification: the case of dismatching and local disunification
- Predicate Completion for non-Horn Clause Sets
- Disunification for ultimately periodic interpretations
- scientific article; zbMATH DE number 7453200 (Why is no real title available?)
- On the cooperation of the constraint domains ℋ, ℛ, and ℱ in CFLP
- A matching process modulo a theory of categorical products
- Building proofs or counterexamples by analogy in a resolution framework
- On inductive inference of cyclic structures
- A new method for undecidability proofs of first order theories
- Partial matching for analogy discovery in proofs and counter-examples
- Nominal equational problems
- What is failure? An approach to constructive negation
- Rewrite semantics for production rule systems: theory and applications
- Extracting models from clause sets saturated under semantic refinements of the resolution rule.
- On solving equations and disequations
- How to win a game with features
- Equivalence-preserving first-order unfold/fold transformation systems
- Matching - a special case of unification?
- Completion for constrained term rewriting systems
- Decision procedures for term algebras with integer constraints
- scientific article; zbMATH DE number 1004365 (Why is no real title available?)
- Combining induction and saturation-based theorem proving
- scientific article; zbMATH DE number 1186371 (Why is no real title available?)
- Generalizing DPLL and satisfiability for equalities
- Model building with ordered resolution: Extracting models from saturated clause sets
- Combination of constraint solving techniques: An algebraic point of view
- On deciding subsumption problems
- A method for simultaneous search for refutations and models by equational constraint solving
- Decidability of affine solution problems
- Working with ARMs: Complexity results on atomic representations of Herbrand models
- Equational formulae with membership constraints
- scientific article; zbMATH DE number 1860670 (Why is no real title available?)
- Equational formulas and pattern operations in initial order-sorted algebras
- Weighted systems of equations
- How to win a game with features
- Accepting/rejecting propositions from accepted/rejected propositions: A unifying overview
- Explicit versus implicit representations of subsets of the Herbrand universe.
- Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness
- Complete axiomatizations of some quotient term algebras
- Equational formulas and pattern operations in initial order-sorted algebras
- Deciding the Inductive Validity of ∀ ∃ * Queries
- Speeding up algorithms on atomic representations of Herbrand models via new redundancy criteria
- Parameterized provability in equational logic
- Negation elimination in equational formulae (extended abstract)
- First order data types and first order logic
- A procedure for deciding symbolic equivalence between sets of constraint systems
- Anti-patterns for rule-based languages
- Unification of infinite sets of terms schematized by primal grammars
- Proof methods of declarative properties of definite programs
- Higher order disunification: some decidable cases
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- The first order theory of primal grammars is decidable
- Analogy in automated deduction: a survey
- Foundations of Information and Knowledge Systems
- Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories
- An improved lower bound for the elementary theories of trees
- Combining enumeration and deductive techniques in order to increase the class of constructible infinite models
- Quantifier elimination for infinite terms
- On the complexity of equational problems in CNF
- On solving nominal disunification constraints
- Variant-Based Satisfiability in Initial Algebras
- Encompassment properties and automata with constraints
- An equivalence preserving first order unfold/fold transformation system
- scientific article; zbMATH DE number 4089518 (Why is no real title available?)
- A method for building models automatically. Experiments with an extension of OTTER
- The first-order theory of lexicographic path orderings is undecidable
- Combination of constraint solvers for free and quasi-free structures
- Deducibility constraints and blind signatures
- Superposition for Fixed Domains
- Narrowing based procedures for equational disunification
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)
