Using well-founded relations for proving operational termination

DOI10.1007/s10817-019-09514-2zbMath1468.03034OpenAlexW2912692218MaRDI QIDQ2303238

Salvador Lucas

Publication date: 3 March 2020

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

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

zbMATH Keywords

program analysisoperational terminationwell-foundednesslogical modelsdeclarative languages

Mathematics Subject Classification ID

Logic in computer science (03B70) Grammars and rewriting systems (68Q42) Structure of proofs (03F07)

Related Items (4)

Automatically Proving and Disproving Feasibility Conditions ⋮ Local confluence of conditional and generalized term rewriting systems ⋮ The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques ⋮ Automatic generation of logical models with AGES

Uses Software

• Prover9
• Maude
• Mace4
• Tyrolean
• AProVE

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Dependency pairs for proving termination properties of conditional term rewriting systems
• Characterizing and proving operational termination of deterministic conditional term rewriting systems
• Mechanizing and improving dependency pairs
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Operational termination of conditional term rewriting systems
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• Sentence-normalized conditional narrowing modulo in rewriting logic and Maude
• Automatic synthesis of logical models for order-sorted first-order theories
• Use of logical models for proving infeasibility in term rewriting
• Context-sensitive rewriting strategies
• Termination of term rewriting using dependency pairs
• Proving operational termination of membership equational programs
• Methods for Proving Termination of Rewriting-based Programming Languages by Transformation
• Use of Logical Models for Proving Operational Termination in General Logics
• Proving Termination Properties with mu-term
• Computationally Equivalent Elimination of Conditions
• Proving innermost normalisation automatically
• Operational Termination of Conditional Rewriting with Built-in Numbers and Semantic Data Structures
• One-Path Reachability Logic
• Logic for Programming, Artificial Intelligence, and Reasoning
• Verification of Erlang processes by dependency pairs

This page was built for publication: Using well-founded relations for proving operational termination