EPSRC Reference: |
GR/M29221/01 |
Title: |
PRODUCTS OF MODAL LOGICS AND DECIDABLE FRAGMENTS OF CLASSICAL LOGIC |
Principal Investigator: |
Gabbay, Professor D |
Other Investigators: |
|
Researcher Co-Investigators: |
|
Project Partners: |
|
Department: |
Computer Science |
Organisation: |
Kings College London |
Scheme: |
Standard Research (Pre-FEC) |
Starts: |
01 July 1998 |
Ends: |
30 June 1999 |
Value (£): |
14,000
|
EPSRC Research Topic Classifications: |
Fundamentals of Computing |
|
|
EPSRC Industrial Sector Classifications: |
No relevance to Underpinning Sectors |
|
|
Related Grants: |
|
Panel History: |
|
Summary on Grant Application Form |
Classical Logic and multimodal logics are the two main logics with wide application in computer science. Classical logic is expressive, but undecidable. Multimodal logics usually are decidable, but not as expressive. Especially useful among the multimodal logics are products (introduced by Shehtman). The recent work of Gabbay and Shehtman established a better link between the two kinds of logics leading to larger decidable fragments of classical logic. During the visit, decision problem for products of different well-known modal systems will be studied. For this purpose the modal logic methods, such as finite depth, normal forms, filtrations, mosaics etc, will be further developed. The results obtained for modal products will be transferred to fragments of classical first-order logic with relativized quantifiers. In particular, the results on the finite model property will be applied to finite model theory. The recent results on relativized quantifiers (on guarded Fragment, studied by Amsterdam - Budapest co-operation) will be further improved to incorporate new results on modal products. Many-dimensional temporal logics will be included into the modal product theory as well. Different axiomatic systems modelling space-time behaviour in terms of modal logic will be proposed, with a view for robotics applications. The general theory of products will be applied to obtain decision procedures for these systems.
|
Key Findings |
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
Potential use in non-academic contexts |
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
Impacts |
Description |
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk |
Summary |
|
Date Materialised |
|
|
Sectors submitted by the Researcher |
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
Project URL: |
|
Further Information: |
|
Organisation Website: |
|