scientific article
From MaRDI portal
Publication:4036585
zbMath0789.68125MaRDI QIDQ4036585
Jean-Pierre Jouannaud, Mitsuhiro Okada
Publication date: 18 May 1993
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
satisfiabilityrecursive path orderingparamodulationordered 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)
Related Items
About the theory of tree embedding, Open problems in rewriting, A precedence-based total AC-compatible ordering, Polynomial time termination and constraint satisfaction tests, More problems in rewriting, Problems in rewriting III, Solving simplification ordering constraints, Abstract data type systems, The first-order theory of lexicographic path orderings is undecidable, Practical algorithms for deciding path ordering constraint satisfaction., Orienting rewrite rules with the Knuth-Bendix order., Stratified resolution, Redundancy criteria for constrained completion, A total AC-compatible ordering based on RPO, Simple LPO constraint solving methods, The use of embeddings to provide a clean separation of term and annotation for higher order rippling, A new method for undecidability proofs of first order theories, Ordinals. I: Basic notions
