Implicates and reduction techniques for temporal logics

Reduction strategies are introduced for the future fragment of a temporal p ropositional logic on linear discrete time, named FNext. These reductions a re based on the information collected from the syntactic structure of the f ormula, which allows the development of efficient strategies to decrease th e size of temporal propositional formulas, viz. new criteria to detect the validity or unsatisfiability of subformulas, and a strong generalisation of the pure literal rule. These results, used as an inner processing step, al low to improve the performance of any automated theorem prover.