Use of logical models for proving operational termination in general logics

DOI10.1007/978-3-319-44802-2_2MaRDI QIDQ2827835zbMATH OpenOpenAlexFDO

Authors 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

abstractionlogical modelsoperational termination

Mathematics Subject Classification ID

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

Recommendations

• Localized operational termination in general logics
• Using well-founded relations for proving operational termination
• Proving correctness and completeness of normal programs – a declarative approach
• On modular termination proofs of general logic programs
• -Universal termination of logic programs

Cites work

• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• scientific article; zbMATH DE number 4018380 (Why is no real title available?)
• scientific article; zbMATH DE number 1189278 (Why is no real title available?)
• scientific article; zbMATH DE number 50939 (Why is no real title available?)
• Operational termination of conditional term rewriting systems
• Operational termination of membership equational programs: the order-sorted way
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• Polynomials over the reals in proofs of termination : from theory to practice
• Proving operational termination of membership equational programs
• Proving termination properties with \textsc{mu-term}
• Revisiting matrix interpretations for proving termination of term rewriting

Cited in

(4)

• Automatic synthesis of logical models for order-sorted first-order theories
• Use of logical models for proving infeasibility in term rewriting
• Using well-founded relations for proving operational termination
• Localized operational termination in general logics

Describes a project that uses

Uses Software

• Maude

This page was built for publication: Use of logical models for proving operational termination in general logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2827835)