(a, t) - Resolution Principle Based on Lattice-Valued Tense Propositional Logic LTP(X)

In this paper, four tense operators E, F, G, H, are introduced into LP(X), then extend a lattice-valued propositional logic system to lattice-valued tense propositional logic system LTP(X). In this system, some definitions including generalized literal, T-skolem standard form, are given out. Based on these work, several conclusions about resolution deduction are got. Finally, alpha-soundness theorem of resolution principle is proved.