scientific article; zbMATH DE number 176755
From MaRDI portal
Publication:4036585
zbMATH Open0789.68125MaRDI QIDQ4036585FDOQ4036585
Authors: Jean-Pierre Jouannaud, Mitsuhiro Okada
Publication date: 18 May 1993
Title of this publication is not available (Why is that?)
Recommendations
satisfiabilityparamodulationrecursive path orderingordered resolutionmultiset path orderingconstrained logic programmingrewrite orderings on termssolving ordering constraints between terms
Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Recursive ordinals and ordinal notations (03F15)
Cited In (20)
- Simple LPO constraint solving methods
- A new method for undecidability proofs of first order theories
- Practical algorithms for deciding path ordering constraint satisfaction.
- Open problems in rewriting
- The use of embeddings to provide a clean separation of term and annotation for higher order rippling
- Stratified resolution
- The first-order theory of lexicographic path orderings is undecidable
- Orienting rewrite rules with the Knuth-Bendix order.
- Abstract data type systems
- More problems in rewriting
- Constraint solving for term orderings compatible with abelian semigroups, monoids and groups
- Solving simplification ordering constraints
- About the theory of tree embedding
- Ordinals. I: Basic notions
- A precedence-based total AC-compatible ordering
- Polynomial time termination and constraint satisfaction tests
- SOLVING SYMBOLIC ORDERING CONSTRAINTS
- A total AC-compatible ordering based on RPO
- Redundancy criteria for constrained completion
- Problems in rewriting III
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4036585)