We present an overview on Temporal Logic Programming under the perspective of its application for Knowledge Representation and declarative problem solving. Such programs are the result of combining usual rules with temporal modal operators, as in Linear-time Temporal Logic (LTL). We focus on recent results of the non-monotonic formalism called Temporal Equilibrium Logic (TEL) that is defined for the full syntax of LTL, but performs a model selection criterion based on Equilibrium Logic, a well known logical characterization of Answer Set Programming (ASP). We obtain a proper extension of the stable models semantics for the general case of arbitrary temporal formulas. We recall the basic definitions for TEL and its monotonic basis, the temporal logic of Here-and-There (THT), and study the differences between infinite and finite traces. We also provide other useful results, such as the translation into other formalisms like Quantified Equilibrium Logic or Second-order LTL, and some techniques for computing temporal stable models based on automata. In a second part, we focus on practical aspects, defining a syntactic fragment called temporal logic programs closer to ASP, and explain how this has been exploited in the construction of the solver TELINGO.

One of the current problems in decision support from Artifici al Intelligence systems is the lack of explanations. When a system is making decisions in critical co ntexts and those decisions may have an impact on people's life like in the medical or legal domains, then explanations turn to be crucial, especially if we expect that a domain expert relies on the obtaine d answers. One of these situations from the medical domain where explanations have a crucial role is the process of donor-patient matching in an organ transplantation unit. This process starts when a new o rgan is received and consists in selecting a patient among those included in a waiting list for transplan tation. The transplantation unit is expected to follow an objective policy that takes into account medica l parameters and is experimentally supported by the existing records, but more importantly, this decisio n must be easily reproducible and explicable in a comprehensible way for other agents potentially involved, since it may have life-critical consequences at personal, medical and legal levels. Typically, this deci sion is taken in terms of a set of numerical weights (the impact of weights variation is studied in [7]). Although different classification systems based on Artificial Neural Networks (ANNs) are being propose d (see for instance [2] for the case of liver transplantation) their decisions rely on a black box whose b ehaviour is not explicable in human terms. In this paper, we present a rule interpreter, web-liver, designed for assisting the medical experts in the donor-patient matching of a liver transplantation un it, using the case scenario from the Digestive F. Aguado et al.

A common feature in Answer Set Programming is the use of a seco nd negation, stronger than default negation and sometimes called explicit, strong or classica l negation. This explicit negation is normally used in front of atoms, rather than allowing its use as a regular op erator. In this paper we consider the arbitrary combination of explicit negation with nested expressions, as those defined by Lifschitz, Tang and Turner. We extend the concept of reduct for this new syntax and then pr ove that it can be captured by an extension of Equilibrium Logic with this second negation. We study som e properties of this variant and compare to the already known combination of Equilibrium Logic with Nel son's strong negation.