Arrow Research search

Author name cluster

Torsten Schaub

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

69 papers
2 author rows

Possible papers

69

ECAI Conference 2025 Conference Paper

Multi-Objective Combinatorial Reconfiguration Considering Cost and Length by Answer Set Programming: Algorithms, Encodings, and Empirical Analysis

  • Kazuki Takada
  • Mutsunori Banbara
  • Takehiro Ito
  • Jun Kawahara
  • Shin-ichi Minato
  • Torsten Schaub
  • Ryuhei Uehara

We introduce the Multi-Objective Combinatorial Reconfiguration Optimization Problem (MO-CROP), and propose an Answer Set Programming (ASP) based approach for its solution. MO-CROP involves finding the Pareto-optimal sequences (or Pareto front) of adjacent feasible solutions between two given feasible solutions of a combinatorial problem, considering both cost and length. Our algorithm is compactly implemented through multi-shot ASP solving, and its implementing solver optirecon provides an effective tool for solving MO-CROP. As a concrete example of MO-CROP, we present an ASP encoding for solving the multi-objective independent set reconfiguration optimization problem. Experimental results on the benchmark set from the recent CoRe Challenge demonstrate our approach’s ability to capture diverse optimal sequences that reveal trade-offs between cost and length, a capability often lacking in traditional combinatorial reconfiguration methods.

KR Conference 2024 System Paper

Large Neighborhood Prioritized Search for Combinatorial Optimization with Answer Set Programming

  • Irumi Sugimori
  • Katsumi Inoue
  • Hidetomo Nabeshima
  • Torsten Schaub
  • Takehide Soh
  • Naoyuki Tamura
  • Mutsunori Banbara

We propose Large Neighborhood Prioritized Search (LNPS) for solving combinatorial optimization problems in Answer Set Programming (ASP). LNPS is a metaheuristic that starts with an initial solution and then iteratively tries to find better solutions by alternately destroying and prioritized searching for a current solution. Due to the variability of neighborhoods, LNPS allows for flexible search without strongly depending on the destroy operators. We present an implementation of LNPS based on ASP. The resulting heulingo solver demonstrates that LNPS can significantly enhance the solving performance of ASP for optimization. Furthermore, we establish the competitiveness of our LNPS approach by empirically contrasting it to (adaptive) large neighborhood search.

AIJ Journal 2023 Journal Article

A general framework for preferences in answer set programming

  • Gerhard Brewka
  • James Delgrande
  • Javier Romero
  • Torsten Schaub

We introduce a general, flexible, and extensible framework for quantitative and qualitative preferences among the stable models of logic programs. Since it is straightforward to capture propositional theories and constraint satisfaction problems with logic programs, our approach is also relevant to optimization in satisfiability testing and constraint processing. We show how complex preference relations can be specified through user-defined preference types and their arguments. We describe how preference specifications are handled internally by so-called preference programs, which are used for dominance testing. We also provide algorithms for computing one, or all, preferred stable models of a logic program, and study the complexity of these problems. We implemented our approach in the asprin system by means of multi-shot answer set solving technology. We demonstrate the generality and flexibility of our methodology by showing how easily existing preference languages can be implemented in asprin. Finally, we empirically evaluate our contributions and contrast them with dedicated implementations.

JELIA Conference 2023 Conference Paper

Hamiltonian Cycle Reconfiguration with Answer Set Programming

  • Takahiro Hirate
  • Mutsunori Banbara
  • Katsumi Inoue
  • Xiao-Nan Lu
  • Hidetomo Nabeshima
  • Torsten Schaub
  • Takehide Soh
  • Naoyuki Tamura

Abstract The Hamiltonian cycle reconfiguration problem is defined as determining, for a given Hamiltonian cycle problem and two among its feasible solutions, whether one is reachable from another via a sequence of feasible solutions subject to certain transition constraints. We develop an approach to solving the Hamiltonian cycle reconfiguration problem based on Answer Set Programming (ASP). Our approach relies on a high-level ASP encoding and delegates both the grounding and solving tasks to an ASP-based solver. To show the effectiveness of our approach, we conduct experiments on the benchmark set of Flinders Hamiltonian Cycle Project.

SoCS Conference 2023 Conference Paper

Multi-Agent Pathfinding with Predefined Paths: To Wait, or Not to Wait, That Is the Question [Extended Abstract]

  • Jirí Svancara
  • Etienne Tignon
  • Roman Barták
  • Torsten Schaub
  • Philipp Wanko
  • Roland Kaminski

Multi-agent pathfinding is the task of navigating a set of agents in a shared environment without collisions. Finding an optimal plan is a computationally hard problem, therefore, one may want to sacrifice optimality for faster computation time. In this paper, we present our preliminary work on finding a valid solution using only a predefined path for each agent with the possibility of adding wait actions. This restriction makes some instances unsolvable, however, we show instances where this approach is guaranteed to find a solution.

JELIA Conference 2023 Conference Paper

Past-Present Temporal Programs over Finite Traces

  • Pedro Cabalar
  • Martín Diéguez
  • François Laferrière
  • Torsten Schaub

Abstract Extensions of Answer Set Programming with language constructs from temporal logics, such as temporal equilibrium logic over finite traces ( \(\text {TEL}_{\! f}\) ), provide an expressive computational framework for modeling dynamic applications. In this paper, we study the so-called past-present syntactic subclass, which consists of a set of logic programming rules whose body references to the past and head to the present. Such restriction ensures that the past remains independent of the future, which is the case in most dynamic domains. We extend the definitions of completion and loop formulas to the case of past-present formulas, which allows for capturing the temporal stable models of past-present temporal programs by means of an \(\text {LTL}_{\! f}\) expression.

JELIA Conference 2023 Conference Paper

Recongo: Bounded Combinatorial Reconfiguration with Answer Set Programming

  • Yuya Yamada
  • Mutsunori Banbara
  • Katsumi Inoue
  • Torsten Schaub

Abstract We develop an approach called bounded combinatorial reconfiguration for solving combinatorial reconfiguration problems based on Answer Set Programming. The general task is to study the solution spaces of source combinatorial problems and to decide whether or not there are sequences of feasible solutions that have special properties. The resulting recongo solver covers all metrics of the solver track in the most recent international competition on combinatorial reconfiguration (CoRe Challenge 2022). recongo ranked first in the shortest metric of the single-engine solvers track.

SoCS Conference 2022 Conference Paper

Multi-agent Pathfinding on Large Maps Using Graph Pruning: This Way or That Way? (Extended Abstract)

  • Jirí Svancara
  • Philipp Obermeier
  • Matej Husár
  • Roman Barták
  • Torsten Schaub

This paper extends a study on improving the performance of reduction-based solvers for the problem of multi-agent pathfinding. The task is to navigate a set of agents in a graph without collisions. Solvers that reduce this problem to other formalisms often have issues scaling to larger instances in terms of the graph size. A previous study suggests that pruning the graph of most vertices based on a randomly chosen shortest path for each agent. In this paper, we study the effect of different choices of these paths.

AAMAS Conference 2022 Conference Paper

Reduction-based Solving of Multi-agent Pathfinding on Large Maps Using Graph Pruning

  • Matej Husár
  • Jiří Švancara
  • Philipp Obermeier
  • Roman Barták
  • Torsten Schaub

Multi-agent pathfinding is the problem of finding collision-free paths for a set of agents. Solving this problem optimally is computationally hard, therefore many techniques based on reductions to other formalisms were developed. In comparison to search-based techniques, the reduction-based techniques fall behind on large maps even for a small number of agents. To combat this phenomenon, we propose several strategies for pruning vertices off large instances that will most likely not be used by agents. First, we introduce these strategies conceptually and prove which of them maintain completeness and optimality. Eventually, we conduct an exhaustive evaluation and show that graph pruning strategies make reduction-based solvers comparable to search-based techniques on large maps while maintaining their advantage on small dense maps.

KR Conference 2020 Conference Paper

A Uniform Treatment of Aggregates and Constraints in Hybrid ASP

  • Pedro Cabalar
  • Jorge Fandinno
  • Torsten Schaub
  • Philipp Wanko

Characterizing hybrid ASP solving in a generic way is difficult since one needs to abstract from specific theories. Inspired by lazy SMT solving, this is usually addressed by treating theory atoms as opaque. Unlike this, we propose a slightly more transparent approach that includes an abstract notion of a term. Rather than imposing a syntax on terms, we keep them abstract by stipulating only some basic properties. With this, we further develop a semantic framework for hybrid ASP solving and provide aggregate functions for theory variables that adhere to different semantic principles, show that they generalize existing aggregate semantics in ASP and how we can rely on off-the-shelf hybrid solvers for implementation.

ECAI Conference 2020 Conference Paper

An ASP Semantics for Constraints Involving Conditional Aggregates

  • Pedro Cabalar
  • Jorge Fandinno
  • Torsten Schaub
  • Philipp Wanko

We elaborate upon the formal foundations of hybrid Answer Set Programming (ASP) and extend its underlying logical framework with aggregate functions over constraint values and variables. This is achieved by introducing the construct of conditional expressions, which allow for considering two alternatives while evaluating constraints. Which alternative is considered is interpretation-dependent and chosen according to an associated condition. We put some emphasis on logic programs with linear constraints and show how common ASP aggregates can be regarded as particular cases of so-called conditional linear constraints. Finally, we introduce a polynomial-size, modular and faithful translation from our framework into regular (condition-free) Constraint ASP, outlining an implementation of conditional aggregates on top of existing hybrid ASP solvers.

ECAI Conference 2020 Conference Paper

Implementing Dynamic Answer Set Programming over Finite Traces

  • Pedro Cabalar
  • Martín Diéguez
  • Torsten Schaub
  • François Laferrière

We introduce an implementation of an extension of Answer Set Programming (ASP) with language constructs from dynamic (and temporal) logic that provides an expressive computational framework for modeling dynamic applications. Starting from logical foundations, provided by dynamic and temporal equilibrium logics over finite linear traces, we develop a translation of dynamic formulas into temporal logic programs. This provides us with a normal form result establishing the strong equivalence of formulas in different logics. Our translation relies on the introduction of auxiliary atoms to guarantee polynomial space complexity and to provide an embedding that is doomed to be impossible over the same language. Finally, the reduction of dynamic formulas to temporal logic programs allows us to extend ASP with both approaches in a uniform way and to implement both extensions via temporal ASP solvers such as telingo.

AIJ Journal 2019 Journal Article

Gelfond–Zhang aggregates as propositional formulas

  • Pedro Cabalar
  • Jorge Fandinno
  • Torsten Schaub
  • Sebastian Schellhorn

Answer Set Programming (ASP) has become a popular and widespread paradigm for practical Knowledge Representation thanks to its expressiveness and the available enhancements of its input language. One of such enhancements is the use of aggregates, for which different semantic proposals have been made. In this paper, we show that any ASP aggregate interpreted under Gelfond and Zhang's (GZ) semantics can be replaced (under strong equivalence) by a propositional formula. Restricted to the original GZ syntax, the resulting formula is reducible to a disjunction of conjunctions of literals but the formulation is still applicable even when the syntax is extended to allow for arbitrary formulas (including nested aggregates) in the condition. Once GZ-aggregates are represented as formulas, we establish a formal comparison (in terms of the logic of Here-and-There) to Ferraris' (F) aggregates, which are defined by a different formula translation involving nested implications. In particular, we prove that if we replace an F-aggregate by a GZ-aggregate in a rule head, we do not lose answer sets (although more can be gained). This extends the previously known result that the opposite happens in rule bodies, i. e. , replacing a GZ-aggregate by an F-aggregate in the body may yield more answer sets. Finally, we characterize a class of aggregates for which GZ- and F-semantics coincide.

SoCS Conference 2019 Conference Paper

Generalized Target Assignment and Path Finding Using Answer Set Programming

  • Van Nguyen 0001
  • Philipp Obermeier
  • Tran Cao Son
  • Torsten Schaub
  • William Yeoh 0001

In Multi-Agent Path Finding (MAPF), a team of agents needs to find collision-free paths from their starting locations to their respective targets. Combined Target Assignment and Path Finding (TAPF) extends MAPF by including the problem of assigning targets to agents as a precursor to the MAPF problem. A limitation of both models is their assumption that the number of agents and targets are equal, which is invalid in some applications. We address this limitation by generalizing TAPF to allow for (1) unequal number of agents and tasks; (2) tasks to have deadlines by which they must be completed; (3) ordering of groups of tasks to be completed; and (4) tasks that are composed of a sequence of checkpoints that must be visited in a specific order. Further, we model the problem using answer set programming (ASP) to show that customizing the desired variant of the problem is simple -- one only needs to choose the appropriate combination of ASP rules to enforce it. We also demonstrate experimentally that if problem specific information can be incorporated into the ASP encoding then ASP based methods can be efficient and can scale up to solve practical applications.

JELIA Conference 2019 Conference Paper

Lower Bound Founded Logic of Here-and-There

  • Pedro Cabalar
  • Jorge Fandinno
  • Torsten Schaub
  • Sebastian Schellhorn

Abstract A distinguishing feature of Answer Set Programming is that all atoms belonging to a stable model must be founded. That is, an atom must not only be true but provably true. This can be made precise by means of the constructive logic of Here-and-There, whose equilibrium models correspond to stable models. One way of looking at foundedness is to regard Boolean truth values as ordered by letting true be greater than false. Then, each Boolean variable takes the smallest truth value that can be proven for it. This idea was generalized by Aziz to ordered domains and applied to constraint satisfaction problems. As before, the idea is that a, say integer, variable gets only assigned to the smallest integer that can be justified. In this paper, we present a logical reconstruction of Aziz’ idea in the setting of the logic of Here-and-There. More precisely, we start by defining the logic of Here-and-There with lower bound founded variables along with its equilibrium models and elaborate upon its formal properties. Finally, we compare our approach with related ones and sketch future work.

IJCAI Conference 2019 Conference Paper

On the Integration of CP-nets in ASPRIN

  • Mario Alviano
  • Javier Romero
  • Torsten Schaub

Conditional preference networks (CP-nets) express qualitative preferences over features of interest. A Boolean CP-net can express that a feature is preferable under some conditions, as long as all other features have the same value. This is often a convenient representation, but sometimes one would also like to express a preference for maximizing a set of features, or some other objective function on the features of interest. ASPRIN is a flexible framework for preferences in ASP, where one can mix heterogeneous preference relations, and this paper reports on the integration of Boolean CP-nets. In general, we extend ASPRIN with a preference program for CP-nets in order to compute most preferred answer sets via an iterative algorithm. For the specific case of acyclic CP-nets, we provide an approximation by partially ordered set preferences, which are in turn normalized by ASPRIN to take advantage of several highly optimized algorithms implemented by ASP solvers for computing optimal solutions. Finally, we take advantage of a linear-time computable function to address dominance testing for tree-shaped CP-nets.

ICAPS Conference 2018 Conference Paper

ASP-Based Time-Bounded Planning for Logistics Robots

  • Björn Schäpers
  • Tim Niemueller
  • Gerhard Lakemeyer
  • Martin Gebser
  • Torsten Schaub

Manufacturing industries are undergoing a major paradigm shift towards more autonomy. Automated planning and scheduling then becomes a necessity. The Planning and Execution Competition for Logistics Robots in Simulation held at ICAPS is based on this scenario and provides an interesting testbed. However, the posed problem is challenging as also demonstrated by the somewhat weak results in 2017. The domain requires temporal reasoning and dealing with uncertainty. We propose a novel planning system based on Answer Set Programming and the Clingo solver to tackle these problems and incentivize robot cooperation. Our results show a significant performance improvement, both, in terms of lowering computational requirements and better game metrics.

IJCAI Conference 2018 Conference Paper

Evaluation Techniques and Systems for Answer Set Programming: a Survey

  • Martin Gebser
  • Nicola Leone
  • Marco Maratea
  • Simona Perri
  • Francesco Ricca
  • Torsten Schaub

Answer set programming (ASP) is a prominent knowledge representation and reasoning paradigm that found both industrial and scientific applications. The success of ASP is due to the combination of two factors: a rich modeling language and the availability of efficient ASP implementations. In this paper we trace the history of ASP systems, describing the key evaluation techniques and their implementation in actual tools.

KR Conference 2018 Conference Paper

Introducing Temporal Stable Models for Linear Dynamic Logic

  • Anne-Gwenn Bosser
  • Pedro Cabalar
  • Martín Diéguez
  • Torsten Schaub

We propose a new temporal extension of the logic of Hereand-There (HT) and its equilibria obtained by combining it with dynamic logic over (linear) traces. Unlike previous temporal extensions of HT based on linear temporal logic, the dynamic logic features allow us to reason about the composition of actions. For instance, this can be used to exercise fine grained control when planning in robotics, as exemplified by GOLOG. In this paper, we lay the foundations of our approach, and refer to it as Linear Dynamic Equilibrium Logic, or simply DEL. We start by developing the formal framework of DEL and provide relevant characteristic results. Among them, we elaborate upon the relationships to traditional linear dynamic logic and previous temporal extensions of HT.

KR Conference 2018 Conference Paper

Preference Relations by Approximation

  • Mario Alviano
  • Javier Romero
  • Torsten Schaub

Declarative languages for knowledge representation and reasoning provide constructs to define preference relations over the set of possible interpretations, so that preferred models represent optimal solutions of the encoded problem. We introduce the notion of approximation for replacing preference relations with stronger preference relations, that is, relations comparing more pairs of interpretations. Our aim is to accelerate the computation of a non-empty subset of the optimal solutions by means of highly specialized algorithms. We implement our approach in Answer Set Programming (ASP), where problems involving quantitative and qualitative preference relations can be addressed by ASPRIN, implementing a generic optimization algorithm. Unlike this, chains of approximations allow us to reduce several preference relations to the preference relations associated with ASP’s native weak constraints and heuristic directives. In this way, ASPRIN can now take advantage of several highly optimized algorithms implemented by ASP solvers for computing optimal solutions.

IJCAI Conference 2017 Conference Paper

AutoFolio: An Automatically Configured Algorithm Selector (Extended Abstract)

  • Marius Lindauer
  • Frank Hutter
  • Holger H. Hoos
  • Torsten Schaub

Algorithm selection (AS) techniques -- which involve choosing from a set of algorithms the one expected to solve a given problem instance most efficiently -- have substantially improved the state of the art in solving many prominent AI problems, such as SAT, CSP, ASP, MAXSAT and QBF. Although several AS procedures have been introduced, not too surprisingly, none of them dominates all others across all AS scenarios. Furthermore, these procedures have parameters whose optimal values vary across AS scenarios. In this extended abstract of our 2015 JAIR article of the same title, we summarize AutoFolio, which uses an algorithm configuration procedure to automatically select an AS approach and optimize its parameters for a given AS scenario. AutoFolio allows researchers and practitioners across a broad range of applications to exploit the combined power of many different AS methods and to automatically construct high-performance algorithm selectors. We demonstrate that AutoFolio was able to produce new state-of-the-art algorithm selectors for 7 well-studied AS scenarios and matches state-of-the-art performance statistically on all other scenarios. Compared to the best single algorithm for each AS scenario, AutoFolio achieved average speedup factors between 1. 3 and 15. 4.

AIJ Journal 2017 Journal Article

Automatic construction of parallel portfolios via algorithm configuration

  • Marius Lindauer
  • Holger Hoos
  • Kevin Leyton-Brown
  • Torsten Schaub

Since 2004, increases in computational power described by Moore's law have substantially been realized in the form of additional cores rather than through faster clock speeds. To make effective use of modern hardware when solving hard computational problems, it is therefore necessary to employ parallel solution strategies. In this work, we demonstrate how effective parallel solvers for propositional satisfiability (SAT), one of the most widely studied NP-complete problems, can be produced automatically from any existing sequential, highly parametric SAT solver. Our Automatic Construction of Parallel Portfolios (ACPP) approach uses an automatic algorithm configuration procedure to identify a set of configurations that perform well when executed in parallel. Applied to two prominent SAT solvers, Lingeling and clasp, our ACPP procedure identified 8-core solvers that significantly outperformed their sequential counterparts on a diverse set of instances from the application and hard combinatorial category of the 2012 SAT Challenge. We further extended our ACPP approach to produce parallel portfolio solvers consisting of several different solvers by combining their configuration spaces. Applied to the component solvers of the 2012 SAT Challenge gold medal winning SAT Solver pfolioUZK, our ACPP procedures produced a significantly better-performing parallel SAT solver.

IJCAI Conference 2017 Conference Paper

Generalized Target Assignment and Path Finding Using Answer Set Programming

  • Van Nguyen
  • Philipp Obermeier
  • Tran Cao Son
  • Torsten Schaub
  • William Yeoh

In Multi-Agent Path Finding (MAPF), a team of agents needs to find collision-free paths from their starting locations to their respective targets. Combined Target Assignment and Path Finding (TAPF) extends MAPF by including the problem of assigning targets to agents as a precursor to the MAPF problem. A limitation of both models is their assumption that the number of agents and targets are equal, which is invalid in some applications such as autonomous warehouse systems. We address this limitation by generalizing TAPF to allow for (1)~unequal number of agents and tasks; (2)~tasks to have deadlines by which they must be completed; (3)~ordering of groups of tasks to be completed; and (4)~tasks that are composed of a sequence of checkpoints that must be visited in a specific order. Further, we model the problem using answer set programming (ASP) to show that customizing the desired variant of the problem is simple one only needs to choose the appropriate combination of ASP rules to enforce it. We also demonstrate experimentally that if problem specific information can be incorporated into the ASP encoding then ASP based method can be efficient and can scale up to solve practical applications.

ECAI Conference 2016 Conference Paper

A Minimization-Based Approach to Iterated Multi-Agent Belief Change

  • Paul Vicol
  • James P. Delgrande
  • Torsten Schaub

We investigate minimization-based approaches to iterated belief change in multi-agent systems. A network of agents is represented by an undirected graph, where propositional formulas are associated with vertices. Information is shared between vertices via a procedure where each vertex minimizes disagreement with other vertices in the graph. Each iterative approach takes into account the proximity between vertices, with the underlying assumption that information from nearby sources is given higher priority than information from more distant sources. We have identified two main approaches to iteration: in the first approach, a vertex takes into account the information at its immediate neighbours only, and information from more distant vertices is propagated via iteration; in the second approach, a vertex first takes into account information from distance-1 neighbours, then from distance-2 neighbours, and so on, in a prioritized fashion. There prove to be three distinct ways to define the second approach, so in total we have four types of iteration. We define these types formally, find relationships between them, and investigate their basic logical properties. We also implemented the approaches in a software system called Equibel.

IJCAI Conference 2016 Conference Paper

An ASP Semantics for Default Reasoning with Constraints

  • Pedro Cabalar
  • Roland Kaminski
  • Max Ostrowski
  • Torsten Schaub

We introduce the logic of Here-and-There with Constraints in order to capture constraint theories in the non-monotonic setting known from Answer Set Programming (ASP). This allows for assigning default values to constraint variables or to leave them undefined. Also, it provides us with a semantic framework integrating ASP and Constraint Processing in a uniform way. We put some emphasis on logic programs dealing with linear constraints on integer variables, where we further introduce a directional assignment operator. We elaborate upon the formal relation and implementation of these programs in terms of Constraint ASP, sketching an existing system.

IJCAI Conference 2016 Conference Paper

ASP for Anytime Dynamic Programming on Tree Decompositions

  • Bernhard Bliem
  • Benjamin Kaufmann
  • Torsten Schaub
  • Stefan Woltran

Answer Set Programming (ASP) has recently been employed to specify and run dynamic programming (DP) algorithms on tree decompositions, a central approach in the field of parameterized complexity, which aims at solving hard problems efficiently for instances of certain structure. This ASP-based method followed the standard DP approach where tables are computed in a bottom-up fashion, yielding good results for several counting or enumeration problems. However, for optimization problems this approach lacks the possibility to report solutions before the optimum is found, and for search problems it often computes a lot of unnecessary rows. In this paper, we present a novel ASP-based system allowing for "lazy" DP, which utilizes recent multi-shot ASP technology. Preliminary experimental results show that this approach not only yields better performance for search problems, but also outperforms some state-of-the-art ASP encodings for optimization problems in terms of anytime computation, i. e. , measuring the quality of the best solution after a certain timeout.

IJCAI Conference 2016 Conference Paper

Knowledge-Based Sequence Mining with ASP

  • Martin Gebser
  • Thomas Guyet
  • Ren
  • eacute; Quiniou
  • Javier Romero
  • Torsten Schaub

We introduce a framework for knowledge-based sequence mining, based on Answer Set Programming (ASP). We begin by modeling the basic task and refine it in the sequel in several ways. First, we show how easily condensed patterns can be extracted by modular extensions of the basic approach. Second, we illustrate how ASP's preference handling capacities can be exploited for mining patterns of interest. In doing so, we demonstrate the ease of incorporating knowledge into the ASP-based mining process. To assess the trade-off in effectiveness, we provide an empirical study comparing our approach with a related sequence mining mechanism.

AAAI Conference 2016 Conference Paper

Solving Goal Recognition Design Using ASP

  • Tran Son
  • Orkunt Sabuncu
  • Christian Schulz-Hanke
  • Torsten Schaub
  • William Yeoh

Goal Recognition Design involves identifying the best ways to modify an underlying environment that agents operate in, typically by making a subset of feasible actions infeasible, so that agents are forced to reveal their goals as early as possible. Thus far, existing work has focused exclusively on imperative classical planning. In this paper, we address the same problem with a different paradigm, namely, declarative approaches based on Answer Set Programming (ASP). Our experimental results show that one of our ASP encodings is more scalable and is significantly faster by up to three orders of magnitude than the current state of the art.

JELIA Conference 2016 Conference Paper

Writing Declarative Specifications for Clauses

  • Martin Gebser
  • Tomi Janhunen
  • Roland Kaminski
  • Torsten Schaub
  • Shahab Tasharrofi

Abstract Modern satisfiability (SAT) solvers provide an efficient implementation of classical propositional logic. Their input language, however, is based on the conjunctive normal form (CNF) of propositional formulas. To use SAT solver technology in practice, a user must create the input clauses in one way or another. A typical approach is to write a procedural program that generates formulas on the basis of some input data relevant for the problem domain and translates them into CNF. In this paper, we propose a declarative approach where the intended clauses are specified in terms of rules in analogy to answer set programming (ASP). This allows the user to write first-order specifications for intended clauses in a schematic way by exploiting term variables. We develop a formal framework required to define the semantics of such specifications. Moreover, we provide an implementation harnessing state-of-the-art ASP grounders to accomplish the grounding step of clauses. As a result, we obtain a general-purpose clause-level grounding approach for SAT solvers. Finally, we illustrate the capabilities of our specification methodology in terms of combinatorial and application problems.

AAAI Conference 2015 Conference Paper

asprin: Customizing Answer Set Preferences without a Headache

  • Gerhard Brewka
  • James Delgrande
  • Javier Romero
  • Torsten Schaub

In this paper we describe asprin1, a general, flexible, and extensible framework for handling preferences among the stable models of a logic program. We show how complex preference relations can be specified through user-defined preference types and their arguments. We describe how preference specifications are handled internally by so-called preference programs, which are used for dominance testing. We also give algorithms for computing one, or all, optimal stable models of a logic program. Notably, our algorithms depend on the complexity of the dominance tests and make use of multi-shot answer set solving technology.

JAIR Journal 2015 Journal Article

AutoFolio: An Automatically Configured Algorithm Selector

  • Marius Lindauer
  • Holger H. Hoos
  • Frank Hutter
  • Torsten Schaub

Algorithm selection (AS) techniques -- which involve choosing from a set of algorithms the one expected to solve a given problem instance most efficiently -- have substantially improved the state of the art in solving many prominent AI problems, such as SAT, CSP, ASP, MAXSAT and QBF. Although several AS procedures have been introduced, not too surprisingly, none of them dominates all others across all AS scenarios. Furthermore, these procedures have parameters whose optimal values vary across AS scenarios. This holds specifically for the machine learning techniques that form the core of current AS procedures, and for their hyperparameters. Therefore, to successfully apply AS to new problems, algorithms and benchmark sets, two questions need to be answered: (i) how to select an AS approach and (ii) how to set its parameters effectively. We address both of these problems simultaneously by using automated algorithm configuration. Specifically, we demonstrate that we can automatically configure claspfolio 2, which implements a large variety of different AS approaches and their respective parameters in a single, highly-parameterized algorithm framework. Our approach, dubbed AutoFolio, allows researchers and practitioners across a broad range of applications to exploit the combined power of many different AS methods. We demonstrate AutoFolio can significantly improve the performance of claspfolio 2 on 8 out of the 13 scenarios from the Algorithm Selection Library, leads to new state-of-the-art algorithm selectors for 7 of these scenarios, and matches state-of-the-art performance (statistically) on all other scenarios. Compared to the best single algorithm for each AS scenario, AutoFolio achieves average speedup factors between 1.3 and 15.4.

TCS Journal 2015 Journal Article

Learning Boolean logic models of signaling networks with ASP

  • Santiago Videla
  • Carito Guziolowski
  • Federica Eduati
  • Sven Thiele
  • Martin Gebser
  • Jacques Nicolas
  • Julio Saez-Rodriguez
  • Torsten Schaub

Boolean networks provide a simple yet powerful qualitative modeling approach in systems biology. However, manual identification of logic rules underlying the system being studied is in most cases out of reach. Therefore, automated inference of Boolean logical networks from experimental data is a fundamental question in this field. This paper addresses the problem consisting of learning from a prior knowledge network describing causal interactions and phosphorylation activities at a pseudo-steady state, Boolean logic models of immediate-early response in signaling transduction networks. The underlying optimization problem has been so far addressed through mathematical programming approaches and the use of dedicated genetic algorithms. In a recent work we have shown severe limitations of stochastic approaches in this domain and proposed to use Answer Set Programming (ASP), considering a simpler problem setting. Herein, we extend our previous work in order to consider more realistic biological conditions including numerical datasets, the presence of feedback-loops in the prior knowledge network and the necessity of multi-objective optimization. In order to cope with such extensions, we propose several discretization schemes and elaborate upon our previous ASP encoding. Towards real-world biological data, we evaluate the performance of our approach over in silico numerical datasets based on a real and large-scale prior knowledge network. The correctness of our encoding and discretization schemes are dealt with in Appendices A–B.

AAAI Conference 2015 Conference Paper

What’s Hot in the SAT and ASP Competitions

  • Marijn Heule
  • Torsten Schaub

During the Vienna Summer of Logic, the first FLoC Olympic Games were organized, bringing together a dozen competitions related to logic. Here we present the highlights of the Satisfiability (SAT) and Answer Set Programming (ASP) competitions.

IJCAI Conference 2013 Conference Paper

Advanced Conflict-Driven Disjunctive Answer Set Solving

  • Martin Gebser
  • Benjamin Kaufmann
  • Torsten Schaub

We introduce a new approach to disjunctive ASP solving that aims at an equitable interplay between “generating” and “testing” solver units. To this end, we develop novel characterizations of answer sets and unfounded sets allowing for a bidirectional dynamic information exchange between solver units for orthogonal tasks. This results in the new multithreaded disjunctive ASP solver claspD-2, greatly improving the performance of existing systems.

AAAI Conference 2013 Conference Paper

Domain-Specific Heuristics in Answer Set Programming

  • Martin Gebser
  • Benjamin Kaufmann
  • Javier Romero
  • Ramón Otero
  • Torsten Schaub
  • Philipp Wanko

We introduce a general declarative framework for incorporating domain-specific heuristics into ASP solving. We accomplish this by extending the first-order modeling language of ASP by a distinguished heuristic predicate. The resulting heuristic information is processed as an equitable part of the logic program and subsequently exploited by the solver when it comes to non-deterministically assigning a truth value to an atom. We implemented our approach as a dedicated heuristic in the ASP solver clasp and show its great prospect by an empirical evaluation.

AIJ Journal 2012 Journal Article

Conflict-driven answer set solving: From theory to practice

  • Martin Gebser
  • Benjamin Kaufmann
  • Torsten Schaub

We introduce an approach to computing answer sets of logic programs, based on concepts successfully applied in Satisfiability (SAT) checking. The idea is to view inferences in Answer Set Programming (ASP) as unit propagation on nogoods. This provides us with a uniform constraint-based framework capturing diverse inferences encountered in ASP solving. Moreover, our approach allows us to apply advanced solving techniques from the area of SAT. As a result, we present the first full-fledged algorithmic framework for native conflict-driven ASP solving. Our approach is implemented in the ASP solver clasp that has demonstrated its competitiveness and versatility by winning first places at various solver contests.

KR Conference 2012 Short Paper

Stream Reasoning with Answer Set Programming

  • Martin Gebser
  • Torsten Grote
  • Roland Kaminski
  • Philipp Obermeier
  • Orkunt Sabuncu
  • Torsten Schaub

To further illustrate this problem, consider a continuous character stream over alphabet {a, b} along with the task of continuously checking whether the stream at hand matches regular expression (a|b)∗ aa. We represent the stream via atoms of the form read(C, T), indicating that character C is at stream position T. As a first attempt, we may then encode the recognition of (a|b)∗ aa by the rule The advance of Internet and Sensor technology has brought about new challenges evoked by the emergence of continuous data streams. While existing data-stream management systems allow for high-throughput stream processing, they lack complex reasoning capacities. We address this shortcoming and elaborate upon an approach to knowledge-intense stream reasoning based on Answer Set Programming (ASP). The emphasis thus shifts from rapid data processing to complex reasoning. To accommodate this in ASP, we develop new techniques that allow us to formulate problem encodings dealing with emerging as well as expiring data in a seamless way. We thus propose novel language constructs and modeling techniques for specifying and reasoning with timedecaying logic programs. accept: - read(a, T-1), read(a, T). This rule can be seen as an “offline” encoding, which is correct for the initial segment of a stream of successive instances of predicate read, that is, up to the smallest i (if any) such that read(a, i−1) and read(a, i) hold. However, instances of read constitute an “online” data flow, and an accept decision has to be withdrawn when letter b is read, eg. in read(b, i+1). Clearly, solving such a problem with traditional ASP systems requires relaunching the system upon the arrival of each character. Although each time only the last two readings need to be taken into account, neither of the following ways to utilize standard ASP systems is satisfactory from a KRR viewpoint: (a) one may add further rules to explicitly identify outdated readings (in order not to reason about them) among the whole data; (b) an external component may filter readings and pass only the most recent ones on to the ASP system. Major drawbacks of (a) are the increasing size of input data over time and the more involved encoding, required for the sake of “garbage collection. ” Compared to this, (b) might appear tempting, but it relies on external filtering and thus fails to model the scenario at hand within the declarative realm of ASP. To overcome this problem, we propose an ASP-based approach to stream reasoning based on the sliding window model (cf. (Golab and Özsu 2010)). The idea is (i) to read an “offline” encoding just once and (ii) to keep only the n last entries of an “online” data stream. We accomplish this by extending our previous approach to reactive ASP (Gebser et al. 2011) by means for dealing with time-decaying program parts. In our example, this implies that instances of predicate read expire after two steps. Hence, when investigating the stream abba, only the atoms read(b, 3) and read(a, 4) are taken into account, while read(a, 1) and read(b, 2) have already expired and been disposed of. In fact, time-decaying data poses a major challenge to ASP given that fixed encodings must tolerate emerging as well

IJCAI Conference 2011 Conference Paper

Finite Model Computation via Answer Set Programming

  • Martin Gebser
  • Orkunt Sabuncu
  • Torsten Schaub

We show how Finite Model Computation (FMC) of first-order theories can efficiently and transparentlybe solved by taking advantage of an extension of Answer Set Programming, called incremental Answer Set Programming (iASP). The idea is to use the incremental parameter in iASP programs to account for the domain size of a model. The FMC problem is then successively addressed for increasing domain sizes until an answer set, representing a finite model of the original first-order theory, is found. We developed a system based on the iASP solver iClingo and demonstrate its competitiveness.

JELIA Conference 2010 Conference Paper

An Incremental Answer Set Programming Based System for Finite ModelComputation

  • Martin Gebser
  • Orkunt Sabuncu
  • Torsten Schaub

Abstract We address the problem of Finite Model Computation (FMC) of first-order theories and show that FMC can efficiently and transparently be solved by taking advantage of a recent extension of Answer Set Programming (ASP), called incremental Answer Set Programming (iASP). The idea is to use the incremental parameter in iASP programs to account for the domain size of a model. The FMC problem is then successively addressed for increasing domain sizes until an answer set, representing a finite model of the original first-order theory, is found. We implemented a system based on the iASP solver iClingo and demonstrate its competitiveness by showing that it slightly outperforms the winner of the FNT division of CADE’s Automated Theorem Proving (ATP) competition.

JELIA Conference 2010 Conference Paper

Coala: A Compiler from Action Languages to ASP

  • Martin Gebser
  • Torsten Grote
  • Torsten Schaub

Abstract Action languages allow for compactly describing dynamic domains. They are usually implemented by compilation, e. g. , to Answer Set Programming. To this end, we developed a tool, called Coala, offering manifold compilation techniques for several action languages. We provide an overview of the salient and distinctive features of Coala as well as an experimental comparison of them.

KR Conference 2010 Conference Paper

Repair and Prediction (under Inconsistency) in Large Biological Networks with Answer Set Programming

  • Martin Gebser
  • Carito Guziolowski
  • Mihail Ivanchev
  • Torsten Schaub
  • Anne Siegel
  • Philippe Veber
  • Sven Thiele

We address the problem of repairing large-scale biological networks and corresponding yet often discrepant measurements in order to predict unobserved variations. To this end, we propose a range of different operations for altering experimental data and/or a biological network in order to reestablish their mutual consistency—an indispensable prerequisite for automated prediction. For accomplishing repair and prediction, we take advantage of the distinguished modeling and reasoning capacities of Answer Set Programming. We validate our framework by an empirical study on the widely investigated organism Escherichia coli.

AAAI Conference 2008 Conference Paper

A Meta-Programming Technique for Debugging Answer-Set Programs

  • Martin Gebser
  • Torsten Schaub

Answer-set programming (ASP) is widely recognised as a viable tool for declarative problem solving. However, there is currently a lack of tools for developing answer-set programs. In particular, providing tools for debugging answer-set programs has recently been identified as a crucial prerequisite for a wider acceptance of ASP. In this paper, we introduce a meta-programming technique for debugging in ASP. The basic question we address is why interpretations expected to be answer sets are not answer sets of the program to debug. We thus deal with finding semantical errors of programs. The explanations provided by our method are based on an intuitive scheme of errors that relies on a recent characterisation of the answer-set semantics. Furthermore, as we are using a metaprogramming technique, debugging queries are expressed in terms of answer-set programs themselves, which has several benefits: For one, we can directly use ASP solvers for processing debugging queries. Indeed, our technique can easily be implemented, and we devised a corresponding prototype debugging system. Also, our approach respects the declarative nature of ASP, and the capabilities of the system can easily be extended to incorporate differing debugging features.

ECAI Conference 2008 Conference Paper

Advanced Preprocessing for Answer Set Solving

  • Martin Gebser
  • Benjamin Kaufmann
  • André Neumann
  • Torsten Schaub

We introduce the first substantial approach to preprocessing in the context of answer set solving. The idea is to simplify a logic program while identifying equivalences among its relevant constituents. These equivalences are then used for building a compact representation of the program (in terms of Boolean constraints). We implemented our approach as well as a SAT-based technique to reduce Boolean constraints. This allows us to empirically analyze both preprocessing types and to demonstrate their computational impact.

KR Conference 2008 Conference Paper

Belief Revision of Logic Programs under Answer Set Semantics

  • James Delgrande
  • Torsten Schaub
  • Hans Tompits
  • Stefan Woltran

We address the problem of belief revision in (nonmonotonic) logic programming under answer set semantics: given logic programs P and Q, the goal is to determine a program R that corresponds to the revision of P by Q, denoted P * Q. Unlike previous approaches in logic programming, our formal techniques are analogous to those of distance-based belief revision in propositional logic. In developing our results, we build upon the model theory of logic programs furnished by SE models. Since SE models provide a formal, monotonic characterisation of logic programs, we can adapt well-known techniques from the area of belief revision to revision in logic programs We investigate two specific operators: (logic program) expansion and a revision operator based on the distance between the SE models of logic programs. It proves to be the case that expansion is an interesting operator in its own right, unlike in classical AGM-style belief revision where it is relatively uninteresting. Expansion and revision are shown to satisfy a suite of interesting properties; in particular, our revision operators satisfy the majority of the AGM postulates for revision. A complexity analysis reveals that our revision operators do not increase the complexity of the base formalism. As a consequence, we present an encoding for computing the revision of a logic program by another, within the same logic programming framework.

KR Conference 2008 Conference Paper

Conflict-Driven Disjunctive Answer Set Solving

  • Christian Drescher
  • Martin Gebser
  • Torsten Grote
  • Benjamin Kaufmann
  • Arne Koenig
  • Max Ostrowski
  • Torsten Schaub

We elaborate a uniform approach to computing answer sets of disjunctive logic programs based on state-of-the-art Boolean constraint solving techniques. Starting from a constraint-based characterization of answer sets, we develop advanced solving algorithms, featuring backjumping and conflict-driven learning using the First-UIP scheme as well as sophisticated unfounded set checking. As a final result, we obtain a competitive solver for $Sigma_2^P$-complete problems, taking advantage of Boolean constraint solving technology without using any legacy solvers as black boxes.

IJCAI Conference 2007 Conference Paper

  • James P. Delgrande
  • J
  • eacute; r
  • ocirc; me Lang
  • Torsten Schaub

A general framework for minimisation-based belief change is presented. A problem instance is made up of an undirected graph, where a formula is associated with each vertex. For example, vertices may represent spatial locations, points in time, or some other notion of locality. Information is shared between vertices via a process of minimisation over the graph. We give equivalent semantic and syntactic characterisations of this minimisation. We also show that this approach is general enough to capture existing minimisation-based approaches to belief merging, belief revision, and (temporal) extrapolation operators. While we focus on a set-theoretic notion of minimisation, we also consider other approaches, such as cardinality-based and priority-based minimisation.

IJCAI Conference 2007 Conference Paper

  • Martin Gebser
  • Benjamin Kaufmann
  • Andr
  • eacute; Neumann
  • Torsten Schaub

We introduce a new approach to computing answer sets of logic programs, based on concepts from constraint processing (CSP) and satisfiability checking (SAT). The idea is to view inferences in answer set programming (ASP) as unit propagation on nogoods. This provides us with a uniform constraint-based framework for the different kinds of inferences in ASP. It also allows us to apply advanced techniques from the areas of CSP and SAT. We have implemented our approach in the new ASP solver clasp. Our experiments show that the approach is competitive with state-of-the-art ASP solvers.

ECAI Conference 2006 Conference Paper

On Probing and Multi-Threading in Platypus

  • Jean Gressmann
  • Tomi Janhunen
  • Robert E. Mercer
  • Torsten Schaub
  • Sven Thiele
  • Richard Tichy

The PLATYPUS approach offers a generic platform for distributed answer set solving, accommodating a variety of different architectures for distributing the search for answer sets across different processes and different search modes for modifying search behaviour. We describe two major extensions of PLATYPUS. First, we present its probing mode which provides a controlled non-linear traversal of the search space. Second, we present its new multi-threading architecture allowing for intra-process distribution. Both contributions are underpinned by experimental results illustrating their computational impact.

ECAI Conference 2006 Conference Paper

What's a Head Without a Body?

  • Christian Anger
  • Martin Gebser
  • Tomi Janhunen
  • Torsten Schaub

Concepts in Answer Set Programming (ASP) are normally defined in terms of atoms. We show that the treatment of atoms and bodies (of rules) as equitable computational objects may yield exponential speed-ups, even for standard ASP-solvers such as smodels. To this end, we give simple transformations providing solvers with access to both kinds of objects and show that some families of examples can be solved exponentially faster after they have been transformed. We prove that these transformations may yield exponentially smaller search spaces.

LPAR Conference 2005 Conference Paper

The nomore++ Approach to Answer Set Solving

  • Christian Anger
  • Martin Gebser
  • Thomas Linke
  • André Neumann
  • Torsten Schaub

Abstract We present a new answer set solver, called nomore + +, along with its underlying theoretical foundations. A distinguishing feature is that it treats heads and bodies equitably as computational objects. Apart from its operational foundations, we show how it improves on previous work through its new lookahead and its computational strategy of maintaining unfounded-freeness. We underpin our claims by selected experimental results.

NMR Workshop 2004 Conference Paper

Consistency-based approaches to merging knowledge bases: preliminary report

  • James P. Delgrande
  • Torsten Schaub

We present a framework for investigating merging operators for belief sets. This framework is a generalisation of our earlier work concerning consistency-based belief revision and contraction. Two distinct merging operators are identified: in the first approach, belief sources are consistently combined so that the result of merging K1 and K2 is a maximal consistent (if possible) set of formulas comprising the joint knowledge of K1 and K2. This approach then accords to one’s intuitions as to what a “merge” operator should do. The second approach is more akin to a generalised belief revision operator: Two knowledge sources are “projected” onto a third (in the simplest case the trivially true knowledge base). In both cases, we consider the incorporation of entailment-based and consistency-based integrity constraints. Properties of these operators are investigated, primarily by comparing their properties with postulates that have been identified previously in the literature. As well, interrelationships between these approaches and belief revision are given.

ICAPS Conference 2004 Conference Paper

Domain-Specific Preferences for Causal Reasoning and Planning

  • James P. Delgrande
  • Torsten Schaub
  • Hans Tompits

We address the issue of incorporating domain-specific preferences in planning systems, where a preference may be seen as a "soft" constraint that it is desirable, but not necessary, to satisfy. To this end, we identify two types of preferences, choice preferences that give a preference over which formulas (typically subgoals) to establish, and temporal preferences, which specify a desirable ordering on the establishment of formulas. Preferences may be constructed from actions or fluents but, as we show, this distinction is immaterial. In fact, we allow preferences on arbitrary formulas build from action and fluent names. These preference orderings induce preference ordering on resulting plans, the maximal elements of which yield the preferred plans. We argue that the approach is general and flexible; as well, it handles conditional preferences. Our framework is developed in the context of transition systems; hence, it is applicable to a large number of different action languages, including the well-known language C. Furthermore, our results are applicable to general planning formalisms.

KR Conference 2004 Conference Paper

Domain-Specific Preferences for Causal Reasoning and Planning

  • James Delgrande
  • Torsten Schaub
  • Hans Tompits

We address the issue of incorporating domain-specific preferences in planning systems, where a preference may be seen as a soft constraint that it is desirable, but not necessary, to satisfy. To this end, we identify two types of preferences, choice preferences that give a preference over which formulas (typically subgoals) to establish, and temporal preferences, which specify a desirable ordering on the establishment of formulas. Preferences may be constructed from actions or fluents but, as we show, this distinction is immaterial. In fact, we allow preferences on arbitrary formulas build from action and fluent names. These preference orderings induce preference ordering on resulting plans, the maximal elements of which yield the preferred plans. We argue that the approach is general and flexible; as well, it handles conditional preferences. Our framework is developed in the context of transition systems; hence, it is applicable to a large number of different action languages, including the well-known language C. Furthermore, our results are applicable to general planning formalisms.

JELIA Conference 2004 Conference Paper

Profiling Answer Set Programming: The Visualization Component of the noMoRe System

  • Andreas Bösel
  • Thomas Linke
  • Torsten Schaub

Abstract Standard debugging techniques, like sequential tracing, fail in answer set programming due to its purely declarative approach. We address this problem by means of the graph-oriented computational model underlying the noMoRe system. Although this is no generic solution, it offers a way to make the computation of answer sets transparent within the noMoRe framwork. Apart from the visualization of answer sets in terms of their generating rules, the computation can be animated in different ways.

JELIA Conference 2004 Conference Paper

Two Approaches to Merging Knowledge Bases

  • James P. Delgrande
  • Torsten Schaub

Abstract We present a framework for expressing different merging operators for belief sets. This framework is a generalisation of our earlier work concerning consistency-based belief revision and contraction. Two distinct merging operators are identified: in the first approach, belief sources are consistently combined so that the result of merging knowledge bases K 1, .. ., K n is a maximal consistent (if possible) set of formulas comprising the joint knowledge of the knowledge bases. This approach then accords to one’s intuitions as to what a “merge” operator should do. The second approach is more akin to a generalised belief revision operator: Knowledge bases K 1, .. ., K n are “projected” onto another (in the simplest case the trivially true knowledge base). In both cases, we consider the incorporation of entailment-based and consistency-based integrity constraints. Properties of these operators are investigated, primarily by comparing their properties with postulates that have been identified previously in the literature. As well, the interrelationships between these approaches and belief revision is given.

AIJ Journal 2003 Journal Article

A consistency-based approach for belief change

  • James P Delgrande
  • Torsten Schaub

This paper presents a general, consistency-based framework for expressing belief change. The framework has good formal properties while being well-suited for implementation. For belief revision, informally, in revising a knowledge base K by a sentence α, we begin with α and include as much of K as consistently possible. This is done by expressing K and α in disjoint languages, asserting that the languages agree on the truth values of corresponding atoms wherever consistently possible, and then re-expressing the result in the original language of K. There may be more than one way in which the languages of K and α can be so correlated: in choice revision, one such “extension” represents the revised state; alternately (skeptical) revision consists of the intersection of all such extensions. Contraction is similarly defined although, interestingly, it is not interdefinable with revision. The framework is general and flexible. For example, one could go on and express other belief change operations such as update and erasure, and the merging of knowledge bases. Further, the framework allows the incorporation of static and dynamic integrity constraints. The approach is well-suited for implementation: belief change can be equivalently expressed in terms of a finite knowledge base; and the scope of a belief change operation can be restricted to just those propositions common to the knowledge base and sentence for change. We give a high-level algorithm implementing the procedure, and an expression of the approach in Default Logic. Lastly, we briefly discuss two implementations of the approach.

NMR Workshop 2002 Conference Paper

A polynomial translation of logic programs with nested expressions into disjunctive logic programs: preliminary report

  • David Pearce 0001
  • Vladimir Sarsakov
  • Torsten Schaub
  • Hans Tompits
  • Stefan Woltran

Nested logic programs have recently been introduced in order to allow for arbitrarily nested formulas in the heads and the bodies of logic program rules under the answer sets semantics. Nested expressions can be formed using conjunction, disjunction, as well as the negation as failure operator in an unrestricted fashion. This provides a very flexible and compact framework for knowledge representation and reasoning. Previous results show that nested logic programs can be transformed into standard (unnested) disjunctive logic programs in an elementary way, applying the negation as failure operator to body literals only. This is of great practical relevance since it allows us to evaluate nested logic programs by means of off-the-shelf disjunctive logic programming systems, like DLV. However, it turns out that this straightforward transformation results in an exponential blow-up in the worst-case, despite the fact that complexity results indicate that there is a polynomial translation among both formalisms. In this paper, we take up this challenge and provide a polynomial translation of logic programs with nested expressions into disjunctive logic programs. Moreover, we show that this translation is modular and (strongly) faithful. We have implemented both the straightforward as well as our advanced transformation; the resulting compiler serves as a front-end to DLV and is publicly available on the Web.

JELIA Conference 2002 Conference Paper

COBA: A Consistency-Based Belief Revision System

  • James P. Delgrande
  • Aaron Hunter 0001
  • Torsten Schaub

Abstract Although the theory of belief revision has been studied extensively, there has not been a great deal of emphasis put on the implementation of belief revision systems. In a recent paper, two of the authors presented a newconsistencybased approach to belief revision, and it was argued that the approach was well suited for implementation [ 3 ], [ 2 ]. In order to test this claim, we implemented the system as a simple java applet. In this paper, we will present a partial sketch of the approach to revision, and we will walk through the simple algorithm used to implement it. Although the system could still be improved in terms of efficiency, we found that the approach to belief revision under consideration was, in fact, well suited for implementation.

NMR Workshop 2002 Conference Paper

Optimality theory through default logic

  • Philippe Besnard
  • Robert E. Mercer
  • Torsten Schaub

Optimality Theory is an approach to linguistic problems which is based on rules with exceptions, resorting to a ranking among rules to resolve conflicts arising from competing rules. In such a way, dealing with linguistic problems amounts to applying rules with exceptions: That is reasoning. A related issue is then about a formalization of the logic at work. An immediate candidate is Default Logic which is dedicated to reasoning from rules with exceptions. Moreover, there are versions of default logic with priorities. We show that Default Logic is well-suited as a specification language capturing Optimality Theory and suggests that implementations of default logic can be applied to run experiments with grammatical interaction in the sense of Optimality Theory and beyond.

JELIA Conference 2002 Conference Paper

Paraconsistent Reasoning via Quantified Boolean Formulas, I: Axiomatising Signed Systems

  • Philippe Besnard
  • Torsten Schaub
  • Hans Tompits
  • Stefan Woltran

Signed systems were introduced as a general, syntax-independent framework for paraconsistent reasoning, that is, non-trivialised reasoning from inconsistent information. In this paper, we show how the family of corresponding paraconsistent consequence relations can be axiomatised by means of quantified Boolean formulas. This approach has several benefits. First, it furnishes an axiomatic specification of paraconsistent reasoning within the framework of signed systems. Second, this axiomatisation allows us to identify upper bounds for the complexity of the different signed consequence relations. We strengthen these upper bounds by providing strict complexity results for the considered reasoning tasks. Finally, we obtain an implementation of different forms of paraconsistent reasoning by appeal to the existing system QUIP.

NMR Workshop 2002 Conference Paper

Preferred well-founded semantics for logic programming by alternating fixpoints: preliminary report

  • Torsten Schaub
  • Kewen Wang 0001

We analyze the problem of defining wellfounded semantics for ordered logic programs within a general framework based on alternating fixpoint theory. We start by showing that generalizations of existing answer set approaches to preference are too weak in the setting of wellfounded semantics. We then specify some informal yet intuitive criteria and propose a semantical framework for preference handling that is more suitable for defining well-founded semantics for ordered logic programs. The suitability of the new approach is convinced by the fact that many attractive properties are satisfied by our semantics. In particular, our semantics is still correct with respect to various existing answer sets semantics while it successfully overcomes the weakness of their generalization to well-founded semantics. Finally, we indicate how an existing preferred well-founded semantics can be captured within our semantical framework.

JELIA Conference 2000 Conference Paper

A Compilation of Brewka and Eiter's Approach to Prioritization

  • James P. Delgrande
  • Torsten Schaub
  • Hans Tompits

Abstract In previous work, we developed a framework for expressing general preference information in default logic and logic programming. Here we show that the approach of Brewka and Eiter can be captured within this framework. Hence, the present results demonstrate that our framework is general enough to capture other independently-developed methodologies. As well, since the extended logic program framework has been implemented, we provide an implementation of the Brewka and Eiter approach via an encoding of their approach.

AIJ Journal 2000 Journal Article

Alternative foundations for Reiter's default logic

  • Thomas Linke
  • Torsten Schaub

We introduce an alternative conceptual basis for default reasoning in Reiter's default logic. In fact, most formal or computational treatments of default logic suffer from the necessity of exhaustive consistency checks with respect to the finally resulting set of conclusions; often this so-called extension is just about being constructed. On the theoretical side, this exhaustive approach is reflected by the usual fixed-point characterizations of extensions. Our goal is to reduce such global considerations to local and strictly necessary ones. For this purpose, we develop various techniques and instruments that draw on an analysis of interaction patterns between default rules, embodied by their mutual blocking behavior. These formal tools provide us with alternative means for addressing a variety of questions in default logic. We demonstrate the utility of our approach by applying it to three traditional problems. First, we obtain a range of criteria guaranteeing the existence and non-existence of extensions. Second, we get alternative characterizations of extensions that avoid fixed-point conditions. Finally, we furnish a formal account of default proofs that was up to now neglected in the literature.

AIJ Journal 2000 Journal Article

Expressing preferences in default logic

  • James P. Delgrande
  • Torsten Schaub

We address the problem of reasoning about preferences among properties (outcomes, desiderata, etc.) in Reiter's default logic. Preferences are expressed using an ordered default theory, consisting of default rules, world knowledge, and an ordering, reflecting preference, on the default rules. In contrast with previous work in the area, we do not rely on prioritised versions of default logic, but rather we transform an ordered default theory into a second, standard default theory wherein the preferences are respected, in that defaults are applied in the prescribed order. This translation is accomplished via the naming of defaults, so that reference may be made to a default rule from within a theory. In an elaboration of the approach, we allow an ordered default theory where preference information is specified within a default theory. Here one may specify preferences that hold by default, in a particular context, or give preferences among preferences. In the approach, one essentially axiomatises how different orderings interact within a theory and need not rely on metatheoretic characterisations. As well, we can immediately use existing default logic theorem provers for an implementation. From a theoretical point of view, this shows that the explicit representation of priorities among defaults adds nothing to the overall expressibility of default logic.

AIJ Journal 1998 Journal Article

Prolog technology for default reasoning: proof theory and compilation techniques

  • Torsten Schaub
  • Stefan Brüning

The aim of this work is to show how Prolog technology can be used for efficient implementation of query answering in default logics. The idea is to translate a default theory along with a query into a Prolog program and a Prolog query such that the original query is derivable from the default theory iff the Prolog query is derivable from the Prolog program. In order to comply with the goal-oriented proof search of this approach, we focus on default theories supporting local proof procedures, as exemplified by so-called semi-monotonic default theories. Although this does not capture general default theories under Reiter's interpretation, it does so under alternative ones'. For providing theoretical underpinnings, we found the resulting compilation techniques upon a top-down proof procedure based on model elimination. We show how the notion of a model elimination proof can be refined to capture default proofs and how standard techniques for implementing and improving model elimination theorem provers (regularity, lemmas) can be adapted and extended to default reasoning. This integrated approach allows us to push the concepts needed for handling defaults from the underlying calculus onto the resulting compilation techniques. This method for default theorem proving is complemented by a model-based approach to incremental consistency checking. We show that the crucial task of consistency checking can benefit from keeping models in order to restrict the attention to ultimately necessary consistency checks. This is supported by the concept of default lemmas that allow for an additional avoidance of redundancy.

AIJ Journal 1994 Journal Article

Alternative approaches to default logic

  • James P. Delgrande
  • Torsten Schaub
  • W. Ken Jackson

Reiter's default logic has proven to be an enduring and versatile approach to non-monotonic reasoning. Subsequent work in default logic has concentrated in two major areas. First, modifications have been developed to extend and augment the approach. Second, there has been ongoing interest in semantic foundations for default logic. In this paper, a number of variants of default logic are developed to address differing intuitions arising from the original and subsequent formulations. First, we modify the manner in which consistency is used in the definition of a default extension. The idea is that a global rather than local notion of consistency is employed in the formation of a default extension. Second, we argue that in some situations the requirement of proving the antecedent of a default is too strong. A second variant of default logic is developed where this requirement is dropped; subsequently these approaches are combined, leading to a final variant. These variants then lead to default systems which conform to alternative intuitions regarding default reasoning. For all of these approaches, a fixed-point and a pseudo-iterative definition are given; as well a semantic characterisation of these approaches is provided. In the combined approach we argue also that one can now reason about a set of defaults and can determine, for example, if a particular default in a set is redundant. We show the relation of this work to that of Łukaszewicz and Brewka, and to the Theorist system.