Edinburgh Research Archive >
Informatics, School of >
Informatics thesis and dissertation collection >
Please use this identifier to cite or link to this item:
|Title: ||Automated Reasoning in Quantified Modal and Temporal Logics|
|Authors: ||Castellini, Claudio|
|Supervisor(s): ||Smaill, Alan|
|Issue Date: ||Jun-2005|
|Publisher: ||University of Edinburgh. College of Science and Engineering. School of Informatics.|
|Abstract: ||This thesis is about automated reasoning in quantified modal and temporal logics, with an application to formal methods. Quantified modal and temporal logics are extensions of classical first-order logic in which the notion of truth is extended to take into account its necessity or equivalently, in the temporal setting, its persistence through time.
Due to their high complexity, these logics are less widely known and studied than their propositional counterparts. Moreover, little so far is known about their mechanisability and usefulness for formal methods.
The relevant contributions of this thesis are threefold: firstly, we devise a sound and complete set of sequent calculi for quantified modal logics; secondly, we extend the approach to the quantified temporal logic of linear, discrete time and develop a framework for doing automated reasoning via Proof Planning in it; thirdly, we show a set of experimental results obtained by applying the framework to the problem of
Feature Interactions in telecommunication systems.
These results indicate that (a) the problem can be concisely and effectively modeled in the aforementioned logic, (b) proof planning actually captures common structures in the related proofs, and (c) the approach is viable also from the point of view of efficiency.|
|Description: ||Centre for Intelligent Systems and their Applications|
|Sponsor(s): ||Engineering and Physical Sciences Research Council (EPSRC)|
|Appears in Collections:||Informatics thesis and dissertation collection|
Items in ERA are protected by copyright, with all rights reserved, unless otherwise indicated.