ABSTRACT. Coherent logic (CL) is a fragment of first-order logic that is  more expressive than resolution logic in that it allows a  restricted form of existential quantification. Consequently,  many theories can be formulated directly in CL, for example,  without skolemization. CL has a simple proof theory yielding readable proofs. Thus it strikes a balance beween expressivity and efficiency of automated reasoning. In the talk we give an overview of CL and its application in automated reasoning, proof assistents, model finding, and constraint handling.

ABSTRACT. We present an example for application of CHR to automated test data generation and model checking in verification of mission critical software for satellite control.

ABSTRACT. Despite its rising popularity as data format especially for web services, the software ecosystem around the JavaScript Object Notation (JSON) is not as widely distributed as that of XML. For both data formats there exist schema languages to specify the structure of instance documents, but there is currently no opportunity to translate already existing XML Schema documents into equivalent JSON Schemas.

In this paper we introduce an implementation of a language translator. It takes an XML Schema and creates its equivalent JSON Schema document. Our approach is based on Prolog and CHR. By unfolding the XML Schema document into CHR constraints, it is possible to specify the concrete translation rules in a declarative way.

ABSTRACT. CHR is a declarative, concurrent and committed choice rule-based constraint programming language. We extend CHR with multiset comprehension patterns, providing the programmer with the ability to write multiset rewriting rules that can match a variable number of constraints in the store. This enables writing more readable, concise and declarative code for algorithms that coordinate large amounts of data or require aggregate operations. We call this extension CHR^cp . We give a high-level abstract semantics of CHR^cp , followed by a lower-level operational semantics. We then show the soundness of this operational semantics with respect to the abstract semantics.

ABSTRACT. We have additional discussion time for all talks before lunch

ABSTRACT. There exist many powerful techniques to analyze termination and complexity of term rewrite systems (TRSs). Our goal is to use these techniques for the analysis of other programming languages as well. For instance, approaches to prove termination of definite logic programs by a transformation to TRSs have been studied for decades. However, a challenge is to handle languages with more complex evaluation strategies (such as Prolog, where predicates like the cut influence the control flow).

We present a general methodology for the analysis of such programs. Here, the logic program is first transformed into a symbolic evaluation graph which represents all possible evaluations in a finite way. Afterwards, different analyses can be performed on these graphs. In particular, one can generate TRSs from such graphs and apply existing tools for termination or complexity analysis of TRSs to infer information on the termination or complexity of the original logic program.

ABSTRACT. Discussion on invited talk about "Symbolic Evaluation Graphs and Term Rewriting - A General Methodology for Analyzing Logic Programs".

ABSTRACT. The main idea of the logic programming approach to the intelligent video surveillance is in using a first order logic for describing complex events and abstract concepts like anomalous human activity, i.e. brawl, sudden attack, armed attack, leaving object, loitering, pick pocketing, personal theft, immobile person, etc. We consider main implementation issues of our approach to the intelligent video surveillance logic programming: object-oriented logic programming of concurrent stages of video processing, translating video surveillance logic programs to fast Java code, embedding low-level means for video storage and processing to the logic programming system.

ABSTRACT. Linear Meld is a concurrent forward-chaining linear logic programming language where logical facts can be asserted and retracted in a structured way. The database of facts is partitioned by the nodes of a graph structure which leads to parallelism if nodes are executed simultaneously. Communication arises whenever nodes send facts to other nodes by fact derivation. We present an overview of the virtual machine that we implemented to run Linear Meld on multicores, including code organization, thread management, rule execution and database organization for efficient fact insertion, lookup and deletion. Although our virtual machine is a work-in-progress, our results already show that Linear Meld is not only capable of scaling graph and machine learning programs but it also exhibits some interesting performance results when compared against other programming languages.

ABSTRACT. We have additional discussion time at the end of the workshop.