LPAR19:Papers with AbstractsPapers 

Abstract. Reachability analysis of programs with arrays is a wellknown challenging problem and many existing approaches are bound to incomplete solutions. In this paper we identify a class of programs with arrays for which safety is fully decidable. The completeness result we provide is built up from acceleration techniques for arrays and the decision procedure for the Array Property Fragment class.  Abstract. Current database systems supporting recursive SQL impose restrictions on queries such as linearity, and do not implement mutual recursion. In a previous work we presented the language and prototype RSQL to overcome those drawbacks. Now we introduce a formalization and an implementation of the database system HRSQL that, in addition to extended recursion, incorporates hypothetical reasoning in a novel way which cannot be found in any other SQL system, allowing both positive and negative assumptions. The formalization extends the fixpoint semantics of RSQL. The implementation improves the eciency of the previous prototype and is integrated in a commercial DBMS.  Abstract. While several interesting argumentationbased semantics for defeasible logic programs have been proposed, to our best knowledge, none of these approaches is able to fully handle the closure under strict rules in a sufficient manner: they are either not closed, or they use workarounds such as transposition of rules which violates the desired directionality of logic programming rules.
We propose a novel argumentationbased semantics, in which the status of arguments is determined by attacks between newly introduced conflict resolutions instead of attacks between arguments. We show that the semantics is closed w.r.t. strict rules and respects the directionality of inference rules, as well as other desired properties previously published in the literature.  Abstract. This paper describes interpolation procedures for EPR. In principle, interpolation for EPR is simple: It is a special case of firstorder interpolation. In practice, we would like procedures that take advantage of properties of EPR: EPR admits finite models and those models are sometimes possible to describe very compactly. Inspired by procedures for propositional logic that use models and cores, but not proofs, we develop a procedure for EPR that uses just models and cores.  Abstract. The area of AI robotics offers a set of fundamentally challenging problems when attempting to integrate logical reasoning functionality in such systems. The problems arise in part from the high degree of complexity in such architectures which include realtime behaviour, distribution, concurrency, various data latencies in operation and several levels of abstraction. For logic to work practically in such systems, traditional theorem proving, although important, is often not feasible for many of the functions of reasoning in such systems. In this article, we present a number of novel approaches to such reasoning functionality based on the use of temporal logic. The functionalities covered include, automated planning, streambased reasoning and execution monitoring.  Abstract. We develop a practical approach to querying temporal data stored in temporal SQL:2011 databases through the semantic layer of OWL 2 QL ontologies. An intervalbased temporal query language (TQL), which we propose for this task, is defined via naturally characterizable combinations of temporal logic with conjunctive queries. This foundation warrants welldefined semantics and formal properties of TQL querying. In particular, we show that under certain mild restrictions the data complexity of query answering remains in AC$^0$, i.e., as in the usual, nontemporal case. On the practical side, TQL is tailored specifically to offer maximum expressivity while preserving the possibility of reusing standard firstorder rewriting techniques and tools for OWL 2 QL.  Abstract. BDI (Bounded Depth Increase) is a new decidable firstorder clause class. It strictly includes known classes such as PVD. The arity of function and predicate symbols as well as the shape of atoms is not restricted in BDI. Instead the shape of "cycles" in resolution inferences is restricted such that the depth of generated clauses may increase but is still finitely bound. The BDI class is motivated by real world problems where function terms are used to represent record structures.
We show that the hyperresolution calculus modulo redundancy elimination terminates on BDI clause sets. Employing this result to the ordered resolution calculus, we can also prove termination of ordered resolution on BDI, yielding a more efficient decision procedure.  Abstract. We present a generalisation of the Event Calculus, specified in classical logic and implemented in ASP, that facilitates reasoning about nonbinaryvalued fluents in domains with nondeterministic, triggered, concurrent, and possibly conflicting actions. We show via a case study how this framework may be used as a basis for a "possibleworlds" style approach to epistemic and causal reasoning in a narrative setting. In this framework an agent may gain knowledge about both fluent values and action occurrences through sensing actions, lose knowledge via nondeterministic actions, and represent plans that include conditional actions whose conditions may be initially unknown.  Abstract. We propose an algorithm called CReaM to incrementally maintain materialized aggregate views with userdefined aggregates in response to changes to the database tables from which the views are derived. We show that when the physical design of the underlying database is optimized, the time taken by CReaM to update an aggregate view is optimal.  Abstract. Monadic predicates play a prominent role in many decidable cases, including decision procedures for symbolic automata. We are here interested in discovering whether a formula can be rewritten into a Boolean combination of monadic predicates. Our setting is quantifierfree formulas over a decidable background theory, such as arithmetic and we here develop a semidecision procedure for extracting a monadic decomposition of a formula when it exists. 

