LPAR-19: Papers with Abstracts

Papers
Acceleration-based safety decision procedure for programs with arrays Francesco Alberti, Silvio Ghilardi and Natasha Sharygina Abstract. Reachability analysis of programs with arrays is a well-known 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.
Incorporating Hypothetical Views and Extended Recursion into SQL Database Systems Gabriel Aranda, Susana Nieva, Fernando Saenz-Perez and Jaime Sánchez-Hernández 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 R-SQL to overcome those drawbacks. Now we introduce a formalization and an implementation of the database system HR-SQL 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 R-SQL. The implementation improves the eciency of the previous prototype and is integrated in a commercial DBMS.
Conflict Resolution in Structured Argumentation Martin Baláž, Jozef Frtús and Martin Homola Abstract. While several interesting argumentation-based 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 argumentation-based 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.
Instantiations, Zippers and EPR Interpolation Nikolaj Bjorner, Arie Gurfinkel, Konstantin Korovin and Ori Lahav Abstract. This paper describes interpolation procedures for EPR. In principle, interpolation for EPR is simple: It is a special case of first-order 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.
Robotics, Temporal Logic and Stream Reasoning Patrick Doherty, Fredrik Heintz and Jonas Kvarnström 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, stream-based reasoning and execution monitoring.
Practical Querying of Temporal Data via OWL 2 QL and SQL:2011 Szymon Klarman 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 interval-based 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 well-defined 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 first-order rewriting techniques and tools for OWL 2 QL.
BDI: A New Decidable First-order Clause Class Manuel Lamotte-Schubert and Christoph Weidenbach Abstract. BDI (Bounded Depth Increase) is a new decidable first-order 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 hyper-resolution 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.
An Epistemic Event Calculus for ASP-based Reasoning About Knowledge of the Past, Present and Future Jiefei Ma, Rob Miller, Leora Morgenstern and Theodore Patkos Abstract. We present a generalisation of the Event Calculus, specified in classical logic and implemented in ASP, that facilitates reasoning about non-binary-valued fluents in domains with non-deterministic, triggered, concurrent, and possibly conflicting actions. We show via a case study how this framework may be used as a basis for a "possible-worlds" 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 non-deterministic actions, and represent plans that include conditional actions whose conditions may be initially unknown.
An Incremental Algorithm to Optimally Maintain Aggregate Views Abhijeet Mohapatra and Michael Genesereth Abstract. We propose an algorithm called CReaM to incrementally maintain materialized aggregate views with user-defined 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.
Effectively Monadic Predicates Margus Veanes, Nikolaj Bjorner, Lev Nachmanson and Sergey Bereg 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 quantifier-free formulas over a decidable background theory, such as arithmetic and we here develop a semi-decision procedure for extracting a monadic decomposition of a formula when it exists.