Sufficient completeness verification for conditional and constrained TRS
From MaRDI portal
Publication:420848
DOI10.1016/J.JAL.2011.09.001zbMATH Open1279.68228OpenAlexW2141421333MaRDI QIDQ420848FDOQ420848
Authors: 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
Recommendations
Cites Work
- Title not available (Why is that?)
- MTT: The Maude Termination Tool (System Description)
- Automated Induction with Constrained Tree Automata
- 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
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Term Rewriting and Applications
- 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
Cited In (10)
- Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems
- Proving weak properties of rewriting
- Title not available (Why is that?)
- On sufficient completeness of conditional specifications
- Constructors, sufficient completeness, and deadlock freedom of rewrite theories
- Incremental Proofs of Termination, Confluence and Sufficient Completeness of OBJ Specifications
- Sufficient-completeness, ground-reducibility and their complexity
- Rewriting modulo SMT and open system analysis
- On transforming cut- and quantifier-free cyclic proofs into rewriting-induction proofs
- Completion for constrained term rewriting systems
Uses Software
This page was built for publication: Sufficient completeness verification for conditional and constrained TRS
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q420848)
