Interpolation in practical formal development

DOI10.1093/JIGPAL/9.2.231MaRDI QIDQ2716926zbMATH OpenOpenAlexFDO

Authors Theo Dimitrakos, Tim Maibaum, J. Bicarregui, Dov Gabbay

Publication date 11 March 2002

Published in Logic Journal of the IGPL (Search for Journal in Brave)

Full work available at URL https://semanticscholar.org/paper/b3177fd6186b71b0da9d8a9d6524fe97a92b3a7e, http://purl.org/net/epubs/work/49250969

zbMATH Keywords

formal developmentinterpolantsmodularization

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

The authors indicate the importance of the presence of interpolants in the logic for expressing specifications of software. They recall some results linking interpolation to important properties such as presentation modularity and proof decomposition. They explain the role of interpolants and modularization for promoting property enrichment from subsystems to systems and for controlling interference. They also advocate the need of reengineering specification logics so that special kinds of interpolants, called uniform interpolants, become available.

Recommendations

• Interpolation and model checking
• Interpolation in computing science: The semantics of modularization
• scientific article; zbMATH DE number 23769
• Interpolation method for multicomponent sequent calculi
• Interpolation in extensions of first-order logic
• scientific article; zbMATH DE number 3876457
• Interpolation with decidable fixpoint logics
• Complete instantiation-based interpolation
• Complete instantiation-based interpolation
• Foundations of Software Science and Computation Structures

Cited in

(14)

• A semantic approach to interpolation
• Interpolation in computing science: The semantics of modularization
• Generalised graded interpolation
• Craig interpolation in the presence of unreliable connectives
• FAME(Q): an automated tool for forgetting in description logics with qualified number restrictions
• Preservation of Craig interpolation by the product of matrix logics
• Definability and interpolation in non-classical logics
• Interpolation for predefined types
• Interpolation in modal logic
• Complete instantiation-based interpolation
• (Heterogeneous) structured specifications in logics without interpolation
• The Craig interpolation property in first-order Gödel logic
• An institution-independent proof of the Robinson consistency theorem
• Common knowledge does not have the Beth property

This page was built for publication: Interpolation in practical formal development

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