Linear-Time Temporal Answer Set Programming

In this survey, we present an overview on (Modal) Temporal Logic Programming in view of its application to Knowledge Representation and Declarative Problem Solving. The syntax of this extension of logic programs is the result of combining usual rules with temporal modal operators, as in Linear-time Temporal Logic (LTL). In the paper, we focus on the main recent results of the non-monotonic formalism called Temporal Equilibrium Logic (TEL) that is defined for the full syntax of LTL but involves a model selection criterion based on Equilibrium Logic, a well known logical characterization of Answer Set Programming (ASP). As a result, we obtain a proper extension of the stable models semantics for the general case of temporal formulas in the syntax of LTL. We recall the basic definitions for TEL and its monotonic basis, the temporal logic of Here-and-There (THT), and study the differences between finite and infinite trace length. We also provide further useful results, such as the translation into other formalisms like Quantified Equilibrium Logic and Second-order LTL, and some techniques for computing temporal stable models based on automata constructions. In the remainder of the paper, we focus on practical aspects, defining a syntactic fragment called (modal) temporal logic programs closer to ASP, and explaining how this has been exploited in the construction of the solver telingo, a temporal extension of the well-known ASP solver clingo that uses its incremental solving capabilities.

A Multi-Objective Optimization Model of Health, Safety, and Environmental Risks of Coastal Landfills (A Case Study of the Coastal City of Bandar Abbas)

Introduction: The increasing development of urban life is one of the fundamental challenges in urban management of waste disposal. Solid municipal waste is one of the major problems of governments and urban planners worldwide, especially in coastal cities. This study aimed to design of an advanced linear planning algorithm for coastal landfills with a focus on safety, health, and environmental risks. Method: This is a qualitative study. Multi-objective optimization presents a mathematical model by evaluating the three risks of health, safety, and environment. First, the data were collected using interviews and qualitative analysis, and then in the second stage, the analysis was presented using model linear planning. Results: In the risk assessment of the landfill site, the presented computational results can be found that stable models provide unfavorable answers compared to definitive models. This is a natural issue; since in stable models, the worst case scenario is considered to achieve the optimal solution, and therefore the resulting answers are always unfavorable compared to the definitive models. Conclusion: By analyzing the risk assessment at the landfill site, the causes of accidents and complications resulting from work in this place include unsafe practices or unsafe and unsanitary conditions. In fact, trying to create and improve health, safety, and environmental conditions of landfills in Bandar Abbas city and the increase in reliability confirmed that these two factors are the secondary causes of accidents. The root causes can be considered as a defect in the management system of the landfill site.

DatalogMTL with Negation Under Stable Models Semantics

We introduce negation under stable models semantics in DatalogMTL—a temporal extension of Datalog with metric operators. As a result, we obtain a rule language which combines the power of answer set programming with the temporal dimension provided by metric operators. We show that, in this setting, reasoning becomes undecidable over the rationals and decidable in EXPSPACE in data complexity over the integers. We also show that, if we restrict our attention to forward-propagating programs (where rules propagate information in a single temporal direction), reasoning over integers becomes PSPACE-complete in data complexity and hence no harder than over positive programs; however, reasoning over the rationals in this fragment remains undecidable.

Semi-Stable Semantics for Abstract Dialectical Frameworks

dialectical frameworks (ADFs) have been introduced as a formalism for modeling and evaluating argumentation allowing general logical satisfaction conditions. Different criteria that have been used to settle the acceptance of arguments are called semantics. However, the notion of semi-stable semantics as studied for abstract argumentation frameworks has received little attention for ADFs. In the current work, we present the concepts of semi-two-valued models and semi-stable models for ADFs. We show that these two notions satisfy a set of plausible properties required for semi-stable semantics of ADFs. Moreover, we show that semi-two-valued and semi-stable semantics of ADFs form a proper generalization of the semi-stable semantics of AFs, just like two-valued model and stable semantics for ADFs are generalizations of stable semantics for AFs.

Defining the Semantics of Abstract Argumentation Frameworks through Logic Programs and Partial Stable Models (Extended Abstract)

Extensions of Dung’s Argumentation Framework (AF) include the class of Recursive Bipolar AFs (Rec-BAFs), i.e. AFs with recursive attacks and supports. We show that a Rec-BAF \Delta can be translated into a logic program P_\Delta so that the extensions of \Delta under different semantics coincide with subsets of the partial stable models of P_\Delta.

Mixed-Stable Models: An Application to High-Frequency Financial Data

The paper extends the study of applying the mixed-stable models to the analysis of large sets of high-frequency financial data. The empirical data under review are the German DAX stock index yearly log-returns series. Mixed-stable models for 29 DAX companies are constructed employing efficient parallel algorithms for the processing of long-term data series. The adequacy of the modeling is verified with the empirical characteristic function goodness-of-fit test. We propose the smart-Δ method for the calculation of the α-stable probability density function. We study the impact of the accuracy of the computation of the probability density function and the accuracy of ML-optimization on the results of the modeling and processing time. The obtained mixed-stable parameter estimates can be used for the construction of the optimal asset portfolio.

Unsatisfiable Core Analysis and Aggregates for Optimum Stable Model Search

Many efficient algorithms for the computation of optimum stable models in the context of Answer Set Programming (ASP) are based on unsatisfiable core analysis. Among them, algorithm OLL was the first introduced in the context of ASP, whereas algorithms ONE and PMRES were first introduced for solving the Maximum Satisfiability problem (MaxSAT) and later on adapted to ASP. In this paper, we present the porting to ASP of another state-of-the-art algorithm introduced for MaxSAT, namely K, which generalizes ONE and PMRES. Moreover, we present a new algorithm called OLL-IN-ONE that compactly encodes all aggregates of OLL by taking advantage of shared aggregate sets propagators. The performance of the algorithms have been empirically compared on instances taken from the latest ASP Competition.

On the Semantics of Abstract Argumentation Frameworks: A Logic Programming Approach

Recently there has been an increasing interest in frameworks extending Dung’s abstract Argumentation Framework (AF). Popular extensions include bipolar AFs and AFs with recursive attacks and necessary supports. Although the relationships between AF semantics and Partial Stable Models (PSMs) of logic programs has been deeply investigated, this is not the case for more general frameworks extending AF.In this paper we explore the relationships between AF-based frameworks and PSMs. We show that every AF-based framework Δ can be translated into a logic program PΔ so that the extensions prescribed by different semantics of Δ coincide with subsets of the PSMs of PΔ. We provide a logic programming approach that characterizes, in an elegant and uniform way, the semantics of several AF-based frameworks. This result allows also to define the semantics for new AF-based frameworks, such as AFs with recursive attacks and recursive deductive supports.

Verifying Tight Logic Programs with anthem and vampire

This paper continues the line of research aimed at investigating the relationship between logic programs and first-order theories. We extend the definition of program completion to programs with input and output in a subset of the input language of the ASP grounder gringo, study the relationship between stable models and completion in this context, and describe preliminary experiments with the use of two software tools, anthem and vampire, for verifying the correctness of programs with input and output. Proofs of theorems are based on a lemma that relates the semantics of programs studied in this paper to stable models of first-order formulas.