| Publication type: |
Article in Proceedings |
| Author: |
Mihai Codescu, Till Mossakowski |
| Editor: |
Andrea Corradini, Bartek Klin |
| Title: |
Refinement trees: calculi, tools and applications |
| Book / Collection title: |
Algebra and Coalgebra in Computer Science, CALCO'11 |
| Volume: |
6859 |
| Page(s): |
145 – 160 |
| Series: |
Lecture Notes in Computer Science |
| Year published: |
2011 |
| Publisher: |
Springer |
| 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.
|
| Internet: |
http://dx.doi.org/10.1007/978-3-642-22944-2_11 |
| PDF Version: |
https://svn.omdoc.org/repos/latin/public/refinement-calco2011.pdf |
| Keywords: |
refinement architectural specification institution proof calculus consistency |
| Status: |
Reviewed |
| Last updated: |
30. 01. 2012 |
