Sufficient completeness verification for conditional and constrained TRS
From MaRDI portal
Publication:420848
DOI10.1016/j.jal.2011.09.001zbMath1279.68228OpenAlexW2141421333MaRDI QIDQ420848
Adel Bouhoula, Florent Jacquemard
Publication date: 23 May 2012
Published in: Journal of Applied Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jal.2011.09.001
Related Items (5)
Rewriting modulo SMT and open system analysis ⋮ On transforming cut- and quantifier-free cyclic proofs into rewriting-induction proofs ⋮ Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems ⋮ Incremental Proofs of Termination, Confluence and Sufficient Completeness of OBJ Specifications ⋮ Proving weak properties of rewriting
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness
- Using induction and rewriting to verify and complete parameterized specifications
- Proofs by induction in equational theories with constructors
- On ground-confluence of term rewriting systems
- On sufficient-completeness and related properties of term rewriting systems
- Simplifying conditional term rewriting systems: Unification, termination and confluence
- The algebraic specification of abstract data types
- Tree automata with one memory set constraints and cryptographic protocols
- Automata-driven automated induction
- Ground reducibility is EXPTIME-complete
- Implicit induction in conditional theories
- Automata for reduction properties solving
- Specification and proof in membership equational logic
- Sufficient-completeness, ground-reducibility and their complexity
- MTT: The Maude Termination Tool (System Description)
- Automated Induction with Constrained Tree Automata
- Term Rewriting and Applications
This page was built for publication: Sufficient completeness verification for conditional and constrained TRS
