Certified Size-Change Termination
From MaRDI portal
Publication:3608789
DOI10.1007/978-3-540-73595-3_34zbMath1213.68571OpenAlexW174766979MaRDI QIDQ3608789
Publication date: 6 March 2009
Published in: Automated Deduction – CADE-21 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-73595-3_34
Related Items
Asymptotically Precise Ranking Functions for Deterministic Size-Change Systems ⋮ Formal verification of termination criteria for first-order recursive functions ⋮ Proving termination by dependency pairs and inductive theorem proving ⋮ Partiality and recursion in interactive theorem provers – an overview ⋮ Partial and nested recursive function definitions in higher-order logic ⋮ Termination Analysis by Dependency Pairs and Inductive Theorem Proving ⋮ Certification of Proving Termination of Term Rewriting by Matrix Interpretations ⋮ All-Termination(T) ⋮ A SAT-Based Approach to Size Change Termination with Global Ranking Functions ⋮ Unnamed Item ⋮ Termination of Isabelle Functions via Termination of Rewriting ⋮ CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates
Uses Software