An automated reasoning method on first-order tense logic

The paper investigates the automated reasoning method on a first-order lattice-valued non-classical logic. Firstly, a new kind of literals, called generalized literals, are defined by introducing tense operators. Then some conclusions are discussed and drawn about the relation between base literals and generalized literals. Afterwards, generalized Skölem standard form and Herbrand-field are proposed. Based on these concepts and results, finally, a new resolution principle is introduced and resolution-based automation deduction theorem on this first-order lattice valued tense logic is provided. The proposed work places theoretical support for automated reasoning associated with imprecision and incomparability under dynamic environment.