Technical Communications of the 28th International Conference on Logic Programming (ICLP'12), ICLP 2012, September 4-8, 2012, Budapest, Hungary
ICLP 2012
September 4-8, 2012
Budapest, Hungary
International Conference on Logic Programming
ICLP
https://www.cs.nmsu.edu/ALP/conferences/
https://dblp.org/db/conf/iclp
Leibniz International Proceedings in Informatics
LIPIcs
https://www.dagstuhl.de/dagpub/1868-8969
https://dblp.org/db/series/lipics
1868-8969
Agostino
Dovier
Agostino Dovier
Vítor
Santos Costa
Vítor Santos Costa
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
17
2012
978-3-939897-43-9
https://www.dagstuhl.de/dagpub/978-3-939897-43-9
Frontmatter, Table of Contents, List of Authors
Frontmatter, Table of Contents, List of Authors
Frontmatter
Table of Contents
List of Authors
i-xvi
Front Matter
Agostino
Dovier
Agostino Dovier
Vítor
Santos Costa
Vítor Santos Costa
10.4230/LIPIcs.ICLP.2012.i
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Introduction to the Technical Communications of the 28th International Conference on Logic Programming Special Issue
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).
Logic Programming
Organization Details
17-21
Regular Paper
Agostino
Dovier
Agostino Dovier
Vítor
Santos Costa
Vítor Santos Costa
10.4230/LIPIcs.ICLP.2012.xvii
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Simulation Unification: Beyond Querying Semistructured Data (Invited Talk)
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.
Simulation Unification
(Semantic) Web Querying
1-13
Invited Talk
François
Bry
François Bry
Sebastian
Schaffert
Sebastian Schaffert
10.4230/LIPIcs.ICLP.2012.1
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Modeling Machine Learning and Data Mining Problems with FO(·)
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.
Knowledge representation and reasoning
declarative modeling
logic programming
knowledge base systems
FO(·)
IDP framework
stemmatology
phylogene
14-25
Regular Paper
Hendrik
Blockeel
Hendrik Blockeel
Bart
Bogaerts
Bart Bogaerts
Maurice
Bruynooghe
Maurice Bruynooghe
Broes
De Cat
Broes De Cat
Stef
De Pooter
Stef De Pooter
Marc
Denecker
Marc Denecker
Anthony
Labarre
Anthony Labarre
Jan
Ramon
Jan Ramon
Sicco
Verwer
Sicco Verwer
10.4230/LIPIcs.ICLP.2012.14
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Answering Why and How questions with respect to a frame-based knowledge base: a preliminary report
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?"
answer set programming
frame based knowledge representation
question answering.
26-36
Regular Paper
Chitta
Baral
Chitta Baral
Nguyen
Ha Vo
Nguyen Ha Vo
Shanshan
Liang
Shanshan Liang
10.4230/LIPIcs.ICLP.2012.26
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Applying Machine Learning Techniques to ASP Solving
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.
Answer Set Programming
Automated Algorithm Selection
Multi-Engine solvers
37-48
Regular Paper
Marco
Maratea
Marco Maratea
Luca
Pulina
Luca Pulina
Francesco
Ricca
Francesco Ricca
10.4230/LIPIcs.ICLP.2012.37
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
An Answer Set Solver for non-Herbrand Programs: Progress Report
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.
Answer Set Programming
non-Herbrand Functions
Answer Set Solving
Knowledge Representation and Reasoning
49-60
Regular Paper
Marcello
Balduccini
Marcello Balduccini
10.4230/LIPIcs.ICLP.2012.49
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Stable Models of Formulas with Generalized Quantifiers (Preliminary Report)
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.
answer set programming
stable model semantics
generalized quantifiers
61-71
Preliminary Report
Joohyung
Lee
Joohyung Lee
Yunsong
Meng
Yunsong Meng
10.4230/LIPIcs.ICLP.2012.61
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Using Answer Set Programming in the Development of Verified Software
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.
Answer Set Programming
verification
SPARK
Ada
contract based verification
safety critical
72-85
Regular Paper
Florian
Schanda
Florian Schanda
Martin
Brain
Martin Brain
10.4230/LIPIcs.ICLP.2012.72
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Generating Event-Sequence Test Cases by Answer Set Programming with the Incidence Matrix
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.
Event-Sequence Testing
Answer Set Programming
Matrix Model
Constraint Programming
Propositional Satisfiability (SAT)
86-97
Regular Paper
Mutsunori
Banbara
Mutsunori Banbara
Naoyuki
Tamura
Naoyuki Tamura
Katsumi
Inoue
Katsumi Inoue
10.4230/LIPIcs.ICLP.2012.86
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Towards Testing Concurrent Objects in CLP
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.
Testing
Glass-box Test Data Generation
Active Objects
Symbolic Execution
98-108
Regular Paper
Elvira
Albert
Elvira Albert
Puri
Arenas
Puri Arenas
Miguel
Gómez-Zamalloa
Miguel Gómez-Zamalloa
10.4230/LIPIcs.ICLP.2012.98
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Visualization of CHR through Source-to-Source Transformation
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.
Source-to-Source Transformation
Constraint Handling Rules
Visualization
109-118
Regular Paper
Slim
Abdennadher
Slim Abdennadher
Nada
Sharaf
Nada Sharaf
10.4230/LIPIcs.ICLP.2012.109
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Static Type Inference for the Q language using Constraint Logic Programming
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.
logic programming
types
static type checking
CSP
CHR
Q language
119-129
Regular Paper
Zsolt
Zombori
Zsolt Zombori
János
Csorba
János Csorba
Péter
Szeredi
Péter Szeredi
10.4230/LIPIcs.ICLP.2012.119
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Improving Lazy Non-Deterministic Computations by Demand Analysis
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.
functional logic programming
implementation
program analysis
130-143
Regular Paper
Michael
Hanus
Michael Hanus
10.4230/LIPIcs.ICLP.2012.130
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
The additional difficulties for the automatic synthesis of specifications posed by logic features in functional-logic languages
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.
Curry
property-oriented specifications
semantics-based inference methods
144-153
Regular Paper
Giovanni
Bacci
Giovanni Bacci
Marco
Comini
Marco Comini
Marco
A. Feliú
Marco A. Feliú
Alicia
Villanueva
Alicia Villanueva
10.4230/LIPIcs.ICLP.2012.144
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
A Concurrent Operational Semantics for Constraint Functional Logic Programming
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.
Constraint logic programming
concurrent logic programming
functional logic programming.
154-163
Regular Paper
Rafael
del Vado Vírseda
Rafael del Vado Vírseda
Fernando
Pérez Morente
Fernando Pérez Morente
Marcos Miguel
García Toledo
Marcos Miguel García Toledo
10.4230/LIPIcs.ICLP.2012.154
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Surviving Solver Sensitivity: An ASP Practitioner’s Guide
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.
algorithm configuration
algorithm selection
portfolio solving
answer set programming
algorithm portfolios
164-175
Regular Paper
Bryan
Silverthorn
Bryan Silverthorn
Yuliya
Lierler
Yuliya Lierler
Marius
Schneider
Marius Schneider
10.4230/LIPIcs.ICLP.2012.164
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
aspeed: ASP-based Solver Scheduling
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.
Algorithm Schedule
Portfolio-based Solving
Answer Set Programming
176-187
Regular Paper
Holger
Hoos
Holger Hoos
Roland
Kaminski
Roland Kaminski
Torsten
Schaub
Torsten Schaub
Marius
Schneider
Marius Schneider
10.4230/LIPIcs.ICLP.2012.176
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Answer Set Solving with Lazy Nogood Generation
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.
Conflict-Driven Nogood Learning
Constraint Answer Set Programming
Constraint Propagation
Lazy Nogood Generation
188-200
Regular Paper
Christian
Drescher
Christian Drescher
Toby
Walsh
Toby Walsh
10.4230/LIPIcs.ICLP.2012.188
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Lazy Model Expansion by Incremental Grounding
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.
Knowledge representation and reasoning
model generation
grounding
IDP framework
first-order logic
201-211
Regular Paper
Broes
De Cat
Broes De Cat
Marc
Denecker
Marc Denecker
Peter
Stuckey
Peter Stuckey
10.4230/LIPIcs.ICLP.2012.201
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Unsatisfiability-based optimization in clasp
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.
answer-set-programming
solvers
212-221
Regular Paper
Benjamin
Andres
Benjamin Andres
Benjamin
Kaufmann
Benjamin Kaufmann
Oliver
Matheis
Oliver Matheis
Torsten
Schaub
Torsten Schaub
10.4230/LIPIcs.ICLP.2012.211
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
An FLP-Style Answer-Set Semantics for Abstract-Constraint Programs with Disjunctions
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.
answer-set programming
abstract constraints
aggregates
disjunction
222-234
Regular Paper
Johannes
Oetsch
Johannes Oetsch
Jörg
Pührer
Jörg Pührer
Hans
Tompits
Hans Tompits
10.4230/LIPIcs.ICLP.2012.222
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Reconciling Well-Founded Semantics of DL-Programs and Aggregate Programs
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.
Well-founded semantics
description logic programs
aggregate logic programs
three-valued logic.
235-246
Regular Paper
Jia-Huai
You
Jia-Huai You
John
Morris
John Morris
Yi
Bi
Yi Bi
10.4230/LIPIcs.ICLP.2012.235
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Preprocessing of Complex Non-Ground Rules in Answer Set Programming
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.
answer set programming
hypertree decomposition
preprocessing
247-258
Regular Paper
Michael
Morak
Michael Morak
Stefan
Woltran
Stefan Woltran
10.4230/LIPIcs.ICLP.2012.247
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Two-Valued Logic Programs
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.
Answer set programming
Non monotonic reasoning
Foundations
259-266
Regular Paper
Vladimir
Lifschitz
Vladimir Lifschitz
10.4230/LIPIcs.ICLP.2012.259
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Possibilistic Nested Logic Programs
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.
Answer Set Programming
Uncertain Information
Possibilistic Reasoning
267-276
Regular Paper
Juan Carlos
Nieves
Juan Carlos Nieves
Helena
Lindgren
Helena Lindgren
10.4230/LIPIcs.ICLP.2012.267
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
A Tarskian Informal Semantics for Answer Set Programming
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.
Answer set programming
informal semantics
generate-define-test
277-289
Regular Paper
Marc
Denecker
Marc Denecker
Yuliya
Lierler
Yuliya Lierler
Miroslaw
Truszczynski
Miroslaw Truszczynski
Joost
Vennekens
Joost Vennekens
10.4230/LIPIcs.ICLP.2012.277
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Paving the Way for Temporal Grounding
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.
ASP
linear temporal logic
grounding
temporal equilibrium logic
290-300
Regular Paper
Felicidad
Aguado
Felicidad Aguado
Pedro
Cabalar
Pedro Cabalar
Martín
Diéguez
Martín Diéguez
Gilberto
Pérez
Gilberto Pérez
Concepción
Vidal
Concepción Vidal
10.4230/LIPIcs.ICLP.2012.290
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Logic + control: An example
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.
program correctness
program completeness
specification
declarative programming
declarative diagnosis.
301-311
Regular Paper
Wlodzimierz
Drabent
Wlodzimierz Drabent
10.4230/LIPIcs.ICLP.2012.301
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Deriving a Fast Inverse of the Generalized Cantor N-tupling Bijection
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 .
generalized Cantor n-tupling bijection
bijective data type transformations
combinatorial number system
solving combinatorial problems in Prolog
op
312-322
Regular Paper
Paul
Tarau
Paul Tarau
10.4230/LIPIcs.ICLP.2012.312
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
On the Termination of Logic Programs with Function Symbols
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.
Logic Programming
Function Symbols
Bottom-up Execution
Program Termination
Stable Models
323-333
Regular Paper
Sergio
Greco
Sergio Greco
Francesca
Spezzano
Francesca Spezzano
Irina
Trubitsyna
Irina Trubitsyna
10.4230/LIPIcs.ICLP.2012.323
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Logic Programming in Tabular Allegories
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.
Category Theory
Logic Programming
Lawvere Categories
Programming Language Semantics
Declarative Programming
334-347
Regular Paper
Emilio Jesús
Gallego Arias
Emilio Jesús Gallego Arias
James
B. Lipton
James B. Lipton
10.4230/LIPIcs.ICLP.2012.334
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Tabling for infinite probability computation
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.
probability
tabling
PRISM
348-358
Regular Paper
Taisuke
Sato
Taisuke Sato
Philipp
Meyer
Philipp Meyer
10.4230/LIPIcs.ICLP.2012.348
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
ASP at Work: An ASP Implementation of PhyloWS
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.
Answer sets
phylogenetic inference
systems
applications
359-369
Regular Paper
Tiep
Le
Tiep Le
Hieu
Nguyen
Hieu Nguyen
Enrico
Pontelli
Enrico Pontelli
Tran
Cao Son
Tran Cao Son
10.4230/LIPIcs.ICLP.2012.359
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
CHR for Social Responsibility
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.
Constraint handling rules
principled decision making
informed voting
client directed voting
social responsibility.
370-380
Regular Paper
Veronica
Dahl
Veronica Dahl
Bradley
Coleman
Bradley Coleman
J. Emilio
Miralles
J. Emilio Miralles
Erez
Maharshak
Erez Maharshak
10.4230/LIPIcs.ICLP.2012.370
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
A Logic Programming approach for Access Control over RDF
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.
Logic Programming
Annotation
Access Control
RDF
381-392
Regular Paper
Nuno
Lopes
Nuno Lopes
Sabrina
Kirrane
Sabrina Kirrane
Antoine
Zimmermann
Antoine Zimmermann
Axel
Polleres
Axel Polleres
Alessandra
Mileo
Alessandra Mileo
10.4230/LIPIcs.ICLP.2012.381
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
LOG-IDEAH: ASP for Architectonic Asset Preservation
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.
Answer set programming
structural engineering
knowledge representation
393-403
Regular Paper
Viviana
Novelli
Viviana Novelli
Marina
De Vos
Marina De Vos
Julian
Padget
Julian Padget
Dina
D’Ayala
Dina D’Ayala
10.4230/LIPIcs.ICLP.2012.393
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Extending C+ with Composite Actions for Robotic Task Planning
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.
Reasoning about Actions
Action Languages
Robotic Task Planning
404-414
Regular Paper
Xiaoping
Chen
Xiaoping Chen
Guoqiang
Jin
Guoqiang Jin
Fangkai
Yang
Fangkai Yang
10.4230/LIPIcs.ICLP.2012.404
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Improving Quality and Efficiency in Home Health Care: an application of Constraint Logic Programming for the Ferrara NHS unit
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.
CLP(FD)
Nurse Scheduling Applications
Home Health Care
415-424
Regular Paper
Massimiliano
Cattafi
Massimiliano Cattafi
Rosa
Herrero
Rosa Herrero
Marco
Gavanelli
Marco Gavanelli
Maddalena
Nonato
Maddalena Nonato
Federico
Malucelli
Federico Malucelli
10.4230/LIPIcs.ICLP.2012.415
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
A Flexible Solver for Finite Arithmetic Circuits
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.
arithmetic circuits
memoization
view maintenance
logic programming
425-438
Regular Paper
Nathaniel Wesley
Filardo
Nathaniel Wesley Filardo
Jason
Eisner
Jason Eisner
10.4230/LIPIcs.ICLP.2012.425
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Software Model Checking by Program Specialization
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.
Software model checking
program specialization
constraint logic programming.
439-444
Regular Paper
Emanuele
De Angelis
Emanuele De Angelis
10.4230/LIPIcs.ICLP.2012.439
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Temporal Answer Set Programming
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.
Answer Set Programming
Temporal Equilibrium Logic
Linear Temporal Logic
445-450
Regular Paper
Martín
Diéguez
Martín Diéguez
10.4230/LIPIcs.ICLP.2012.445
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
A Gradual Polymorphic Type System with Subtyping for Prolog
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.
Type Inference
Polymorphic Type System
Gradual Typing
Tabling
Answer Subsumption
451-457
Regular Paper
Spyros
Hadjichristodoulou
Spyros Hadjichristodoulou
10.4230/LIPIcs.ICLP.2012.451
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
ASP modulo CSP: The clingcon system
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.
Answer Set Programming
Constraint Programming
458-463
Regular Paper
Max
Ostrowski
Max Ostrowski
10.4230/LIPIcs.ICLP.2012.458
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
An ASP Approach for the Optimal Placement of the Isolation Valves in a Water Distribution System
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.
Answer Set Programming
Isolation Valves Positioning
Hydroinformatics
464-468
Regular Paper
Andrea
Peano
Andrea Peano
10.4230/LIPIcs.ICLP.2012.464
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Answer Set Programming with External Sources
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.
Answer Set Programming
Nonmonotonic Reasoning
External Computation
FLP Semantics
469-475
Regular Paper
Christoph
Redl
Christoph Redl
10.4230/LIPIcs.ICLP.2012.469
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Together, Is Anything Possible? A Look at Collective Commitments for Agents
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.
Reasoning About Knowledge
Action Languages
Commitments
Multi-agent systems
Modal Logic
476-480
Regular Paper
Ben
Wright
Ben Wright
10.4230/LIPIcs.ICLP.2012.476
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode