Satisfiability of systems of ordinal notations with the subterm property is decidable

DOI10.1007/3-540-54233-7_155MaRDI QIDQ4036585zbMATH OpenFDO

Authors Jean-Pierre Jouannaud, Mitsuhiro Okada

Publication date 18 May 1993

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-54233-7_155

zbMATH Keywords

constrained logic programmingmultiset path orderingordered resolutionparamodulationrecursive path orderingrewrite orderings on termssatisfiabilitysolving 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)

• A new method for undecidability proofs of first order theories
• 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
• Constraint solving for term orderings compatible with abelian semigroups, monoids and groups
• Ordinals. I: Basic notions
• 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
• The use of embeddings to provide a clean separation of term and annotation for higher order rippling
• SOLVING SYMBOLIC ORDERING CONSTRAINTS
• Redundancy criteria for constrained completion
• A total AC-compatible ordering based on RPO
• Simple LPO constraint solving methods

This page was built for publication: Satisfiability of systems of ordinal notations with the subterm property is decidable

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4036585)