Title
Refinement trees: calculi, tools, and applications
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.
Year
DOI
Venue
2011
10.1007/978-3-642-22944-2_11
CALCO
Keywords
Field
DocType
heterogeneous tool set,present proof calculus,conservativity checker,model finder,refinement tree,formal development,first-order ontology
Discrete mathematics,Ontology,Computer science,Correctness,Theoretical computer science,Branching (version control)
Conference
Citations 
PageRank 
References 
2
0.42
12
Authors
2
Name
Order
Citations
PageRank
Mihai Codescu18912.58
Till Mossakowski2105290.11