eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
0
0
10.4230/LIPIcs.ICLP.2012
article
LIPIcs, Volume 17, ICLP'12, Complete Volume
Dovier, Agostino
Santos Costa, Vítor
LIPIcs, Volume 17, ICLP'12, Complete Volume
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012/LIPIcs.ICLP.2012.pdf
Logic Programming, Software Engineering, Mathematical Logic, Knowledge Representation Formalisms and Methods, Problem Solving, Control Methods
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
i
xvi
10.4230/LIPIcs.ICLP.2012.i
article
Frontmatter, Table of Contents, List of Authors
Dovier, Agostino
Santos Costa, Vítor
Frontmatter, Table of Contents, List of Authors
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.i/LIPIcs.ICLP.2012.i.pdf
Frontmatter
Table of Contents
List of Authors
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
17
21
10.4230/LIPIcs.ICLP.2012.xvii
article
Introduction to the Technical Communications of the 28th International Conference on Logic Programming Special Issue
Dovier, Agostino
Santos Costa, Vítor
We are proud to introduce this special issue of LIPIcs — Leibniz International Proceedings in Informatics, dedicated to the technical communications accepted for the 28th International Conference on Logic Programming (ICLP).
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.xvii/LIPIcs.ICLP.2012.xvii.pdf
Logic Programming
Organization Details
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
1
13
10.4230/LIPIcs.ICLP.2012.1
article
Simulation Unification: Beyond Querying Semistructured Data (Invited Talk)
Bry, François
Schaffert, Sebastian
This article first reminds of simulation unification, a non-standard unification proposed at the 18th International Conference on Logic Programming (ICLP 2002) for making logic programming capable of querying semistructured data on the Web. This article further argues that, beyond querying semistructured data on the Web, simulation unification has a potential for Web querying of multimedia data and semantic metadata and for Web searching of data of all kinds.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.1/LIPIcs.ICLP.2012.1.pdf
Simulation Unification
(Semantic) Web Querying
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
14
25
10.4230/LIPIcs.ICLP.2012.14
article
Modeling Machine Learning and Data Mining Problems with FO(·)
Blockeel, Hendrik
Bogaerts, Bart
Bruynooghe, Maurice
De Cat, Broes
De Pooter, Stef
Denecker, Marc
Labarre, Anthony
Ramon, Jan
Verwer, Sicco
This paper reports on the use of the FO(·) language and the IDP framework for modeling and solving some machine learning and data mining tasks. The core component of a model in the IDP framework is an FO(·) theory consisting of formulas in first order logic and definitions; the latter are basically logic programs where clause bodies can have arbitrary first order formulas. Hence, it is a small step for a well-versed computer scientist to start modeling. We describe some models resulting from the collaboration between IDP experts and domain experts solving machine learning and data mining tasks. A first task is in the domain of stemmatology, a domain of philology concerned with the relationship between surviving variant versions of text. A second task is about a somewhat similar problem within biology where phylogenetic trees are used to represent the evolution of species. A third and final task is about learning a minimal automaton consistent with a given set of strings. For each task, we introduce the problem, present the IDP code and report on some experiments.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.14/LIPIcs.ICLP.2012.14.pdf
Knowledge representation and reasoning
declarative modeling
logic programming
knowledge base systems
FO(·)
IDP framework
stemmatology
phylogene
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
26
36
10.4230/LIPIcs.ICLP.2012.26
article
Answering Why and How questions with respect to a frame-based knowledge base: a preliminary report
Baral, Chitta
Ha Vo, Nguyen
Liang, Shanshan
Being able to answer questions with respect to a given text is the cornerstone of language understanding and at the primary school level students are taught how to answer various kinds of questions including why and how questions. In the building of automated question answering systems the focus so far has been more on factoid questions and comparatively little attention has been devoted to answering why and how questions. In this paper we explore answering why and how questions with respect to a frame-based knowledge base and give algorithms and ASP (answer set programming) implementation to answer two classes of questions in the Biology domain. They are of the form: "How are X and Y related in the process Z?" and "Why is X important to Y?"
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.26/LIPIcs.ICLP.2012.26.pdf
answer set programming
frame based knowledge representation
question answering.
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
37
48
10.4230/LIPIcs.ICLP.2012.37
article
Applying Machine Learning Techniques to ASP Solving
Maratea, Marco
Pulina, Luca
Ricca, Francesco
Having in mind the task of improving the solving methods for Answer Set Programming (ASP), there are two usual ways to reach this goal: (i) extending state-of-the-art techniques and ASP solvers, or (ii) designing a new ASP solver from scratch. An alternative to these trends is to build on top of state-of- the-art solvers, and to apply machine learning techniques for choosing automatically the "best" available solver on a per-instance basis.
In this paper we pursue this latter direction. We first define a set of cheap-to-compute syntactic features that characterize several aspects of ASP programs. Then, given the features of the instances in a training set and the solvers performance on these instances, we apply a classification method to inductively learn algorithm selection strategies to be applied to a test set. We report the results of an experiment considering solvers and training and test sets of instances taken from the ones submitted to the "System Track" of the 3rd ASP competition. Our analysis shows that, by applying machine learning techniques to ASP solving, it is possible to obtain very robust performance: our approach can solve a higher number of instances compared with any solver that entered the 3rd ASP competition.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.37/LIPIcs.ICLP.2012.37.pdf
Answer Set Programming
Automated Algorithm Selection
Multi-Engine solvers
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
49
60
10.4230/LIPIcs.ICLP.2012.49
article
An Answer Set Solver for non-Herbrand Programs: Progress Report
Balduccini, Marcello
In this paper we propose an extension of Answer Set Programming (ASP) by non-Herbrand functions, i.e. functions over non-Herbrand domains, and describe a solver for the new language. Our approach stems for our interest in practical applications, and from the corresponding need to compute the answer sets of programs with non-Herbrand functions efficiently. Our extension of ASP is such that the semantics of the new language is obtained by a comparatively small change to the ASP semantics from [8]. This makes it possible to modify a state-of-the-art ASP solver in an incremental fashion, and use it for the computation of the answer sets of (a large class of) programs of the new language. The computation is rather efficient, as demonstrated by our experimental evaluation.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.49/LIPIcs.ICLP.2012.49.pdf
Answer Set Programming
non-Herbrand Functions
Answer Set Solving
Knowledge Representation and Reasoning
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
61
71
10.4230/LIPIcs.ICLP.2012.61
article
Stable Models of Formulas with Generalized Quantifiers (Preliminary Report)
Lee, Joohyung
Meng, Yunsong
Applications of answer set programming motivated various extensions of the stable model semantics, for instance, to allow aggregates or to facilitate interface with external ontology descriptions. We present a uniform, reductive view on these extensions by viewing them as special cases of formulas with generalized quantifiers. This is done by extending the first-order stable model semantics by Ferraris, Lee and Lifschitz to account for generalized quantifiers and then by reducing the individual extensions to this formalism.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.61/LIPIcs.ICLP.2012.61.pdf
answer set programming
stable model semantics
generalized quantifiers
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
72
85
10.4230/LIPIcs.ICLP.2012.72
article
Using Answer Set Programming in the Development of Verified Software
Schanda, Florian
Brain, Martin
Software forms a key component of many modern safety and security critical systems. One approach to achieving the required levels of assurance is to prove that the software is free from bugs and meets its specification. If a proof cannot be constructed it is important to identify the root cause as it may be a flaw in the specification or a bug. Novice users often find this process frustrating and discouraging, and it can be time-consuming for experienced users. The paper describes a commercial application based on Answer Set Programming called Riposte. It generates simple counter-examples for false and unprovable verification conditions (VCs). These help users to understand why problematic VC are false and makes the development of verified software easier and faster.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.72/LIPIcs.ICLP.2012.72.pdf
Answer Set Programming
verification
SPARK
Ada
contract based verification
safety critical
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
86
97
10.4230/LIPIcs.ICLP.2012.86
article
Generating Event-Sequence Test Cases by Answer Set Programming with the Incidence Matrix
Banbara, Mutsunori
Tamura, Naoyuki
Inoue, Katsumi
The effective use of ASP solvers is essential for enhancing efficiency and scalability. The incidence matrix is a simple representation used in Constraint Programming (CP) and Integer Linear Programming for modeling combinatorial problems. Generating test cases for event-sequence testing is to find a sequence covering array (SCA). In this paper, we consider the problem of finding optimal sequence covering arrays by ASP and CP. Our approach is based on an effective combination of ASP solvers and the incidence matrix. We first present three CP models from different viewpoints of sequence covering arrays: the naïve matrix model, the event-position matrix model, and the incidence matrix model. Particularly, in the incidence matrix model, an SCA can be represented by a (0,1)-matrix called the incidence matrix of the array in which the coverage constraints of the given SCA can be concisely expressed. We then present an ASP program of the incidence matrix model. It is compact and faithfully reflects the original constraints of the incidence matrix model. In our experiments, we were able to significantly improve the previously known bounds for many arrays of strength three. Moreover, we succeeded either in finding optimal solutions or in improving known bounds for some arrays of strength four.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.86/LIPIcs.ICLP.2012.86.pdf
Event-Sequence Testing
Answer Set Programming
Matrix Model
Constraint Programming
Propositional Satisfiability (SAT)
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
98
108
10.4230/LIPIcs.ICLP.2012.98
article
Towards Testing Concurrent Objects in CLP
Albert, Elvira
Arenas, Puri
Gómez-Zamalloa, Miguel
Testing is a vital part of the software development process. It is even more so in the context of concurrent languages, since due to undesired task interleavings and to unexpected behaviours of the underlying task scheduler, errors can go easily undetected. This paper studies the extension of the CLP-based framework for glass-box test data generation of sequential programs to the context of concurrent objects, a concurrency model which constitutes a promising solution to concurrency in OO languages. Our framework combines standard termination and coverage criteria used for testing sequential programs with specific criteria which control termination and coverage from the concurrency point of view, e.g., we can limit the number of task interleavings allowed and the number of loop unrollings performed in each parallel component, etc.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.98/LIPIcs.ICLP.2012.98.pdf
Testing
Glass-box Test Data Generation
Active Objects
Symbolic Execution
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
109
118
10.4230/LIPIcs.ICLP.2012.109
article
Visualization of CHR through Source-to-Source Transformation
Abdennadher, Slim
Sharaf, Nada
In this paper, we propose an extension of Constraint Handling Rules (CHR) with different visualization features. One feature is to visualize the execution of rules applied on a list of constraints. The second feature is to represent some of the CHR constraints as objects and visualize the effect of CHR rules on them. To avoid changing the compiler, our implementation is based on source-to-source transformation.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.109/LIPIcs.ICLP.2012.109.pdf
Source-to-Source Transformation
Constraint Handling Rules
Visualization
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
119
129
10.4230/LIPIcs.ICLP.2012.119
article
Static Type Inference for the Q language using Constraint Logic Programming
Zombori, Zsolt
Csorba, János
Szeredi, Péter
We describe an application of Prolog: a type inference tool for the Q functional language. Q is a terse vector processing language, a descendant of APL, which is getting more and more popular, especially in financial applications. Q is a dynamically typed language, much like Prolog. Extending Q with static typing improves both the readability of programs and programmer productivity, as type errors are discovered by the tool at compile time, rather than through debugging the program execution.
We map the task of type inference onto a constraint satisfaction problem and use constraint logic programming, in particular the Constraint Handling Rules extension of Prolog. We determine the possible type values for each program expression and detect inconsistencies. As most built-in function names of Q are overloaded, i.e. their meaning depends on the argument types, a quite complex system of constraints had to be implemented.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.119/LIPIcs.ICLP.2012.119.pdf
logic programming
types
static type checking
CSP
CHR
Q language
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
130
143
10.4230/LIPIcs.ICLP.2012.130
article
Improving Lazy Non-Deterministic Computations by Demand Analysis
Hanus, Michael
Functional logic languages combine lazy (demand-driven) evaluation strategies from functional programming with non-deterministic computations from logic programming. The lazy evaluation of non-deterministic subexpressions results in a demand-driven exploration of the search space: if the value of some subexpression is not required, the complete search space connected to it is not explored. On the other hand, this improvement could cause efficiency problems if unevaluated subexpressions are duplicated and later
evaluated in different parts of a program. In order to improve the execution behavior in such situations, we propose a program analysis that guides a program transformation to avoid such inefficiencies.
We demonstrate the positive effects of this program transformation
with KiCS2, a recent highly efficient implementation of the functional logic programming language Curry.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.130/LIPIcs.ICLP.2012.130.pdf
functional logic programming
implementation
program analysis
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
144
153
10.4230/LIPIcs.ICLP.2012.144
article
The additional difficulties for the automatic synthesis of specifications posed by logic features in functional-logic languages
Bacci, Giovanni
Comini, Marco
A. Feliú, Marco
Villanueva, Alicia
This paper discusses on the additional issues for the automatic inference of algebraic property-oriented specifications which arises because of interaction between laziness and logical variables in lazy functional logic languages.
We present an inference technique that overcomes these issues for the first-order fragment of the lazy functional logic language Curry. Our technique statically infers from the source code of a Curry program a specification which consists of a set of equations relating (nested) operation calls that have the same behavior. Our proposal is a (glass-box) semantics-based inference method which can guarantee, to some extent, the correctness of the inferred specification, differently from other (black-box) approaches based on testing techniques.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.144/LIPIcs.ICLP.2012.144.pdf
Curry
property-oriented specifications
semantics-based inference methods
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
154
163
10.4230/LIPIcs.ICLP.2012.154
article
A Concurrent Operational Semantics for Constraint Functional Logic Programming
del Vado Vírseda, Rafael
Pérez Morente, Fernando
García Toledo, Marcos Miguel
In this paper we describe a sound and complete concurrent operational semantics for constraint functional logic programming languages which allows to model declarative applications in which the interaction between demand-driven narrowing and constraint solving helps to prune the search space, leading to shorter goal derivations. We encode concurrency into the generic CFLP(D) scheme, a uniform foundation for the operational semantics of constraint functional logic programming systems parameterized by a constraint solver over the given domain D. In this concurrent version of the CFLP(D) scheme, goal solving processes can be executed concurrently and cooperate together to perform their specific tasks via demand-driven narrowing and declarative residuation guided by constrained definitional trees, constraint solving, and communication by synchronization on logical variables.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.154/LIPIcs.ICLP.2012.154.pdf
Constraint logic programming
concurrent logic programming
functional logic programming.
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
164
175
10.4230/LIPIcs.ICLP.2012.164
article
Surviving Solver Sensitivity: An ASP Practitioner’s Guide
Silverthorn, Bryan
Lierler, Yuliya
Schneider, Marius
Answer set programming (ASP) is a declarative programming formalism that allows a practitioner to specify a problem without describing an algorithm for solving it. In ASP, the tools for processing problem specifications are called answer set solvers. Because specified problems are often NP complete, these systems often require significant computational effort to succeed. Furthermore, they offer different heuristics, expose numerous parameters, and their running time is sensitive to the configuration used. Portfolio solvers and automatic algorithm configuration systems are recent attempts to automate the problem of manual parameter tuning, and to mitigate
the burden of identifying the right solver configuration. The approaches taken in portfolio solvers and automatic algorithm configuration systems are orthogonal. This paper evaluates these approaches, separately and jointly, in the context of real-world ASP application development. It outlines strategies for their use in such settings, identifies their respective strengths and weaknesses, and advocates for a methodology that would make them an integral part of developing ASP applications.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.164/LIPIcs.ICLP.2012.164.pdf
algorithm configuration
algorithm selection
portfolio solving
answer set programming
algorithm portfolios
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
176
187
10.4230/LIPIcs.ICLP.2012.176
article
aspeed: ASP-based Solver Scheduling
Hoos, Holger
Kaminski, Roland
Schaub, Torsten
Schneider, Marius
Although Boolean Constraint Technology has made tremendous progress over the last decade, it suffers from a great sensitivity to search configuration. This problem was impressively counterbalanced at the
2011 SAT Competition by the rather simple approach of ppfolio relying on a handmade, uniform and unordered solver schedule. Inspired by this, we take advantage of the modeling and solving capacities of ASP to automatically determine more refined, that is, non-uniform and ordered solver schedules from existing benchmarking data. We begin by formulating the determination of such schedules as multi-criteria optimization problems and provide corresponding ASP encodings. The resulting encodings are easily customizable for different settings and the computation of optimum schedules can mostly be done in the blink of an eye, even when dealing with large runtime data sets stemming from many solvers on hundreds to thousands of instances. Also, its high customizability made it easy to generate even parallel
schedules for multi-core machines.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.176/LIPIcs.ICLP.2012.176.pdf
Algorithm Schedule
Portfolio-based Solving
Answer Set Programming
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
188
200
10.4230/LIPIcs.ICLP.2012.188
article
Answer Set Solving with Lazy Nogood Generation
Drescher, Christian
Walsh, Toby
Although Answer Set Programming (ASP) systems are highly optimised, their performance is sensitive to the size of the input and the inference it encodes. We address this deficiency by introducing a new extension to ASP solving. The idea is to integrate external propagators to represent parts of the encoding implicitly, rather than generating it a-priori. To match the state-of-the-art in conflict-driven solving, however, external propagators can make their inference explicit on demand. We demonstrate applicability in a novel Constraint Answer Set Programming system that can seamlessly integrate constraint propagation without sacrifficing the advantages
of conflict-driven techniques. Experiments provide evidence for computational impact.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.188/LIPIcs.ICLP.2012.188.pdf
Conflict-Driven Nogood Learning
Constraint Answer Set Programming
Constraint Propagation
Lazy Nogood Generation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
201
211
10.4230/LIPIcs.ICLP.2012.201
article
Lazy Model Expansion by Incremental Grounding
De Cat, Broes
Denecker, Marc
Stuckey, Peter
Ground-and-solve methods used in state-of-the-art Answer Set Programming and model expansion systems proceed by rewriting the problem specification into a ground format and afterwards
applying search. A disadvantage of such approaches is that the rewriting step blows up the original specification for large input domains and is unfeasible in case of infinite domains. In this
paper we describe a lazy approach to model expansion in the context of first-order logic that can cope with large and infinite problem domains. The method interleaves grounding and search, incrementally extending the current partial grounding only when necessary. It often allows to solve the original problem without creating the full grounding and is hence more widely applicable than ground-and-solve. We report on an existing implementation within the IDP system
and on experiments that show the promise of the method.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.201/LIPIcs.ICLP.2012.201.pdf
Knowledge representation and reasoning
model generation
grounding
IDP framework
first-order logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
212
221
10.4230/LIPIcs.ICLP.2012.211
article
Unsatisfiability-based optimization in clasp
Andres, Benjamin
Kaufmann, Benjamin
Matheis, Oliver
Schaub, Torsten
Answer Set Programming (ASP) features effective optimization capacities based on branch-and-bound algorithms. Unlike this, in the area of Satisfiability Testing (SAT) the finding of minimum
unsatisfiable cores was put forward as an alternative approach to solving Maximum Satisfiability (MaxSAT) problems. We explore this alternative approach to optimization in the context of ASP. To this end, we extended the ASP solver clasp with optimization components based upon the computation of minimal unsatisfiable cores. The resulting system, unclasp, is based on an extension of the well-known algorithms msu1 and msu3 and tailored to the characteristics of ASP.
We evaluate our system on multi-criteria optimization problems stemming from realistic Linux package configuration problems. In fact, the ASP-based Linux configuration system aspuncud relies on unclasp and won four out of seven tracks at the 2011 MISC competition.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.211/LIPIcs.ICLP.2012.211.pdf
answer-set-programming
solvers
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
222
234
10.4230/LIPIcs.ICLP.2012.222
article
An FLP-Style Answer-Set Semantics for Abstract-Constraint Programs with Disjunctions
Oetsch, Johannes
Pührer, Jörg
Tompits, Hans
We introduce an answer-set semantics for abstract-constraint programs with disjunction in rule heads in the style of Faber, Leone, and Pfeifer (FLP). To this end, we extend the definition of an answer set for logic programs with aggregates in rule bodies using the usual FLP-reduct. Additionally, we also provide a characterisation of our semantics in terms of unfounded sets, likewise generalising the standard concept of an unfounded set. Our work is motivated by the desire to have simple and rule-based definitions of the semantics of an answer-set programming (ASP) language that is close to those implemented by the most prominent ASP solvers. The new definitions are intended as a theoretical device to allow for development methods and methodologies for ASP, e.g., debugging or testing techniques, that are general enough to work for different types of solvers. We use abstract constraints as an abstraction of literals whose truth values depend on subsets of an interpretation. This includes weight constraints, aggregates, and external atoms, which are frequently used in real-world answer-set programs. We compare the new semantics to previous semantics for abstract-constraint programs and show that they are equivalent to recent extensions of the FLP semantics to propositional and first-order theories when abstract-constraint
programs are viewed as theories.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.222/LIPIcs.ICLP.2012.222.pdf
answer-set programming
abstract constraints
aggregates
disjunction
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
235
246
10.4230/LIPIcs.ICLP.2012.235
article
Reconciling Well-Founded Semantics of DL-Programs and Aggregate Programs
You, Jia-Huai
Morris, John
Bi, Yi
Logic programs with aggregates and description logic programs (dl-programs) are two recent extensions to logic programming. In this paper, we study the relationships between these two classes of logic programs, under the well-founded semantics. The main result is that, under a satisfaction-preserving mapping from dl-atoms to aggregates, the well-founded semantics of dl-programs by Eiter et al., coincides with the well-founded semantics of aggregate programs, defined by Pelov et al. as the least fixpoint of a 3-valued immediate consequence operator under the ultimate approximating aggregate. This result enables an alternative definition of the same well-founded semantics for aggregate programs, in terms of the first principle of unfounded sets. Furthermore, the result can be applied, in a uniform manner, to define the well-founded semantics for dl-programs with aggregates, which agrees with the existing semantics when either dl-atoms or aggregates are absent.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.235/LIPIcs.ICLP.2012.235.pdf
Well-founded semantics
description logic programs
aggregate logic programs
three-valued logic.
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
247
258
10.4230/LIPIcs.ICLP.2012.247
article
Preprocessing of Complex Non-Ground Rules in Answer Set Programming
Morak, Michael
Woltran, Stefan
In this paper we present a novel method for preprocessing complex non-ground rules in answer set programming (ASP). Using a well-known result from the area of conjunctive query evaluation, we apply
hypertree decomposition to ASP rules in order to make the structure of rules more explicit to grounders. In particular, the decomposition of rules reduces the number of variables per rule, while on the other hand, additional predicates are required to link the decomposed rules together. As we show in this paper, this technique can reduce the size of the grounding significantly and thus improves the performance of ASP systems in certain cases. Using a prototype implementation and the benchmark suites of the Answer Set Programming Competition 2011, we perform extensive tests of our decomposition approach that clearly
show the improvements in grounding time and size.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.247/LIPIcs.ICLP.2012.247.pdf
answer set programming
hypertree decomposition
preprocessing
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
259
266
10.4230/LIPIcs.ICLP.2012.259
article
Two-Valued Logic Programs
Lifschitz, Vladimir
We define a nonmonotonic formalism that shares some features with three other systems of nonmonotonic reasoning—default logic, logic programming with strong negation, and nonmonotonic causal logic—and study its possibilities as a language for describing actions.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.259/LIPIcs.ICLP.2012.259.pdf
Answer set programming
Non monotonic reasoning
Foundations
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
267
276
10.4230/LIPIcs.ICLP.2012.267
article
Possibilistic Nested Logic Programs
Nieves, Juan Carlos
Lindgren, Helena
We introduce the class of possibilistic nested logic programs. These possibilistic logic programs allow us to use nested expressions in the bodies and the heads of their rules. By considering a
possibilistic nested logic program as a possibilistic theory, a construction of a possibilistic logic programing semantics based on answer sets for nested logic programs and the proof theory of
possibilistic logic is defined. We show that this new semantics for possibilistic logic programs is computable by means of transforming possibilistic nested logic programs into possibilistic disjunctive logic programs. The expressiveness of the possibilistic nested logic programs is illustrated by scenarios from the medical domain. In particular, we exemplify how possibilistic nested logic programs are expressive enough for capturing medical guidelines which are pervaded of vagueness and qualitative information.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.267/LIPIcs.ICLP.2012.267.pdf
Answer Set Programming
Uncertain Information
Possibilistic Reasoning
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
277
289
10.4230/LIPIcs.ICLP.2012.277
article
A Tarskian Informal Semantics for Answer Set Programming
Denecker, Marc
Lierler, Yuliya
Truszczynski, Miroslaw
Vennekens, Joost
In their seminal papers on stable model semantics, Gelfond and Lifschitz introduced ASP by casting programs as epistemic theories, in which rules represent statements about the knowledge of a rational
agent. To the best of our knowledge, theirs is still the only published systematic account of the intuitive meaning of rules and programs under the stable semantics. In current ASP practice, however, we find numerous applications in which rational agents no longer seem to play any role. Therefore, we propose here an alternative explanation of the intuitive meaning of ASP programs, in which they are not viewed as statements about an agent's beliefs, but as objective statements about the world. We argue that this view is more natural for a large part of current ASP practice, in particular the so-called Generate-Define-Test programs.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.277/LIPIcs.ICLP.2012.277.pdf
Answer set programming
informal semantics
generate-define-test
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
290
300
10.4230/LIPIcs.ICLP.2012.290
article
Paving the Way for Temporal Grounding
Aguado, Felicidad
Cabalar, Pedro
Diéguez, Martín
Pérez, Gilberto
Vidal, Concepción
In this paper we consider the problem of introducing variables in temporal logic programs under the formalism of Temporal Equilibrium Logic (TEL), an extension of Answer Set Programming (ASP) for dealing with linear-time modal operators. We provide several fundamental contributions that pave the way for the implementation of a grounding process, that is, a method that allows replacing variables by ground instances in all the possible (or better, relevant) ways.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.290/LIPIcs.ICLP.2012.290.pdf
ASP
linear temporal logic
grounding
temporal equilibrium logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
301
311
10.4230/LIPIcs.ICLP.2012.301
article
Logic + control: An example
Drabent, Wlodzimierz
We present a Prolog program - the SAT solver of Howe and King - as a (pure) logic program with added control. The control consists of a selection rule (delays of Prolog) and pruning the search space. We construct the logic program together with proofs of its correctness and completeness, with respect to a formal specification. Correctness and termination of the logic program are inherited by the Prolog program; the change of selection rule preserves completeness. We prove
that completeness is also preserved by one case of pruning; for the other an informal justification is presented.
For proving correctness we use a method, which should be well known but is often neglected. For proving program completeness we employ a new, simpler variant of a method published previously. We point out usefulness of approximate specifications. We argue that the proof
methods correspond to natural declarative thinking about programs, and that they can be used, formally or informally, in every-day programming.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.301/LIPIcs.ICLP.2012.301.pdf
program correctness
program completeness
specification
declarative programming
declarative diagnosis.
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
312
322
10.4230/LIPIcs.ICLP.2012.312
article
Deriving a Fast Inverse of the Generalized Cantor N-tupling Bijection
Tarau, Paul
We attack an interesting open problem (an efficient algorithm to invert the generalized Cantor N-tupling bijection) and solve it through a sequence of equivalence preserving transformations of logic programs, that take advantage of unique strengths of this programming paradigm. An extension to set and multiset tuple encodings, as well as a simple application to a "fair-search" mechanism illustrate practical uses of our algorithms.
The code in the paper (a literate Prolog program, tested with SWI-Prolog and Lean Prolog) is available at http://logic.cse.unt.edu/tarau/research/2012/pcantor.pl .
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.312/LIPIcs.ICLP.2012.312.pdf
generalized Cantor n-tupling bijection
bijective data type transformations
combinatorial number system
solving combinatorial problems in Prolog
op
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
323
333
10.4230/LIPIcs.ICLP.2012.323
article
On the Termination of Logic Programs with Function Symbols
Greco, Sergio
Spezzano, Francesca
Trubitsyna, Irina
Recently there has been an increasing interest in the bottom-up evaluation of the semantics of logic programs with complex terms. The main problem due to the presence of functional symbols in the head of rules is that the corresponding ground program could be infinite and that finiteness of models and termination of the evaluation procedure is not guaranteed. This paper introduces, by deeply analyzing program structure, new decidable criteria, called safety and Gamma-acyclicity,
for checking termination of logic programs with function symbols under bottom-up evaluation. These criteria guarantee that stable models are finite and computable, as it is possible to generate
a finitely ground program equivalent to the source program. We compare new criteria with other decidable criteria known in the literature and show that the Gamma-acyclicity criterion is the most
general one. We also discuss its application in answering bound queries.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.323/LIPIcs.ICLP.2012.323.pdf
Logic Programming
Function Symbols
Bottom-up Execution
Program Termination
Stable Models
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
334
347
10.4230/LIPIcs.ICLP.2012.334
article
Logic Programming in Tabular Allegories
Gallego Arias, Emilio Jesús
B. Lipton, James
We develop a compilation scheme and categorical abstract machine for execution of logic programs based on allegories, the categorical version of the calculus of relations. Operational and denotational semantics are developed using the same formalism, and query execution is performed using algebraic reasoning. Our work serves two purposes: achieving a formal model of a logic programming compiler and efficient runtime; building the base for incorporating features typical of functional programming in a declarative way, while maintaining 100% compatibility with existing Prolog programs.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.334/LIPIcs.ICLP.2012.334.pdf
Category Theory
Logic Programming
Lawvere Categories
Programming Language Semantics
Declarative Programming
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
348
358
10.4230/LIPIcs.ICLP.2012.348
article
Tabling for infinite probability computation
Sato, Taisuke
Meyer, Philipp
Tabling in logic programming has been used to eliminate redundant computation and also to stop infinite loop. In this paper we add the third usage of tabling, i.e. to make infinite computation possible for probabilistic logic programs. Using PRISM, a logic-based probabilistic modeling language with a tabling mechanism, we generalize prefix probability computation for PCFGs to probabilistic logic programs. Given a top-goal, we search for all SLD proofs
by tabled search regardless of whether they contain loop or not. We then convert them to a set of linear probability equations and solve them by matrix operation. The solution gives us the probability of the top-goal, which, in nature, is an infinite sum of probabilities. Our generalized approach to prefix probability computation through tabling opens a way to logic-based probabilistic modeling of cyclic dependencies.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.348/LIPIcs.ICLP.2012.348.pdf
probability
tabling
PRISM
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
359
369
10.4230/LIPIcs.ICLP.2012.359
article
ASP at Work: An ASP Implementation of PhyloWS
Le, Tiep
Nguyen, Hieu
Pontelli, Enrico
Cao Son, Tran
This paper continues the exploration started in [Bininda-Emonds,2004], aimed at demonstrating the use of logic programming technology to support a large scale deployment and analysis of phylogenetic data from biological studies. This application paper illustrates the use of ASP technology in implementing the PhyloWS web service API — a recently proposed and community-agreed standard API to enable uniform access and inter-operation among phylogenetic applications and repositories. To date, only very incomplete implementations of PhyloWS have been realized; this paper demonstrates how ASP provides an ideal technology to support a more comprehensive realization of PhyloWS on a repository of semantically-described phylogenetic studies. The paper also presents a challenge for the developers of ASP-solvers.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.359/LIPIcs.ICLP.2012.359.pdf
Answer sets
phylogenetic inference
systems
applications
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
370
380
10.4230/LIPIcs.ICLP.2012.370
article
CHR for Social Responsibility
Dahl, Veronica
Coleman, Bradley
Miralles, J. Emilio
Maharshak, Erez
Publicly traded corporations often operate against the public's interest, serving a very limited group of stakeholders. This is counter-intuitive, since the public as a whole owns these corporations through direct investment in the stock-market, as well as indirect investment in mutual, index, and pension funds. Interestingly, the public's role in the proxy voting process, which
allows shareholders to influence their company's direction and decisions, is essentially ignored by individual investors. We
speculate that a prime reason for this lack of participation is information overload, and the disproportionate efforts required for an investor to make an informed decision. In this paper we propose a CHR based model that significantly simplifies the decision making process, allowing users to set general guidelines that can be applied to every company they own to produce voting recommendations. The use of CHR here is particularly advantageous as it allows users to easily track back the most relevant data that was used to formulate the decision, without the user having to go through large amounts of irrelevant information. Finally we describe a simplified algorithm that could be used as part of this model.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.370/LIPIcs.ICLP.2012.370.pdf
Constraint handling rules
principled decision making
informed voting
client directed voting
social responsibility.
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
381
392
10.4230/LIPIcs.ICLP.2012.381
article
A Logic Programming approach for Access Control over RDF
Lopes, Nuno
Kirrane, Sabrina
Zimmermann, Antoine
Polleres, Axel
Mileo, Alessandra
The Resource Description Framework (RDF) is an interoperable data representation format suitable for interchange and integration of data, especially in Open Data contexts. However, RDF is also becoming increasingly attractive in scenarios involving sensitive data, where data protection is a major concern. At its core, RDF does not support any form of access control and current proposals for extending RDF with access control do not fit well with the RDF representation model. Considering an enterprise scenario, we present a modelling that caters for access control over the stored RDF data in an intuitive and transparent manner. For this paper we rely on Annotated RDF, which introduces concepts from Annotated Logic Programming into
RDF. Based on this model of the access control annotation domain, we propose a mechanism to manage permissions via application-specific logic rules. Furthermore, we illustrate how our Annotated Query Language (AnQL) provides a secure way to query this access control annotated RDF data.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.381/LIPIcs.ICLP.2012.381.pdf
Logic Programming
Annotation
Access Control
RDF
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
393
403
10.4230/LIPIcs.ICLP.2012.393
article
LOG-IDEAH: ASP for Architectonic Asset Preservation
Novelli, Viviana
De Vos, Marina
Padget, Julian
D’Ayala, Dina
To preserve our cultural heritage, it is important to preserve our architectonic assets, comprising buildings, their decorations and the spaces they encompass. In some geographical areas, occasional natural disasters, specifically earthquakes, damage these cultural assets. Perpetuate is a European Union funded project aimed at establishing a methodology for the classification of the damage to these buildings, expressed as "collapse mechanisms". Structural engineering research
has identified 17 different collapse mechanisms for masonry buildings damaged by earthquakes. Following established structural engineering practice, paper-based decisions trees have been specified to encode the recognition process for each of the various collapse mechanisms. In this paper, we report on how answer set programming has been applied to the construction of a machine-processable representation of these collapse mechanisms as an alternative for these decision-trees and their subsequent verification and application to building records from L'Aquila, Algiers and Rhodes. As a result, we advocate that structural engineers do not require the time-consuming
and error-prone method of decisions trees, but can instead specify the properties of collapse mechanisms directly as an answer set program.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.393/LIPIcs.ICLP.2012.393.pdf
Answer set programming
structural engineering
knowledge representation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
404
414
10.4230/LIPIcs.ICLP.2012.404
article
Extending C+ with Composite Actions for Robotic Task Planning
Chen, Xiaoping
Jin, Guoqiang
Yang, Fangkai
This paper extends action language C+ by introducing composite actions as sequential execution of other actions, leading to a more intuitive and flexible way to represent action domains, better exploit a general-purpose formalization, and improve the reasoning efficiency for large domains. Our experiments show that the composite actions can be seen as a method of knowledge acquisition for intelligent robots.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.404/LIPIcs.ICLP.2012.404.pdf
Reasoning about Actions
Action Languages
Robotic Task Planning
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
415
424
10.4230/LIPIcs.ICLP.2012.415
article
Improving Quality and Efficiency in Home Health Care: an application of Constraint Logic Programming for the Ferrara NHS unit
Cattafi, Massimiliano
Herrero, Rosa
Gavanelli, Marco
Nonato, Maddalena
Malucelli, Federico
Although sometimes it is necessary, no one likes to stay in a hospital, and patients who need to stay in bed but do not require constant medical surveillance prefer their own bed at home. At
the same time, a patient in a hospital has a high cost for the community, that is not acceptable if the patient needs service only a few minutes a day.
For these reasons, the current trend in Europe and North-America is to send nurses to visit patients in their home: this choice reduces costs for the community and gives better quality of life to patients. On the other hand, it introduces the combinatorial problem of assigning patients to the available nurses in order to maximize the quality of service, without having nurses travel for overly long distances.
In this paper, we describe the problem as a practical application of Constraint Logic Programming. We first introduce the problem, as it is currently addressed by the nurses in the National Health Service (NHS) in Ferrara, a mid-sized city in the North of Italy. Currently, the nurses solve the problem by hand, and this introduces several inefficiencies in the schedules.
We formalize the problem, obtained by interacting with the nurses in the NHS, into a Constraint Logic Programming model. In order to solve the problem efficiently, we implemented a new constraint that tackles with the routing part of the problem. We propose a declarative
semantics for the new constraint, and an implementation based on an external solver.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.415/LIPIcs.ICLP.2012.415.pdf
CLP(FD)
Nurse Scheduling Applications
Home Health Care
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
425
438
10.4230/LIPIcs.ICLP.2012.425
article
A Flexible Solver for Finite Arithmetic Circuits
Filardo, Nathaniel Wesley
Eisner, Jason
Arithmetic circuits arise in the context of weighted logic programming languages, such as Datalog with aggregation, or Dyna. A weighted logic program defines a generalized arithmetic circuit—the weighted version of a proof forest, with nodes having arbitrary rather than boolean values. In this paper, we focus on finite circuits. We present a flexible algorithm for efficiently querying
node values as they change under updates to the circuit's inputs. Unlike traditional algorithms, ours is agnostic about which nodes are tabled (materialized), and can vary smoothly between the traditional strategies of forward and backward chaining. Our algorithm is designed to admit future generalizations, including cyclic and infinite circuits and propagation of delta updates.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.425/LIPIcs.ICLP.2012.425.pdf
arithmetic circuits
memoization
view maintenance
logic programming
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
439
444
10.4230/LIPIcs.ICLP.2012.439
article
Software Model Checking by Program Specialization
De Angelis, Emanuele
We introduce a general verification framework based on program specialization to prove properties of the runtime behaviour of imperative programs. Given a program P written in a programming language L and a property phi in a logic M, we can verify that phi holds for P by: (i) writing an interpreter I for L and a semantics S
for M in a suitable metalanguage, (ii) specializing I and S with respect to P and phi, and (iii) analysing the specialized program by performing a further specialization. We have instantiated our framework to verify safety properties of a simple imperative language, called SIMP, extended with a nondeterministic choice operator. The method is fully automatic and it has been implemented using the MAP transformation system.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.439/LIPIcs.ICLP.2012.439.pdf
Software model checking
program specialization
constraint logic programming.
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
445
450
10.4230/LIPIcs.ICLP.2012.445
article
Temporal Answer Set Programming
Diéguez, Martín
Answer Set Programming (ASP) has become a popular way for representing different kinds of scenarios from knowledge representation in Artificial Intelligence. Frequently, these scenarios
involve a temporal component which must be considered. In ASP, time is usually represented as a variable whose values are defined by an extensional predicate with a finite domain. Dealing with a finite temporal interval has some disadvantages. First, checking the existence of a plan is not possible and second, it also makes difficult to decide whether two programs are strongly equivalent.
If we extend the syntax of Answer Set Programming by using temporal operators from temporal modal logics, then infinite time can be considered, so the aforementioned disadvantages can be overcome. This extension constitutes, in fact, a formalism called Temporal Equilibrium Logic, which is based on Equilibrium Logic (a logical characterisation of ASP).
Although recent contributions have shown promising results, Temporal Equilibrium Logic is still a novel paradigm and there are many gaps to fill. Our goal is to keep developing this paradigm, filling those gaps and turning it into a suitable framework for temporal reasoning.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.445/LIPIcs.ICLP.2012.445.pdf
Answer Set Programming
Temporal Equilibrium Logic
Linear Temporal Logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
451
457
10.4230/LIPIcs.ICLP.2012.451
article
A Gradual Polymorphic Type System with Subtyping for Prolog
Hadjichristodoulou, Spyros
Although Prolog was designed and developed as an untyped language, there have been numerous attempts at proposing type systems suitable for it. The goal of research in this area has been to make Prolog programming easier and less error-prone not only for novice users, but for the experienced programmer as well. Despite the fact that many of the proposed systems have deep theoretical foundations that add types to Prolog, most Prolog vendors are still unwilling to include any of them in their compiler's releases. Hence standard Prolog remains an untyped language. Our work can be understood as a step towards typed Prolog. We propose an extension to one of the most extensively studied type systems proposed for Prolog, the Mycroft-O'Keefe type system, and present an implementation in XSB-Prolog. The resulting type system can be characterized as a Gradual type system, where the user begins with a completely untyped version of his program, and incrementally obtains information about the possible types of the predicates he defines from the system itself, until type signatures are found for all the predicates in the source code.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.451/LIPIcs.ICLP.2012.451.pdf
Type Inference
Polymorphic Type System
Gradual Typing
Tabling
Answer Subsumption
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
458
463
10.4230/LIPIcs.ICLP.2012.458
article
ASP modulo CSP: The clingcon system
Ostrowski, Max
Answer Set Programming (ASP) has become a prime paradigm for declarative problem solving due to its combination of an easy yet expressive modeling language with high-performance Boolean constraint solving technology. However, certain applications are more naturally modeled by mixing Boolean with non-Boolean constructs, for instance, accounting for resources, fine timings, or functions over finite
domains. The challenge lies in combining the elaborated solving capacities of ASP, like backjumping and conflict-driven learning, with advanced techniques from the area of constraint programming (CP).
I therefore developed the solver clingcon, which follows the approach of modern Satisfiability Modulo Theories (SMT). My research shall contribute to bridging the gap between Boolean and Non-Boolean reasoning, in order to bring out the best of both worlds.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.458/LIPIcs.ICLP.2012.458.pdf
Answer Set Programming
Constraint Programming
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
464
468
10.4230/LIPIcs.ICLP.2012.464
article
An ASP Approach for the Optimal Placement of the Isolation Valves in a Water Distribution System
Peano, Andrea
My Ph.D. Thesis relates to real-life optimization problems in the hydraulic engineering field. More precisely, with the collaboration of computer scientists, operational researchers and hydraulic engineers, I investigate and exploit potentialities of various Operational Research and Artificial Intelligence techniques in order to achieve good (and, whenever possible, optimal) solutions for those particular design issues of the urban hydraulic network that can be effectively modelled as known combinatorial optimization problems. Furthermore, suchdesign issues often require to devise new specialized variants of the known combinatorial optimization problems.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.464/LIPIcs.ICLP.2012.464.pdf
Answer Set Programming
Isolation Valves Positioning
Hydroinformatics
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
469
475
10.4230/LIPIcs.ICLP.2012.469
article
Answer Set Programming with External Sources
Redl, Christoph
Answer Set Programming (ASP) is a well-known problem solving approach based on nonmonotonic logic programs and efficient solvers. To enable access to external information, HEX-programs extend programs with external atoms, which allow for a bidirectional communication
between the logic program and external sources of computation (e.g., description logic reasoners and Web resources). Current solvers evaluate HEX-programs by a translation to ASP itself, in which values of external atoms are guessed and verified after the ordinary answer set computation. This elegant approach does not scale with the number of external accesses in general, in particular in presence of nondeterminism (which is instrumental for ASP). Hence, there is a need
for genuine algorithms which handle external atoms as first-class citizens, which is the main focus of this PhD project.
In the first phase of the project, state-of-the-art conflict driven algorithms were already integrated into the prototype system dlvhex and extended to external sources. In particular, the evaluation of external sources may trigger a learning procedure, such that the reasoner gets additional information about the internals of external sources. Moreover, problems on the second level of the polynomial hierarchy were addressed by integrating a minimality check, based on
unfounded sets. First experimental results show already clear improvements.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.469/LIPIcs.ICLP.2012.469.pdf
Answer Set Programming
Nonmonotonic Reasoning
External Computation
FLP Semantics
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-05
17
476
480
10.4230/LIPIcs.ICLP.2012.476
article
Together, Is Anything Possible? A Look at Collective Commitments for Agents
Wright, Ben
In this research, commitments - specifically collective commitments - are looked at as a way to model connections between agents in groups. Using the concepts and ideas from action languages, we propose to model these commitments as actions along with the other basic actions that autonomous agents are capable of performing. The languages developed will be tested against different examples from various multi-agent system (MAS) areas and implemented to run in answer set programming.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol017-iclp2012/LIPIcs.ICLP.2012.476/LIPIcs.ICLP.2012.476.pdf
Reasoning About Knowledge
Action Languages
Commitments
Multi-agent systems
Modal Logic