View: session overviewtalk overviewside by side with other conferences

09:00-10:15 Session 87B: Invited Talk (joint with CICLOPS-WLPE)
Location: FH, Hörsaal 7
Coherent Logic and Applications
SPEAKER: Marc Bezem

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.

10:15-10:45Coffee Break
10:45-12:45 Session 90BE: Contributed Talks (joint with CICLOPS-WLPE)
Location: FH, Hörsaal 7
Automated Test Case Generation and Model Checking with CHR
SPEAKER: Ralf Gerlich

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.

From XML Schema to JSON Schema: Translation with CHR
SPEAKER: Falco Nogatz

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.

Constraint Handling Rules with Multiset Comprehension Patterns

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.

SPEAKER: Everyone

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

13:00-14:30Lunch Break
14:30-16:00 Session 96AL: Invited Talk (joint with CICLOPS-WLPE)
Location: FH, Hörsaal 7
Symbolic Evaluation Graphs and Term Rewriting - A General Methodology for Analyzing Logic Programs
SPEAKER: Jürgen Giesl

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.

SPEAKER: Everyone

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

16:00-16:30Coffee Break
16:30-18:00 Session 99AK: Implementation Issues (joint with CICLOPS-WLPE)
Location: FH, Hörsaal 7
Intelligent Visual Surveillance Logic Programming: Implementation Issues

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.

A Parallel Virtual Machine for Executing Forward-Chaining Linear Logic Programs
SPEAKER: Flavio Cruz

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.

SPEAKER: Everyone

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