Abstract
We recall a language for refinement and branching of formal developments. We introduce a notion of refinement tree and present proof calculi for checking correctness of refinements as well as their consistency. Both calculi have been implemented in the Heterogeneous Tool Set (Hets), and have been integrated with other tools like model finders and conservativity checkers. This technique has already been applied for showing the consistency of a first-order ontology that is too large to be tackled directly by model finders. © 2011 Springer-Verlag.
Cite
CITATION STYLE
Codescu, M., & Mossakowski, T. (2011). Refinement trees: Calculi, tools, and applications. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6859 LNCS, pp. 145–160). https://doi.org/10.1007/978-3-642-22944-2_11
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
