Practical Reasoning Approaches for Web Ontologies and Multi-Agent Systems
Lead Research Organisation:
University of Manchester
Department Name: Computer Science
Abstract
Logical and automated reasoning methods are crucial for web technologies and agent technologies for the intelligent processing of large ontologies, decision making based on knowledge bases of structured data, and formal specification and verification of multi-agent systems.Concerning ontology reasoning the current tableau description logic reasoners used for this purpose have a number of significant shortcomings. These include insufficient expressiveness, suboptimal complexity, over specialisation and incomplete formal treatment. All these are serious issues which need to be tackled and overcome if such systems are to form the backbone ontology reasoning for the semantic web. Concerning reasoning within and about multi-agent systems, in the form of intelligent decision making by agent and the formal specification and verification of agent systems, there exists a plethora of agent logics which have been proposed for this purpose, but almost no implemented reasoning systems for solving satisfiability and validity problems in these logics. This lack of system support is a serious problem.We will use techniques from first-order logic and resolution to develop a resolution framework for reasoning about expressive ontological languages and expressive agent logics. A series of tools will be developed to provide automated support for reasoning tasks in these areas. Principles of benchmarking will be studied, designed and used for empirical investigations of developed technologies and tools.
Organisations
People |
ORCID iD |
| Renate Schmidt (Principal Investigator) |
Publications
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
(2007)
The Semantic Web
Schmidt R
(2012)
The Ackermann approach for modal logic, correspondence theory and second-order reduction
in Journal of Applied Logic
Schmidt R
(2011)
Automated Synthesis of Tableau Calculi
in Logical Methods in Computer Science
Schmidt R
(2007)
On combinations of propositional dynamic logic and doxastic modal logics
in Journal of Logic, Language and Information
Schmidt R
(2014)
Using tableau to decide description logics with full role negation and identity
in ACM Transactions on Computational Logic
Schmidt R
(2009)
A new methodology for developing deduction methods
in Annals of Mathematics and Artificial Intelligence
Schmidt R
(2010)
Simulation and Synthesis of Deduction Calculi
in Electronic Notes in Theoretical Computer Science
| Description | Logical and automated reasoning methods are crucial for web technologies and agent technologies for the intelligent processing of large ontologies, decision making based on knowledge bases of structured data, and formal specification and verification of multi-agent systems. In this joint project between the School of Computer Science at the University of Manchester and the Department of Computer Science at the University of Liverpool the aim was to use techniques from automated reasoning to deve |
| Exploitation Route | The methods developed and results obtained are of interest to any applications requiring automated reasoning, especially areas requiring the intelligent processing of large ontologies, decision making based on knowledge bases of structured data, and formal specification and verification of multi-agent systems. The automated reasoning systems developed as part of this project are freely available for download via the project webpage. |
| Sectors | Digital/Communication/Information Technologies (including Software) |
| URL | http://www.cs.man.ac.uk/~schmidt/womas |
| Description | The developed tableau synthesis framework has provided a brand new and automatic way of developing tableau algorithms. Combined with the new blocking technique it gives us a methodology for solving problems in expressive logics, for which so far it has not been known how to use tableau methods as decision procedures. As a consequence, for the first time non-specialists are able to easily devise reasoning algorithms for applications requiring logical reasoning. This is useful in all scientific disciplines and commercial applications where practical reasoning algorithms are needed. The results have provided the foundation for research on automatic prover generation (a completely new and promising research direction). |
| First Year Of Impact | 2010 |
| Sector | Digital/Communication/Information Technologies (including Software) |
| Impact Types | Economic |
| Title | MetTeL Version 1 |
| Description | A generic tableau prover incorporating the main features of the newly developed tableau synthesis framework. |
| Type Of Technology | Software |
| Year Produced | 2007 |
| Impact | MetTeL Version 1 is a logic-independent inference engine allowing users to define tableau rules for fixed modal-type languages. It provides the first implementation of a tableau prover for ALBOid, a very expressive description logic. |
| URL | http://www.mettel-prover.org/downloads/mettel-1.0-197.tar.gz |
| Title | SPASS 3.0 |
| Description | A resolution prover for full sorted first-order logic with equality, sorted clause logic with equality. The new release now also supports numerous traditional modal logics, dynamic modal logics and description logics. |
| Type Of Technology | Software |
| Year Produced | 2007 |
| Open Source License? | Yes |
| Impact | The SPASS prover was enhanced to handle not only first-order (clause) logic, put also several modal logics and description logics, and the relational calculus. By-products are a few new parameter settings and conversion techniques. |
| URL | http://www.spass-prover.org/ |
| Title | SPASS-tab |
| Description | An adaptation of SPASS, which translates first-order resolution proofs into modal tableau proofs and first-order models into modal models. |
| Type Of Technology | Software |
| Year Produced | 2009 |
| Open Source License? | Yes |
| Impact | This is a proof-of-concept implementation showing that a deduction approach seemingly very different than resolution can be realised. |
| URL | http://www.cs.man.ac.uk/~schmidt/spass-tab/ |