Overseas Visit in Automated Model Building

The projects requests funding for a short overseas visit of the PI to NICTA (Canberra), Australia's ICT Research Centre of Excellence, in order to work together with Prof Peter Baumgartner and Dr Rajeev Gore on the topic of automated model building. Prof Baumgartner is a leading expert in the area of automated reasoning with special expertise relating to model building and first-order theorem proving. He has extensive expertise in instantiation methods, first-order Davis-Putnam, model generation and the development and implementation of theorem provers. Dr Gore is a well-known expert in proof theory and non-classical logic, including tableaux methods, regular grammar modal logics and description logics.The project has two main objectives: (i) Investigating the paradigm of bottom-up model generation methods and work on the development of stronger, more efficient and more general model generation methods. (ii) Exploiting the developed techniques for devising and implementing novel model generation and automated reasoning methodologies for description logics and modal-type logics.Model building is hugely important for testing, validation and verification purposes, for instance, software testing, testing of multi-agent systems, validation of ontologies, verification of ontology reasoners. They can be used for fault analysis, verification of systems, and they can be used for validation of data models.