Solving partial order constraints for LPO termination

MaRDI QIDQ3620437zbMATH OpenFDO

Authors Michael Codish, V. Lagoon, Peter J. Stuckey

Publication date 14 April 2009

zbMATH Keywords

Boolean satisfiabilityterm rewrite systemslexicographic path orders

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• Solving Partial Order Constraints for LPO Termination
• SAT solving for termination proofs with recursive path orders and dependency pairs
• Proving Termination Using Recursive Path Orders and SAT Solving
• SAT Solving for Argument Filterings
• Constraints for Argument Filterings

Cited in

(3)

• SAT solving for termination proofs with recursive path orders and dependency pairs
• SAT Solving for Argument Filterings
• Solving Partial Order Constraints for LPO Termination

Describes a project that uses

Uses Software

• MiniSat

This page was built for publication: Solving partial order constraints for LPO termination

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