Simple LPO constraint solving methods

DOI10.1016/0020-0190(93)90226-YMaRDI QIDQ685481zbMATH OpenFDO

Authors Robert Nieuwenhuis

Publication date 17 October 1993

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0020-0190(93)90226-Y

zbMATH Keywords

automatic theoremNP-completeproving

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Analysis of algorithms and problem complexity (68Q25)

Review text

Satisfiability of lexicographic path ordering constraints was shown to be decidable under the given signature by \textit{H. Comon} [Int. J. Found. Comp. Sci. 1, No. 4, 387-411 (1990; Zbl 0722.03012)]; the author and \textit{A. Rubio} [Theorem proving with ordering constrained clauses, Proc. 11th Int. Conf. on Automated Deduction, Saratoga Springs, NY, Springer, Berlin, 477-491 (1992)] obtained the like result for satisfiability under extended signatures. Both satisfiability problem are now proved to be NP- complete by reducing the constraints to disjunctions of ``simple systems (conjunctions of equalities and inequalities); it is argued that this technique should have practical relevance.

Recommendations

• A simplex method based on reducing the constraint conditions of linear programming
• Linear programs for constraint satisfaction problems
• An LP-Designed Algorithm for Constraint Satisfaction
• scientific article; zbMATH DE number 5251052
• scientific article; zbMATH DE number 4158377
• scientific article; zbMATH DE number 232263
• scientific article; zbMATH DE number 5000797
• Simplex algorithms for linear programming
• scientific article; zbMATH DE number 916038

Cites work

• scientific article; zbMATH DE number 176755 (Why is no real title available?)
• scientific article; zbMATH DE number 1348468 (Why is no real title available?)
• SOLVING SYMBOLIC ORDERING CONSTRAINTS

Cited in

(16)

• 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
• Decision Procedures for Automating Termination Proofs
• scientific article; zbMATH DE number 176755 (Why is no real title available?)
• scientific article; zbMATH DE number 1342225 (Why is no real title available?)
• Ordered tableaux: extensions and applications
• More problems in rewriting
• Solving simplification ordering constraints
• Ordered chaining for total orderings
• What you always wanted to know about rigid \(E\)-unification
• SOLVING SYMBOLIC ORDERING CONSTRAINTS
• KBO Constraint Solving Revisited
• Term ordering diagrams
• Partial redundancy in saturation

This page was built for publication: Simple LPO constraint solving methods

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