Use of logical models for proving infeasibility in term rewriting

DOI10.1016/j.ipl.2018.04.002zbMath1477.68140OpenAlexW2799786954MaRDI QIDQ1751429

Raúl Gutiérrez, Salvador Lucas

Publication date: 25 May 2018

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/10251/121414

zbMATH Keywords

formal methodsconfluenceoperational terminationconditional rewriting

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items

Automatically Proving and Disproving Feasibility Conditions ⋮ mu-term: Verify Termination Properties Automatically (System Description) ⋮ The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors ⋮ The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques ⋮ Proving semantic properties as first-order satisfiability ⋮ Using well-founded relations for proving operational termination ⋮ Automatic generation of logical models with AGES ⋮ Term orderings for non-reachability of (conditional) rewriting

Uses Software

• Prover9
• Mace4
• Conditional Confluence

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Dependency pairs for proving termination properties of conditional term rewriting systems
• Normal forms and normal theories in conditional rewriting
• Operational termination of conditional term rewriting systems
• Automatic synthesis of logical models for order-sorted first-order theories
• Analysis of rewriting-based systems as first-order theories
• Termination of term rewriting using dependency pairs
• Disproving Confluence of Term Rewriting Systems by Interpretation and Ordering
• 2D Dependency Pairs for Proving Operational Termination of CTRSs
• Extending the 2D Dependency Pair Framework for Conditional Term Rewriting Systems
• Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion
• Frontiers of Combining Systems