In previous work, the so-called Temporal Equilibrium Logic (TEL) was introduced. This formalism provides an extension of the Answer Set semantics for logic programs to arbitrary theories in the syntax of Linear Temporal Logic. It has already been shown that, in the non-temporal case, arbitrary propositional theories can always be reduced to logic program rules (with disjunction and negation in the head) independently on the context. That is, logic programs constitute a normal form for the non-temporal case. In this paper we show that TEL can be similarly reduced to a normal form consisting of a set of implications (embraced by a necessity operator) quite close to logic program rules. This normal form may be useful both for a practical implementation of TEL and a simpler analysis of theoretical problems.
展开▼
