CICLOPS-WLPE 2014 PAPERS: PAPERS WITH ABSTRACTS

ABSTRACT. FO(·)IDP3 is a declarative modeling language that extends first-order logic with inductive definitions, partial functions, types and aggregates. Its model generator IDP3 evaluates all definitions that depend on fully known information before grounding and solving the problem specification. In this paper, we introduce a technique which allows us to refine the interpretation of defined symbols when they depend on information that is only partially given instead of completely given. We extend our existing transformation of FO(·)IDP3 definitions to Tabled Prolog rules with support for definitions that depend on information that is possibly partially unknown. In this paper we present an algorithm that uses XSB Prolog to evaluate these rules in such a way that we achieve the most precise possible refinement of the defined symbols. Experimental results show that our technique derives extra information for the defined symbols.

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. This paper describes three important extensions for the Finite Domain solver of GNU Prolog. First, the solver now supports negative integers. Second, the solver detects and prevents integer overflows from occurring. Third, the internal representation of sparse domains has been redesigned to overcome its current limitations. The preliminary performance evaluation shows a limited slowdown factor with respect to the initial solver. This factor is widely counterbalanced by the new possibilities and the robustness of the solver. Furthermore these results are preliminary and we propose some directions to limit this overhead.

ABSTRACT. Specifications in the Twelf system are based on a logic programming interpretation of the Edinburgh Logical Framework or LF. We consider an approach to animating such specifications using a Prolog implementation. This approach is based on a lossy encoding of LF expressions by simply typed lambda calculus (STLC) terms and a subsequent encoding of the lost dependency information in predicates that are defined by suitable clauses. To use this idea in an actual implementation, it is necessary also to describe an inverse transformation from STLC terms into LF expressions. While such an inverse does not always exist, we show that it does in the restricted setting where the STLC terms are the outcome of derivations constructed from predicate clauses that result from translating Twelf specifications. Twelf also supports the possibility of computing with LF specications in which types may contain variables with existential force. We discuss the possibility of supporting such a capability in our translation based approach to animation.

ABSTRACT. Indexing of terms and clauses is a well-known technique used in Prolog implementations, as well as automated theorem provers, to speed up search. In this paper we show how the same mechanism can be used to implement efficient reversible mappings between term representations (which we will call pre-indexing). Based on user-provided term descriptions, this mapping allows us to use cheap data encodings internally (such as prefix trees). We found that for some classes of programs we can drastically improve the efficiency by carefully selecting the application of the mapping at specific program points.

ABSTRACT. Despite of being a dominant tool for solving some practical NP-complete problems, Propositional Satisfiability (SAT) also has a number of weaknesses, including its inability to compactly represent numerical constraints and its low level, unstructured language of clauses. In contrast, Constraint Programming (CP) has been widely used for scheduling and solving combinatorial search problems. In this report, We present a tight integration of SAT with CP, called SAT(gc),which embeds global constraints into SAT. A prototype is implemented by integrating the state of the art SAT solver zchaff and the generic constraint solver gecode. Experiments are carried out for benchmarks from puzzle domains and planning domains to reveal insights in compact representation, solving effectiveness, and novel usability of the new framework.

ABSTRACT. SWI-Prolog version~7 extends the Prolog language further as a general purpose programming language that can be used as `glue' between components written in different languages. Taking this role rather than that of a DSL \emph{inside} other IT components has always been the design objective of SWI-Prolog as illustrated by XPCE (its object oriented communication to the OS and graphics), the HTTP server library and the many interfaces to external systems and file formats. In recent years, we started extending the language itself, notably to accomodate expressing syntactic constructions of other languages. This resulted in an extended notion of operators and quasi quotations. SWI-Prolog version~7 takes this one step further by extending the primitive data types of Prolog. This article describes and motivates these extensions.

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. Rational terms or rational trees are terms with one or more infinite sub-terms but with a finite representation. Rational terms appeared as a side effect of omitting the \emph{occurs check} in the unification of terms, but its support across Prolog systems varies and often fails to provide the expected functionality. A common problem is the lack of support for printing query bindings with rational terms. In this paper, we discuss the minimum requirements a Prolog system should have to support printing rational terms and propose the integration of an ISO Prolog predicate that works in several existing Prolog systems in order to overcome the technical problem of printing rational terms. This predicate could be easily adapted to work both for the top query printouts and for user printing.