scientific article; zbMATH DE number 7359426

DOI10.4230/LIPIcs.FSCD.2018.30zbMath1462.68098MaRDI QIDQ4993362

Sarah Winkler, Aart Middeldorp

Publication date: 15 June 2021

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

theorem provingcompletionautomationconstrained rewriting

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (4)

Operationally-based program equivalence proofs using LCTRSs ⋮ Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting ⋮ Extending Maximal Completion (Invited Talk) ⋮ Runtime complexity analysis of logically constrained rewriting

Uses Software

• z3
• Slothrop
• Ctrl

Cites Work

• Term Rewriting with Logical Constraints
• A New and Formalized Proof of Abstract Completion
• Constrained Term Rewriting tooL
• Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
• Slothrop: Knuth-Bendix Completion with a Modern Termination Checker
• Proving Termination of Integer Term Rewriting
• Algebraic data integration
• Verifying Procedural Programs via Constrained Rewriting Induction
• Unnamed Item
• Unnamed Item

This page was built for publication: