Commonsense temporal reasoning is full of situations that require drawing default conclusions, since we rarely have all the information available. Unfortunately, most modal temporal logics cannot accommodate default reasoning, since they typically deal with a monotonic inference relation. On the other hand, non-monotonic approaches are very expensive and their treatment of time is not so well delimited and studied as in modal logic.

Temporal Equilibrium Logic (TEL) is the first non-monotonic temporal logic which fully covers the syntax of some standard modal temporal approach without requiring further constructions. TEL shares the syntax of Linear-time Temporal Logic (LTL) (first proposed by Arthur Prior and later extended by Hans Kamp) which has become one of the simplest, most used and best known temporal logics in Theoretical Computer Science.

Although TEL had been already defined, few results were known about its fundamental properties and nothing at all on potential computational methods that could be applied for practical purposes. This situation unfavourably contrasted with the huge body of knowledge available for LTL, both in well-known formal properties and in computing methods with practical implementations. In this thesis we have mostly filled this gap, following a research program that has systematically analysed different essential properties of TEL and, simultaneously, built computational tools for its practical application. As an overall, this thesis collects a corpus of results that constitutes a significant breakthrough in the knowledge about TEL.