CiME

swMATH9970MaRDI QIDQ21947FDOQ21947

Author name not available (Why is that?)

Cited In (38)

• Intruder deduction problem for locally stable theories with normal forms and inverses
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Tuple interpretations for termination of term rewriting
• Towards Rewriting in Coq
• Title not available (Why is that?)
• Certification of Proving Termination of Term Rewriting by Matrix Interpretations
• Certified Rule Labeling
• Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof
• Proving operational termination of membership equational programs
• Title not available (Why is that?)
• Rewrite systems for natural, integral, and rational arithmetic
• Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
• Automated Deduction – CADE-20
• Polynomials over the reals in proofs of termination : from theory to practice
• Slothrop: Knuth-Bendix Completion with a Modern Termination Checker
• On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting
• Proving termination of context-sensitive rewriting by transformation
• Term Rewriting and Applications
• Certifying a Termination Criterion Based on Graphs, without Graphs
• Mechanically proving termination using polynomial interpretations
• Title not available (Why is that?)
• Computationally sound implementations of equational theories against passive adversaries
• Proving termination of nonlinear command sequences
• Structural Analysis of Narratives with the Coq Proof Assistant
• Automatically proving termination and memory safety for programs with pointer arithmetic
• Sufficient completeness verification for conditional and constrained TRS
• Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems
• Proving Termination of Programs Automatically with AProVE
• A Lambda-Free Higher-Order Recursive Path Order
• On tree automata that certify termination of left-linear term rewriting systems
• Modular and incremental proofs of AC-termination
• Formally proving size optimality of sorting networks
• Title not available (Why is that?)
• CSI – A Confluence Tool
• Termination of just/fair computations in term rewriting
• Rewrite rules for \(\mathrm{CTL}^\ast\)
• Termination of string rewriting proved automatically
• Rewriting Techniques and Applications

This page was built for software: CiME