scientific article; zbMATH DE number 176755

MaRDI QIDQ4036585zbMATH OpenFDO

Authors Jean-Pierre Jouannaud, Mitsuhiro Okada

Publication date 18 May 1993

zbMATH Keywords

satisfiabilityparamodulationrecursive path orderingordered resolutionmultiset path orderingconstrained logic programmingrewrite orderings on termssolving ordering constraints between terms

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Recursive ordinals and ordinal notations (03F15)

Recommendations

• Practical algorithms for deciding path ordering constraint satisfaction.
• Solving simplification ordering constraints
• Maximal extensions of simplification orderings
• Simple LPO constraint solving methods
• Polynomial time termination and constraint satisfaction tests

Cited in

(20)

• SOLVING SYMBOLIC ORDERING CONSTRAINTS
• Problems in rewriting III
• Simple LPO constraint solving methods
• A new method for undecidability proofs of first order theories
• Practical algorithms for deciding path ordering constraint satisfaction.
• The use of embeddings to provide a clean separation of term and annotation for higher order rippling
• Open problems in rewriting
• Stratified resolution
• The first-order theory of lexicographic path orderings is undecidable
• Orienting rewrite rules with the Knuth-Bendix order.
• Abstract data type systems
• Constraint solving for term orderings compatible with abelian semigroups, monoids and groups
• More problems in rewriting
• 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
• A total AC-compatible ordering based on RPO
• Redundancy criteria for constrained completion

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)