SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs

No abstract is available for this paper.

• Publication year

  2012

• Venue

  Journal of automated reasoning

• Publication date

  2012-06-01

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1007/s10817-010-9211-0
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• A declarative approach to robust weighted Max-SAT

  2010cited by this paper
• Implementing logical connectives in constraint programming

  2010cited by this paper
• KBO Orientability

  2009cited by this paper
• Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme

  2009cited by this paper
• A declarative encoding of telecommunications feature subscription in SAT

  2009cited by this paper
• Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic

  2009cited by this paper
• Search Techniques for Rational Polynomial Orders

  2008cited by this paper
• SAT(ID): Satisfiability of Propositional Logic Extended with Inductive Definitions

  2008cited by this paper
• Global difference constraint propagation for finite domain solvers

  2008cited by this paper
• Maximal Termination

  2008cited by this paper
• A SAT-Based Approach to Size Change Termination with Global Ranking Functions

  2008cited by this paper
• Increasing interpretations

  2008cited by this paper
• Proving Termination Using Recursive Path Orders and SAT Solving

  2007cited by this paper
• SAT Solving for Termination Analysis with Polynomial Interpretations

  2007cited by this paper
• Tyrolean termination tool: Techniques and features

  2007cited by this paper
• Constraints for Argument Filterings

  2007cited by this paper
• Predictive Labeling with Dependency Pairs Using SAT

  2007cited by this paper
• Compiling finite linear CSP into SAT

  2006cited by this paper
• Mechanizing and Improving Dependency Pairs

  2006influential reference
• SAT Solving for Argument Filterings

  2006cited by this paper
• Translating Pseudo-Boolean Constraints into SAT

  2006cited by this paper
• Automatic Termination Proofs in the Dependency Pair Framework

  2006cited by this paper
• Matrix Interpretations for Proving Termination of Term Rewriting

  2006cited by this paper
• The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs

  2005influential reference
• Solving Partial Order Constraints for LPO Termination

  2005influential reference
• Proving and Disproving Termination of Higher-Order Functions

  2005cited by this paper
• Automating the Dependency Pair Method

  2005influential reference
• Efficient BDD Encodings for Partial Order Constraints with Application to Expert Systems in Software Verification

  2004cited by this paper
• Termination of term rewriting using dependency pairs

  2000influential reference
• Argument Filtering Transformation

  1999cited by this paper
• Term rewriting and all that

  1998cited by this paper
• Relative Termination

  1990cited by this paper
• Termination of Rewriting Systems by Polynomial Interpretations and Its Implementation

  1987cited by this paper
• Journal of automated reasoning

  1986cited by this paper
• On Recursive Path Ordering

  1985cited by this paper
• Computer experiments with the REVE term rewriting system generator

  1983cited by this paper
• On the Complexity of Derivation in Propositional Calculus

  1983cited by this paper
• Orderings for term-rewriting systems

  1979cited by this paper
• DOI: 10.1017/S000000000000000 Printed in the United Kingdom TCAS software verification using Constraint Programming

  year unknowncited by this paper

• Termination of Term Rewriting: Foundation, Formalization, Implementation, and Competition (Invited Talk)

  2023cites this paper
• The Generalized Multiset Ordering is NP-Complete

  2022cites this paper
• Certifying the Weighted Path Order

  2020cites this paper
• Specialising Software for Different Downstream Applications Using Genetic Improvement and Code Transplantation

  2018cites this paper
• Size-based termination of higher-order rewriting

  2018cites this paper
• A Lambda-Free Higher-Order Recursive Path Order

  2017cites this paper
• Analyzing Program Termination and Complexity Automatically with AProVE

  2016cites this paper
• Termination checking in Dedukti

  2016cites this paper
• Analysing the Termination of Term Rewriting Systems using Data Mining

  2015cites this paper
• The computability path ordering

  2015cites this paper
• 14th International Workshop on Termination (WST 2014)

  2014cites this paper
• SAT Compilation for Constraints over Finite Structured Domains

  2014cites this paper
• Termination analysis with recursive calling graphs

  2014cites this paper
• First-Order Formative Rules

  2014cites this paper
• AC-KBO revisited* †

  2014cites this paper
• A unified ordering for termination proving

  2014influential citation
• Verifying and Synthesizing Software with Recursive Functions - (Invited Contribution)

  2014cites this paper
• Automated SAT Encoding for Termination Proofs with Semantic Labelling ∗

  2014cites this paper
• Verifying and Synthesizing Software with

  2014cites this paper
• AC-KBO Revisited

  2014cites this paper
• The Weighted Path Order for Termination of Term Rewriting

  2014cites this paper
• Unifying the Knuth-Bendix, recursive path and polynomial orders

  2013cites this paper
• Propositional Encoding of Constraints over Tree-Shaped Data

  2013cites this paper
• Compact Encoding of Model-Based Diagnosis to Boolean Satisfiability

  2012cites this paper
• SAT encodings: from constraint-based termination analysis to circuit synthesis

  2012cites this paper
• Harnessing First Order Termination Provers Using Higher Order Dependency Pairs

  2011cites this paper