## Practical Reasoning Approaches for Web Ontologies and Multi-Agent Systems

EPSRC reseach grant EP/D060451/1Start date: 1 December 2006

End date: 30 November 2009

Principal investigator: Ullrich Hustadt

Co-investigator: Clare Dixon

PhD student: Lan Zhang

**Summary**

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 (Zhang, Hustadt, and Dixon, 2009). 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 (Zhang, Hustadt, and Dixon, 2010). CTL-RP is the first implemented resolution system for CTL. In a system comparision 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 (Ludwig and Hustadt, 2009c). 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 (Ludwig and Hustadt, 2009a). We have implemented the semi-decision procedure in the theorem prover TSPASS (Ludwig and Hustadt, 2010). 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 (Dixon, Fisher, and Konev, 2007a, Dixon, Fisher, and Konev, 2007b). The tableau calculus was further extended to a combination of TLX with epistemic logic (Dixon, Fisher, and Konev, 2009). A number of applications of TLX have been investigated, in particular, the specification of robot swarms (Behdenna, Dixon, and Fisher, 2010).

**Bibliography**

**A. Behdenna, C. Dixon, and M. Fisher (2010):**

*Deductive Verification of Simple Foraging Robotic Behaviours.*International Journal of Intelligent Computing and Cybernetics 2(4):604-643, 2010.

Abstract + PDF (via Emerald Group Publishing).

**C. Dixon, M. Fisher, and and B. Konev (2009):**

*Taming the Complexity of Temporal Epistemic Reasoning.*In S. Ghilardi and R. Sebastiani, editors,

*Proceeding of the Seventh International Symposium on the Frontiers of Combining Systems FRoCoS'09*(Trento, Italy, 16-18 September, 2009). LNAI, Springer 2009.

Abstract + PDF (via Springer).

**C. Dixon, M. Fisher, and B. Konev (2007a):**

*Temporal Logic with Capacity Constraints.*In

*Proceedings of the 6th International Symposium on Frontiers of Combining Systems FroCoS'07*(Liverpool, UK, 10-12 September, 2007). LNAI, Springer 2007.

Abstract + PDF (via Springer).

**C. Dixon, M. Fisher, and and B. Konev (2007b):**

*Tractable Temporal Reasoning.*In

*Proceedings of the Twentieth International Joint Conference on Artificial Intelligence IJCAI-07*(Hyderabad, India, 6-12 September, 2007), pages 318-323.

PDF (via IJCAI Org)

**M. Ludwig and U. Hustadt (2009a)**:

*Redundancy Elimination in Monodic Temporal Reasoning.*In N. Peltier and V. Sofronie-Stokkermans, editors,

*Proceedings of the 7th International Workshop on First-Order Theorem Proving FTP 2009*(Oslo, Norway, July 6-7, 2009).

Abstract, BibTeX, PDF.

**M. Ludwig and U. Hustadt (2009b)**:

*Resolution-Based Model Construction for PLTL.*In C. Lutz and J.-F. Raskin, editors,

*Proceedings of the 16th International Symposium on Temporal Representation and Reasoning TIME-2009*(Brixen-Bressanone, Italy, 23-25 July, 2009). IEEE Computer Society.

Abstract, BibTeX, PDF.

**M. Ludwig and Ullrich Hustadt (2009c)**:

*Fair Derivations in Monodic Temporal Reasoning.*In R. A. Schmidt, editor,

*Proceedings of the 22nd International Conference on Automated Deduction CADE-22*(Montreal, Canada, August 2-7, 2009), pp. 261-276. LNAI 5663, Spinger.

Abstract (via Springer), BibTeX (via DBLP), PDF (via Springer).

**M. Ludwig and U. Hustadt (2010)**:

*Implementing a fair monodic temporal logic prover.*AI Communications 23(2-3):69-96.

Abstract, BibTeX, Abstract + PDF (via IOS Press).

**L. Zhang, U. Hustadt, and C. Dixon (2009)**:

*A Refined Resolution Calculus for CTL.*In R. A. Schmidt, editor,

*Proceedings of the 22nd International Conference on Automated Deduction CADE-22*(Montreal, Canada, August 2-7, 2009), pp. 245-260. LNAI 5663, Spinger.

Abstract (via Springer), BibTeX (via DBLP), PDF (via Springer).

**L. Zhang, U. Hustadt, and C. Dixon (2010)**:

*CTL-RP: A computation tree logic resolution prover.*AI Communications 23(2-3):111-136.

Abstract, BibTeX, Abstract + PDF (IOS Press).

**Software**

- CTL-RP - a C implementation of a theorem prover for Computation Tree Logic (CTL), developed by Lan Zhang. Uses the SPASS theorem prover as `computational engine'.
- TSPASS.
a C implementation of a
*fair*theorem prover for the monodic fragment of first-order linear-time temporal logic over expanding domains based on the temporal resolution calculus, developed by Michel Ludwig. Uses the SPASS theorem prover as `computational engine'.