Use of Logical Models for Proving Operational Termination in General Logics

DOI10.1007/978-3-319-44802-2_2zbMath1367.68068OpenAlexW2509903391MaRDI QIDQ2827835

Salvador Lucas

Publication date: 21 October 2016

Published in: Rewriting Logic and Its Applications (Search for Journal in Brave)

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

zbMATH Keywords

abstractionoperational terminationlogical models

Mathematics Subject Classification ID

Logic in computer science (03B70) Grammars and rewriting systems (68Q42) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (2)

Automatic synthesis of logical models for order-sorted first-order theories ⋮ Using well-founded relations for proving operational termination

Uses Software

• Maude

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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
• Proving operational termination of membership equational programs
• Proving Termination Properties with mu-term
• Operational Termination of Membership Equational Programs: the Order-Sorted Way
• Polynomials over the reals in proofs of termination : from theory to practice
• Revisiting Matrix Interpretations for Proving Termination of Term Rewriting

This page was built for publication: Use of Logical Models for Proving Operational Termination in General Logics