Implicates and reduction techniques for temporal logics

Abstract

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