Overseas Visit in Automated Model Building
Lead Research Organisation:
University of Manchester
Department Name: Computer Science
Abstract
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.
Organisations
People |
ORCID iD |
Renate Schmidt (Principal Investigator) |
Publications
Schmidt R
(2009)
A new methodology for developing deduction methods
in Annals of Mathematics and Artificial Intelligence
Khodadadi M
(2013)
Automated Reasoning with Analytic Tableaux and Related Methods
Renate A. Schmidt (Author)
(2014)
Axiomatic and tableau-based reasoning for Kt(H,R)
in Advances in Modal Logic
Schmidt R
(2014)
Using tableau to decide description logics with full role negation and identity
in ACM Transactions on Computational Logic
Baumgartner P
(2019)
Blocking and Other Enhancements for Bottom-Up Model Generation Methods
in Journal of Automated Reasoning
Baumgartner, Peter
Blocking and Other Enhancements for Bottom-Up Model Generation Methods
Description | The project provided funding for a three month 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. 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 analys |
Sectors | Digital/Communication/Information Technologies (including Software) |
Title | MSPASS-yarralumla |
Description | Improvements and extensions to the YARRALUMLA system and the MSPASS theorem prover. A first-order generalisation of the unrestricted blocking rule was developed and implemented in MSPASS . The user interface was improved giving the user more control over the transformations that are performed in MSPASS . A new variation of the splitting rule and new strategies were implemented in order to facilitate the restricted and unrestricted blocking mechanisms needed for simulating bottom-up model generation procedures. A testing framework was set up to for doing experiments with theorem provers using the various combinations of settings and techniques. Experiments were conducted on problems of the TPTP benchmark suite of problems in first-order logic and first-order clause logic. Further experiments are currently being undertaken with description logic knowledge bases and web ontologies. The properties of the models generated by the different combinations of techniques were investigated. |
Type Of Technology | Software |
Year Produced | 2008 |
Impact | The work is highly cited and relevant to many applications where reasoning is used because of the introduction of a generalised, very powerful blocking principle. Blocking is absolutely indespensible in systems utilizing tableau-like reasoning and model-generation techniques for guaranteeing termination and avoiding indefinite computations. |
URL | http://users.rsise.anu.edu.au/~baumgart/systems/yarralumla |