Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs

DOI10.1007/978-3-031-38499-8_20MaRDI QIDQ6492754zbMATH OpenFDO

Authors Jürgen Giesl

Publication date 26 April 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-38499-8_20

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A linear operational semantics for termination and complexity analysis of ISO prolog
• Analyzing innermost runtime complexity of term rewriting by dependency pairs
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Automated Expected Amortised Cost Analysis of Probabilistic Data Structures
• Automated termination analysis of Java bytecode by term rewriting
• Automated termination analysis of polynomial probabilistic programs
• Automating the dependency pair method
• Computing expected runtimes for constant probability programs
• Expected Runtime Analyis by Program Verification
• From Jinja bytecode to term rewriting: a complexity reflecting transformation
• scientific article; zbMATH DE number 2090077 (Why is no real title available?)
• Inferring expected runtimes of probabilistic integer programs using expected sizes
• Logic for Programming, Artificial Intelligence, and Reasoning
• Mechanizing and improving dependency pairs
• mu-term: Verify Termination Properties Automatically (System Description)
• Nagoya termination tool
• On probabilistic term rewriting
• Orderings for term-rewriting systems
• Probabilistic rewriting and asymptotic behaviour: on termination and unique normal forms
• Probabilistic termination by monadic affine sized typing
• Probabilistic termination: soundness, completeness, and compositionality
• Term Rewriting and All That
• Term Rewriting and Applications
• Termination Analysis of Probabilistic Programs with Martingales
• Termination of term rewriting using dependency pairs
• Weakest precondition reasoning for expected runtimes of randomized algorithms

Cited in

(3)

• From innermost to full almost-sure termination of probabilistic term rewriting
• From innermost to full probabilistic term rewriting: almost-sure termination, complexity, and modularity
• A dependency pair framework for relative termination of term rewriting

This page was built for publication: Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs

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