Modal Temporal Logic

We have developed an efficient executional model for an interval based linear modal temporal logic. The efficiency of the execution stems from viewing temporal evaluations as temporal constraints on intervals end points and generating maximal intervals at which formulae holds. This executable logic was used to develop a demonstrator PAYE tax system. The research is being extended to include branching time flow. Investigation of theorem proving for modal temporal logic led to the development of a non-clausal theorem prover for first order temporal logic. The theorem prover uses heuristics generated by a neural network which examines patterns of modal and classical connectives in formulae. These heuristics are then used to prune the proof tree and for the selection of the most appropriate inference rule to apply next. Early results are very promising and further research is continuing to improve the pattern classification of neural network, generation of heuristics and proof strategies.