Temporal resolution: removing irrelevant information

The generation of too much information prohibits efficient resolution proof search in classical logics. Hence subsumption is used to discard redundant information and strategies have been developed to guide the proof search avoiding irrelevant information. The extension of the resolution method to temporal logics, for example that by Fisher (1991) for propositional linear-time temporal logics, further magnifies this problem. We provide an algorithm to efficiently remove irrelevant information prior to the application of Fisher´s temporal resolution rule, show that it retains the completeness of the temporal resolution system and demonstrate its efficiency on a set of examples