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

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