Practical Reasoning Approaches for Web Ontologies and Multi-Agent Systems
Lead Research Organisation:
University of Liverpool
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
Publications
Zhang L
(2010)
CTL-RP: A computation tree logic resolution prover
in AI Communications
Zhang L
(2009)
Automated Deduction - CADE-22
Zhang L
(2014)
A resolution calculus for the branching-time temporal logic CTL
in ACM Transactions on Computational Logic
Nalon C
(2014)
A Resolution Prover for Coalition Logic
in Electronic Proceedings in Theoretical Computer Science
Nalon C
(2014)
A resolution-based calculus for Coalition Logic
in Journal of Logic and Computation
Ludwig M
(2009)
Resolution-Based Model Construction for PLTL
Ludwig M
(2010)
Implementing a fair monodic temporal logic prover
in AI Communications
Ludwig M
(2009)
Automated Deduction - CADE-22
Dixon C
(2007)
Frontiers of Combining Systems
Dixon C
(2007)
Tractable Temporal Reasoning
in Proceedings of the Twentieth International Joint Conference on Artificial Intelligence (IJCAI-07)
| 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 first-order logic and resolution to develop a resolution framework for reasoning about expressive ontological languages and expressive agent logics. The emphasis of the work at the University of Liverpool was on temporal and agent logics. In particular, we have focussed on four logics, namely, Computation Tree Logic (CTL), the monodic fragment of first-order linear-time temporal logic, Alternating-time Temporal Logic (ATL), and a novel temporal logic with capacity constraints. For CTL we have developed a comprehensive approach to reasoning using resolution-based techniques. The approach requires a polynomial time computable transformation of an arbitrary CTL formula to an equi-satisfiable clausal normal form formulated in an extension of CTL with indexed existential path quantifiers. The calculus itself consists of a set of resolution rules which can be used as the basis for an EXPTIME decision procedure for the satisfiability problem of CTL. We have shown the correctness of the normal form transformation, calculus, and decision procedure. Furthermore, we have implemented the approach in the theorem prover CTL-RP, based on the first-order theorem prover SPASS. CTL-RP is the first implemented resolution system for CTL. In a system comparison that we conducted CTL-RP consistently performed better than other existing provers for CTL. Following an analogous approach, we have developed a fair resolution-based semi-decision procedure for monodic first-order temporal logic. Here, the main advance over previous calculi and procedures is a solution to the fairness problem which tends to be given less attention than it deserves. Such a solution is essential to ensure that an automated procedure can systematically search for a proof for a given formula and is guaranteed to eventually find such a proof if it exists. To further improve the effectiveness of proof search we have investigated redundancy criteria for the resolution calculus underlying the approach. We have implemented the semi-decision procedure in the theorem prover TSPASS. The implementation is again based on the first-order theorem prover SPASS. This work is of particular significance for our project, as monodic first-order temporal logic is a suitable target logic for the translation of combinations of (propositional) temporal logic with modal and description logics, for example, epistemic temporal logic. We have also started to investigate a resolution-based decision procedure for ATL. We have completed work on a transformation of arbitrary ATL formulae into a clausal normal form, which then forms the basis for a resolution-based calculus for ATL. Finally, we have investigated a novel propositional temporal logic, called TLX, where propositions are constrained such that at most N, or exactly M, can hold at any moment in time. Both a resolution calculus and a tableau calculus were developed for this logic. The tableau calculus was further extended to a combination of TLX with epistemic logic. A number of applications of TLX have been investigated, in particular, the specification of robot swarms. An implementation of the tableau calculus for TLX is currently being developed. Overall, the project has resulted in practical proof systems for a variety of temporal and agent logics and also produced several freely available theorem provers for these logics. |
| Exploitation Route | For CTL, we again have developed an ordered resolution calculus and a good implementation of this calculus, CTL-RP. However, CTL-RP performs badly on a class of benchmark formulae derived from business process synthesis (though most other provers do not perform well on these problems either). This is rather disappointing since business process modelling, compliance checking, and synthesis is an interesting application area. We intend to investigate why this is the case. Another line of research in this area are extensions of CTL. We have found a counterexample for the correctness of a resolution calculus for ECTL and ECTL+ by Basukoski and Bolotov. A sound and complete resolution calculus for ECTL and ECTL+ is therefore still an open problem that we intend to investigate. While our work on the project has provided a good foundation for a resolution-based calculus for ATL, this work remains to be completed. In addition, there are many extensions of alternating-time temporal logic that have been suggested in the literature, including extensions with epistemic, counterfactual, commitment operators and extensions to first-order logic, likewise there are many interesting extensions of propositional dynamic logic including combinations of propositional dynamic logic with temporal logics. The downside of some of these extensions is that for some of them not even the model checking problem is decidable. However, this might open the possibility to investigate decidable fragments of such logics. |
| Sectors | Digital/Communication/Information Technologies (including Software) |
| URL | http://cgi.csc.liv.ac.uk/~ullrich/PRAWOMAS/ |
| Description | The project has investigated and developed reasoning method for a range of non-classical logics, in particular, for Computation Tree Logic (CTL), the monodic fragment of first-order linear-time temporal logic, the next-time fragment of Alternating-time Temporal Logic (ATL), and a novel temporal logic with capacity constraints (TLX). For Computation Tree Logic and the monodic fragment of first-order temporal logic we also have developed implementations of our reasoning methods that are available as open source software. Such reasoning methods and the software systems implementing are a necessary basis for the formal verification of software and hardware systems whose specification involves notions of time or actions. An area in which we are particularly active and have used the logics and software systems developed in this project is the specification of robot swarms. We are publicising our results outside the Logic and Automated Reasoning communities and are trying to collaborate with industry in this area. |
| Title | CTL-RP |
| Description | CTL-RP is an implementation of a resolution-based method for Computation Tree Logic (CTL). The method requires a transformation of an arbitrary CTL formula to an equi-satisfiable clausal normal form formulated in an extension of CTL with indexed path formulae. The calculus itself consists of a set of resolution rules which can be used for an EXPTIME decision procedure for the satisfiability problem of CTL. |
| Type Of Technology | Software |
| Year Produced | 2010 |
| Open Source License? | Yes |
| Impact | CTL-RP has shown to be a useful addition to the current set of tools available for CTL. |
| URL | http://cgi.csc.liv.ac.uk/~lan/softwares.html |
| Title | TSPASS |
| Description | TSPASS is an implementation of the ordered fine-grained resolution with selection calculus for monodic first-order temporal logic. Monodic first-order temporal logic is a semi-decidable fragment of first-order temporal logic. In contrast to earlier resolution-based provers for this logic, TSPASS is able to construct fair derivations which means that for any theorem of monodic first-order temporal logic TSPASS is guaranteed to eventually produce a proof. |
| Type Of Technology | Software |
| Year Produced | 2010 |
| Impact | TeMP has been used in a number of contexts in which monodic first-order temporal has been utilised as a specification language. |
| URL | http://lat.inf.tu-dresden.de/~michel/software/tspass/ |