ABSTRACT. We present a computer-assisted non-existence proof of nine-input sorting networks consisting of 24 comparators, hence showing that the 25-comparator sorting network found by Floyd in 1964 is optimal. As a corollary, we obtain that the 29-comparator network found by Waksman in 1969 is optimal when sorting ten inputs. This closes the two smallest open instances of the optimal size sorting network problem, which have been open since the results of Floyd and Knuth from 1966 proving optimality for sorting networks of up to eight inputs.

The entire implementation is written in SWI-Prolog and was run on a cluster of 12 nodes with 12 cores each, able to run a total of 288 concurrent threads, making extensive use of SWI-Prolog’s built-in predicate concurrency/3. The search space of 2.2×10 37 comparator networks was exhausted after just under 10 days of computation. This shows the ability of logic programming to provide a scalable parallel implementation while at the same time instilling a high level of trust in the correctness of the proof.

This talk will be given by Luís Cruz-Filipe and Peter Schneider-Kamp.

ABSTRACT. Discussion for the invited talk on "Proofs for Optimality of Sorting Networks by Logic Programming".

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. 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. 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. 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. We have additional discussion time for all talks before lunch on July 17th.

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. 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. 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.

ABSTRACT. The third round of the Kurt Gödel Research Prize Fellowships Program, under the title: Connecting Foundations and Technology, aims at supporting young scholars in early stages of their academic careers by offering highest fellowships in history of logic, kindly supported by the John Templeton Foundation. Young scholars being less or exactly 40 years old at the time of the commencement of the Vienna Summer of Logic (July 9, 2014) will be awarded one fellowship award in the amount of EUR 100,000, in each of the following categories:

• Logical Foundations of Mathematics,
• Logical Foundations of Computer Science, and
• Logical Foundations of Artificial Intelligence

The following three Boards of Jurors were in charge of choosing the winners:

• Logical Foundations of Mathematics: Jan Krajíček, Angus Macintyre, and Dana Scott (Chair).
• Logical Foundations of Computer Science: Franz Baader, Johann Makowsky, and Wolfgang Thomas (Chair).
• Logical Foundations of Artificial Intelligence: Luigia Carlucci Aiello, Georg Gottlob (Chair), and Bernhard Nebel.

http://fellowship.logic.at/

ABSTRACT. The aim of the FLoC Olympic Games is to start a tradition in the spirit of the ancient Olympic Games, a Panhellenic sport festival held every four years in the sanctuary of Olympia in Greece, this time in the scientific community of computational logic. Every four years, as part of the Federated Logic Conference, the Games will gather together all the challenging disciplines from a variety of computational logic in the form of the solver competitions.

At the Award Ceremonies, the competition organizers will have the opportunity to present their competitions to the public and give away special prizes, the prestigious Kurt Gödel medals, to their successful competitors. This reinforces the main goal of the FLoC Olympic Games, that is, to facilitate the visibility of the competitions associated with the conferences and workshops of the Federated Logic Conference during the Vienna Summer of Logic.

This award ceremony will host the

• 3rd Confluence Competition (CoCo 2014);
• Configurable SAT Solver Challenge (CSSC 2014);
• Ninth Max-SAT Evaluation (Max-SAT 2014);
• QBF Gallery 2014; and
• SAT Competition 2014 (SAT-COMP 2014).

ABSTRACT. This talk will discuss the recent results achieved in inference and learning for probabilistic logic programs under the distribution semantics  and will propose directions for future work.