Implicates and reduction techniques for temporal logics

Reduction strategies are introduced for the future fragment of a temporal propositional logic on linear discrete time, named FNext. These reductions are based on the information collected from the syntactic structure of the formula, which allows the development of efficient strategies to decrease the 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, allow to improve the performance of any automated theorem prover.