Frontiers of Combining Systems

DOI10.1007/11559306zbMath1171.68714OpenAlexW4205914269MaRDI QIDQ5491901

René Thiemann, Peter Schneider-Kamp, Jürgen Giesl

Publication date: 10 October 2006

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

Full work available at URL: https://doi.org/10.1007/11559306

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (31)

Analyzing program termination and complexity automatically with \textsf{AProVE} ⋮ mu-term: Verify Termination Properties Automatically (System Description) ⋮ Harnessing First Order Termination Provers Using Higher Order Dependency Pairs ⋮ Generalized and Formalized Uncurrying ⋮ The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors ⋮ KBO orientability ⋮ Certification of Termination Proofs Using CeTA ⋮ SAT solving for termination proofs with recursive path orders and dependency pairs ⋮ Uncurrying for termination and complexity ⋮ Lower bounds for runtime complexity of term rewriting ⋮ Mechanizing and improving dependency pairs ⋮ Flow analysis of lazy higher-order functional programs ⋮ Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures ⋮ Deciding Innermost Loops ⋮ Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems ⋮ Enhancing dependency pair method using strong computability in simply-typed term rewriting ⋮ Loop detection in term rewriting using the eliminating unfoldings ⋮ Use of logical models for proving infeasibility in term rewriting ⋮ Typing termination in a higher-order concurrent imperative language ⋮ Characterizing and proving operational termination of deterministic conditional term rewriting systems ⋮ Proving operational termination of membership equational programs ⋮ From Outermost Termination to Innermost Termination ⋮ Beyond Dependency Graphs ⋮ Context-sensitive dependency pairs ⋮ CSI – A Confluence Tool ⋮ Loops under Strategies ⋮ Dependency Pairs and Polynomial Path Orders ⋮ Argument Filterings and Usable Rules for Simply Typed Dependency Pairs ⋮ Match-bounds revisited ⋮ Increasing interpretations ⋮ Termination of Lazy Rewriting Revisited

Uses Software

• Tyrolean
• AProVE
• Matchbox

This page was built for publication: Frontiers of Combining Systems