We introduce Scheduling MTL (SMTL) an extension of Metric Temporal Logic that supports the specification of complex scheduling problems with repeated and conditional occurrences of activities, and rich temporal relationships among them. We define the syntax and semantics of SMTL, and explore natural restrictions of the language to gain tractability. We also provide an algorithm for finding a schedule to a problem specified as an SMTL formula, and establish a novel equivalence between a fragment of MTL and simple temporal networks, a widely-used formalism in AI temporal planning.

Graphol is a visual language designed to help non-experts to understand and specify ontologies. Our language builds on the Entity-Relationship model, but has a formal semantics and higher expressiveness. Notably, OWL 2 can be completely encoded in Graphol. Thanks to the novel open-source Eddy ontology editor, designers can easily draw Graphol diagrams corresponding to OWL ontologies and export them into standard OWL 2 format. Both Graphol and Eddy have been used in several successful industrial projects and are currently under active development. This paper reports on our more recent progresses.

Algorithms based on first-order knowledge compilation are currently the state-of-the-art for lifted inference. These algorithms typically compile a probabilistic relational model into an intermediate data structure and use it to answer many inference queries. In this paper, we propose compiling a probabilistic relational model directly into a low-level target (e.g., C or C++) program instead of an intermediate data structure and taking advantage of advances in program compilation. Our experiments represent orders of magnitude speedup compared to existing approaches.

We investigate case-based reasoning (CBR) problems where cases are represented by abstract factors and (positive or negative) outcomes, and an outcome for a new case, represented by abstract factors, needs to be established. To this end, we employ abstract argumentation (AA) and propose a novel methodology for CBR, called AA-CBR. The argumentative formulation naturally allows to characterise the computation of an outcome as a dialogical process between a proponent and an opponent, and can also be used to extract explanations for why an outcome for a new case is (not) computed.

Domain-independent planning requires only to specify planning problems in a standard language (e.g. PDDL) in order to utilise planning in some application. Despite a huge advancement in domain-independent planning, some relatively-easy problems are still challenging for existing planning engines. Such an issue can be mitigated by specifying Domain Control Knowledge (DCK) that can provide better guidance for planning engines. In this paper, we introduce transition-based DCK, inspired by Finite State Automata, that is efficient as demonstrated empirically, planner-independent (can be encoded within planning problems) and easy to specify.

In this report from the field we describe jArgSemSAT, a Java re-implementation of ArgSemSAT. We show that jArgSemSAT can be easily integrated in existing argumentation systems (1) as an off-the-shelf, standalone, library; (2) as a Tweety compatible library; and (3) as a fast and robust web service freely available on the Web. The performance section shows that — despite being written in Java — jArgSemSAT is very efficient w.r.t. preferred semantics, which has associated problems with high computational complexity.

We study the logical properties of the (parametric) well-founded fixed point operation. We show that the operation satisfies several, but not all of the equational properties of fixed point operations described by the axioms of iteration theories.

Probabilistic logic programs without negation can have cycles (with a preference for false), but cannot represent all conditional distributions. Probabilistic logic programs with negation can represent arbitrary conditional probabilities, but with cycles they create logical inconsistencies. We show how allowing negative noise probabilities allows us to represent arbitrary conditional probabilities without negations. Noise probabilities for non-exclusive rules are difficult to interpret and unintuitive to manipulate; to alleviate this we define ``probability-strengths'' which provide an intuitive additive algebra for combining rules. For acyclic programs we prove what constraints on the strengths allow for proper distributions on the non-noise variables and allow for all non-extreme distributions to be represented. We show how arbitrary CPDs can be converted into this form in a canonical way. Furthermore, if a joint distribution can be compactly represented by a cyclic program with negations, we show how it can also be compactly represented with negative noise probabilities and no negations. This allows algorithms for exact inference that do not support negations to be applicable to probabilistic logic programs with negations.

We consider knowledge representation (KR) formalisms as collections of finite knowledge bases with a model-theoretic semantics. In this setting, we show that for every KR formalism there is a formalism that characterizes strong equivalence in the original formalism, that is unique up to isomorphism and that has a model theory similar to classical logic.

In the study of argumentation-based reasoning, argument justification has received far more attention than statement justification, often treated as a simple byproduct of the former. As a consequence, counterintuitive results and significant losses of sensitivity can be identified in the treatment of statement justification by otherwise appealing formalisms. To overcome this limitation, we propose to reappraise statement justification as a formalism-independent component. To this purpose, we introduce a novel general model of argumentation-based reasoning based on multiple levels of labellings, one of which is devoted to statement justification. This model is able to encompass several literature proposals as special cases: we illustrate this ability for the case of the ASPIC+ formalism and provide a first example of tunable statement justification in this context.