Automated reasoning in quantified modal and temporal logics

Article type: Research Article

Authors: Castellini, Claudio

Affiliations: LIRA-Lab/DIST, University of Genova, Italy E-mail: [email protected] http://people.liralab.it/drwho

Abstract: This paper is a summary of the author's PhD thesis, concerned with automated reasoning in quantified modal and temporal logics. The relevant contributions are: (i) a sound and complete set of sequent calculi for quantified modal logics is devised; (ii) the approach is extended to the quantified temporal logic of linear, discrete time and a framework for doing automated reasoning via Proof Planning in it is developed; (iii) a set of promising experimental results is shown, obtained by applying the framework to the problem of Feature Interactions in telecommunication systems.

Keywords: Automated reasoning, quantified modal logics, quantified temporal logics, proof planning, feature interactions

Journal: AI Communications, vol. 19, no. 2, pp. 183-185, 2006