Refinement trees: calculi, tools and applications

Mihai Codescu, Till Mossakowski

In: Andrea Corradini , Bartek Klin (Hrsg.). Algebra and Coalgebra in Computer Science. Conference on Algebra and Coalgebra in Computer Science (CALCO-11) 4th August 30-September 2 Winchster United Kingdom Seiten 145-160 Lecture Notes in Computer Science (LNCS) 6859 Springer Verlag Berlin 2011.


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.


Weitere Links

refinement-calco2011.pdf (pdf, 451 KB )

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence