### Towards a General Argumentation System based on Answer-Set Programming

Sarah Alice Gaggl
Within the last years, especially since the work proposed by Dung in 1995, argumentation has emerged as a central issue in Artificial Intelligence. With the so called argumentation frameworks (AFs) it is possible to represent statements (arguments) together with a binary attack relation between them. The conflicts between the statements are solved on a semantical level by selecting acceptable sets of arguments. An increasing amount of data requires an automated computation of such solutions. Logic...

### Streaming Aerial Video Textures

Christopher S. Co, Mark A. Duchaineau & Kenneth I. Joy
We present a streaming compression algorithm for huge time-varying aerial imagery. New airborne optical sensors are capable of collecting billion-pixel images at multiple frames per second. These images must be transmitted through a low-bandwidth pipe requiring aggressive compression techniques. We achieve such compression by treating foreground portions of the imagery separately from background portions. Foreground information consists of moving objects, which form a tiny fraction of the total pixels. Background areas are compressed effectively over...

### On Optimal Heuristic Randomized Semidecision Procedures, with Application to Proof Complexity

Edward A. Hirsch & Dmitry Itsykson
The existence of a ($p$-)optimal propositional proof system is a major open question in (proof) complexity; many people conjecture that such systems do not exist. Kraj\'{\i}\v{c}ek and Pudl\'{a}k \cite{KP} show that this question is equivalent to the existence of an algorithm that is optimal\footnote{Recent papers \cite{Monroe} call such algorithms \emph{$p$-optimal} while traditionally Levin's algorithm was called \emph{optimal}. We follow the older tradition. Also there is some mess in terminology here, thus please see formal definitions...

### The Second Chvatal Closure Can Yield Better Railway Timetables

Christian Liebchen & Elmar Swarat
We investigate the polyhedral structure of the Periodic Event Scheduling Problem (PESP), which is commonly used in periodic railway timetable optimization. This is the first investigation of Chvatal closures and of the Chvatal rank of PESP instances. In most detail, we first provide a PESP instance on only two events, whose Chvatal rank is very large. Second, we identify an instance for which we prove that it is feasible over the first Chvatal closure, and...

### WCET Analysis for Preemptive Scheduling

Sebastian Altmeyer & Gernot Gebhard
Hard real-time systems induce strict constraints on the timing of the task set. Validation of these timing constraints is thus a major challenge during the design of such a system. Whereas the derivation of timing guarantees must already be considered complex if tasks are running to completion, it gets even more complex if tasks are scheduled preemptively -- especially due to caches, deployed to improve the average performance. In this paper we propose a new...

### Computing Minimum Spanning Trees with Uncertainty

Michael Hoffmann, Thomas Erlebach, Danny Krizanc, Matús Mihal'ák & Rajeev Raman
We consider the minimum spanning tree problem in a setting where information about the edge weights of the given graph is uncertain. Initially, for each edge $e$ of the graph only a set $A_e$, called an uncertainty area, that contains the actual edge weight $w_e$ is known. The algorithm can update' $e$ to obtain the edge weight $w_e in A_e$. The task is to output the edge set of a minimum spanning tree after a...

### On the decomposition of k-valued rational relations

Jacques Sakarovitch & Rodrigo De Souza
We give a new, and hopefully more easily understandable, structural proof of the decomposition of a $k$-valued transducer into $k$ unambiguous functional ones, a result established by A. Weber in 1996. Our construction is based on a lexicographic ordering of computations of automata and on two coverings that can be build by means of this ordering. The complexity of the construction, measured as the number of states of the transducers involved in the decomposition, improves...

### Column Generation Heuristic for a Rich Arc Routing Problem

Sébastien Lannez, Christian Artigues, Jean Damay & Michel Gendreau
In this paper we address a real world optimisation problem, the Rail Track Inspection Scheduling Problem (RTISP). This problem consists of scheduling network inspection tasks. The objective is to minimise total deadhead distance. A mixed integer formulation of the problem is presented. A column generation based algorithm is proposed to solve this rich arc routing problem. Its performance is analysed by benchmarking a real world dataset from the French national railway company (SNCF). The efficiency...

### Focused Proof Search for Linear Logic in the Calculus of Structures

Nicolas Guenot
The proof-theoretic approach to logic programming has benefited from the introduction of focused proof systems, through the non-determinism reduction and control they provide when searching for proofs in the sequent calculus. However, this technique was not available in the calculus of structures, known for inducing even more non-determinism than other logical formalisms. This work in progress aims at translating the notion of focusing into the presentation of linear logic in this setting, and use some...

### Dedicated Tabling for a Probabilistic Setting

ProbLog is a probabilistic framework that extends Prolog with probabilistic facts. To compute the probability of a query, the complete SLD proof tree of the query is collected as a sum of products. ProbLog applies advanced techniques to make this feasible and to assess the correct probability. Tabling is a well-known technique to avoid repeated subcomputations and to terminate loops. We investigate how tabling can be used in ProbLog. The challenge is that we have...

### Treewidth Reduction for Constrained Separation and Bipartization Problems

Dániel Marx, Barry O'Sullivan & Igor Razgon
We present a method for reducing the treewidth of a graph while preserving all the minimal $s-t$ separators. This technique turns out to be very useful for establishing the fixed-parameter tractability of constrained separation and bipartization problems. To demonstrate the power of this technique, we prove the fixed-parameter tractability of a number of well-known separation and bipartization problems with various additional restrictions (e.g., the vertices being removed from the graph form an independent set). These...

### ATMOS 2006 Abstracts Collection -- Presentations at the 6th Workshop on Algorithmic Methods and Models for Optimization of Railways

Riko Jacob & Matthias Müller-Hannemann
The 6th Workshop on Algorithmic Methods and Models for Optimization of Railways (ATMOS 06) is held on September 14, 2006 in ZÃÂ¼rich, Switzerland (http://algo06.inf.ethz.ch/atmos), as part of the ALGO meeting.

### Dynamic Algorithms for Recoverable Robustness Problems

Serafino Cicerone, Gabriele Di Stefano, Michael Schachtebeck & Anita Schöbel
Recently, the recoverable robustness model has been introduced in the optimization area. This model allows to consider disruptions (input data changes) in a unified way, that is, during both the strategic planning phase and the operational phase. Although the model represents a significant improvement, it has the following drawback: we are typically not facing only one disruption, but many of them might appear one after another. In this case, the solutions provided in the context...

### Uniqueness, Continuity, and Existence of Implicit Functions in Constructive Analysis

Hannes Diener & Peter Schuster
We extract a quantitative variant of uniqueness from the usual hypotheses of the implicit functions theorem. This leads not only to an a priori proof of continuity, but also to an alternative, fully constructive existence proof.

### Realizing the Dependently Typed Lambda Calculus

Zachary Snow
Dependently typed lambda calculi such as the Edinburgh Logical Framework (LF) can encode relationships between terms in types and can naturally capture correspondences between formulas and their proofs. Such calculi can also be given a logic programming interpretation: the system is based on such an interpretation of LF. We have considered whether a conventional logic programming language can also provide the benefits of a Twelf-like system for encoding type and term dependencies through dependent typing,...

### On extracting computations from propositional proofs (a survey)

Pavel Pudlák
This paper describes a project that aims at showing that propositional proofs of certain tautologies in weak proof system give upper bounds on the computational complexity of functions associated with the tautologies. Such bounds can potentially be used to prove (conditional or unconditional) lower bounds on the lengths of proofs of these tautologies and show separations of some weak proof systems. The prototype are the results showing the feasible interpolation property for resolution. In order...

### Intrinsic Universality in Self-Assembly

David Doty, Jack H. Lutz, Matthew J. Patitz, Scott M. Summers & Damien Woods
We show that the Tile Assembly Model exhibits a strong notion of universality where the goal is to give a single tile assembly system that simulates the behavior of any other tile assembly system. We give a tile assembly system that is capable of simulating a very wide class of tile systems, including itself. Specifically, we give a tile set that simulates the assembly of any tile assembly system in a class of systems that...

### Cardinality and counting quantifiers on omega-automatic structures

Lukasz Kaiser, Sasha Rubin & Vince Bárány
We investigate structures that can be represented by omega-automata, so called omega-automatic structures, and prove that relations defined over such structures in first-order logic expanded by the first-order quantifiers there exist at most $aleph_0$ many', 'there exist finitely many' and 'there exist $k$ modulo $m$ many' are omega-regular. The proof identifies certain algebraic properties of omega-semigroups. As a consequence an omega-regular equivalence relation of countable index has an omega-regular set of representatives. This implies Blumensath's...

### ATMOS Preface -- Algorithmic Methods and Models for Optimization of Railways

Leo G. Kroon & Rolf H. Möhring
This issue contains six papers that were presented in preliminary form at the 5th Workshop on Algorithmic Methods and Models for Optimization of Railways (ATMOS 2005), held at Palma de Mallorca, Spain, October 7, 2005 in conjunction with ALGO 2005. These papers are representative of several areas of research within the scope of ATMOS: rolling stock circulation and engine assignment, station location, line planning, railway traffic scheduling and dispatching, transfer optimization within network design, and...

### Trimmed Moebius Inversion and Graphs of Bounded Degree

Andreas Björklund, Thore Husfeldt, Petteri Kaski & Mikko Koivisto
We study ways to expedite Yates's algorithm for computing the zeta and Moebius transforms of a function defined on the subset lattice. We develop a trimmed variant of Moebius inversion that proceeds point by point, finishing the calculation at a subset before considering its supersets. For an $n$-element universe $U$ and a family $scr F$ of its subsets, trimmed Moebius inversion allows us to compute the number of packings, coverings, and partitions of $U$ with...

### The Complexity of Integrating Routing Decisions in Public Transportation Models

Marie Schmidt & Anita Schöbel
To model and solve optimization problems arising in public transportation, data about the passengers is necessary and has to be included in the models in any phase of the planning process. Many approaches assume a two-step procedure: in a first step, the data about the passengers is distributed over the public transportation network using traffic-assignment procedures. In a second step, the actual planning of lines, timetables, etc. takes place. This approach ignores that for most...

### Computing Least Fixed Points of Probabilistic Systems of Polynomials

Javier Esparza, Andreas Gaiser & Stefan Kiefer
We study systems of equations of the form $X_1 = f_1(X_1, \ldots, X_n), \ldots, X_n = f_n(X_1, \ldots, X_n)$ where each $f_i$ is a polynomial with nonnegative coefficients that add up to~$1$. The least nonnegative solution, say~$\mu$, of such equation systems is central to problems from various areas, like physics, biology, computational linguistics and probabilistic program verification. We give a simple and strongly polynomial algorithm to decide whether $\mu=(1,\ldots,1)$ holds. Furthermore, we present an algorithm...

### Unique Normal Forms in Infinitary Weakly Orthogonal Rewriting

Joerg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Jan Willem Klop & Vincent Van Oostrom
We present some contributions to the theory of infinitary rewriting for weakly orthogonal term rewrite systems, in which critical pairs may occur provided they are trivial. We show that the infinitary unique normal form property (UNinf) fails by a simple example of a weakly orthogonal TRS with two collapsing rules. By translating this example, we show that UNinf also fails for the infinitary lambda-beta-eta-calculus. As positive results we obtain the following: Infinitary confluence, and hence...

### Evasiveness and the Distribution of Prime Numbers

László Babai, Anandam Banerjee, Raghav Kulkarni & Vipul Naik
A Boolean function on $N$ variables is called \emph{evasive} if its decision-tree complexity is $N$. A sequence $B_n$ of Boolean functions is \emph{eventually evasive} if $B_n$ is evasive for all sufficiently large $n$. We confirm the eventual evasiveness of several classes of monotone graph properties under widely accepted number theoretic hypotheses. In particular we show that Chowla's conjecture on Dirichlet primes implies that (a) for any graph $H$, forbidden subgraph $H$'' is eventually evasive and...

### Declarative Debugging of Missing Answers for Maude

Adrian Riesco, Alberto Verdejo & Narciso Marti-Oliet
Declarative debugging is a semi-automatic technique that starts from an incorrect computation and locates a program fragment responsible for the error by building a tree representing this computation and guiding the user through it to find the error. Membership equational logic (MEL) is an equational logic that in addition to equations allows the statement of membership axioms characterizing the elements of a sort. Rewriting logic is a logic of change that extends MEL by adding...

• 2010
453

• Text
453

• Dagstuhl
453