Hans Tompits

JELIA Conference 2019 Conference Paper

\mathsf Uhura: An Authoring Tool for Specifying Answer-Set Programs Using Controlled Natural Language

• Tobias Kain
• Hans Tompits

Abstract In this paper, we present the tool \(\mathsf {Uhura}\) for developing answer-set programs by means of specifying problem descriptions in a controlled natural language which then are translated into answer-set programming (ASP) rules. The tool is aimed for supporting users not familiar with answer-set programming—or logic-based approaches in general—for developing programs. \(\mathsf {Uhura}\) is based on a new controlled natural language called \(\mathsf {L}^{\text {U}}\), which is in turn an adaption of \(\mathsf {PENG}^{\text {ASP}}\), a controlled natural language employed in the PENG ASP system, developed by Guy and Schwitter, for solving computational problems by translating \(\mathsf {PENG}^{\text {ASP}}\) statements into answer-set programs. In contrast to \(\mathsf {PENG}^{\text {ASP}}\), \(\mathsf {L}^{\text {U}}\) allows for a more natural translation into ASP rules and provides also a broader set of pre-defined sentence patterns. \(\mathsf {Uhura}\) is implemented in \(\mathsf {Java}\) and employs \(\mathsf {DLV}\) as backend answer-set solver.

JELIA Conference 2019 Conference Paper

Characterising Relativised Strong Equivalence with Projection for Non-ground Answer-Set Programs

• Tobias Geibinger
• Hans Tompits

Abstract Starting with the seminal work on strong equivalence by Lifschitz, Pearce, and Valverde, many different advanced notions of program equivalence have been studied in the area of answer-set programming (ASP). In particular, relativised strong equivalence with projection has been introduced as a generalisation of strong equivalence by parameterising, on the one hand, the alphabet of the context programs used for checking program equivalence as well as, on the other hand, allowing the filtering of auxiliary atoms. Like many other advanced equivalence notions, it was introduced originally for propositional programs, along with model-theoretic concepts providing characterisations when equivalence between two programs hold. In this paper, we extend these concepts and characterisations to the general case of non-ground programs.

LPAR Conference 2017 Conference Paper

Blocked Clauses in First-Order Logic

• Benjamin Kiesl
• Martin Suda 0001
• Martina Seidl
• Hans Tompits
• Armin Biere

Blocked clauses provide the basis for powerful reasoning techniques used in SAT, QBF, and DQBF solving. Their definition, which relies on a simple syntactic criterion, guarantees that they are both redundant and easy to find. In this paper, we lift the notion of blocked clauses to first-order logic. We introduce two types of blocked clauses, one for first-order logic with equality and the other for first-order logic without equality, and prove their redundancy. In addition, we give a polynomial algorithm for checking whether a clause is blocked. Based on our new notions of blocking, we implemented a novel first-order preprocessing tool. Our experiments showed that many first-order problems in the TPTP library contain a large number of blocked clauses whose elimination can improve the performance of modern theorem provers, especially on satisfiable problem instances.

IJCAI Conference 2017 Conference Paper

Blockedness in Propositional Logic: Are You Satisfied With Your Neighborhood?

• Benjamin Kiesl
• Martina Seidl
• Hans Tompits
• Armin Biere

Clause-elimination techniques that simplify formulas by removing redundant clauses play an important role in modern SAT solving. Among the types of redundant clauses, blocked clauses are particularly popular. For checking whether a clause C is blocked in a formula F, one only needs to consider the so-called resolution neighborhood of C, i. e. , the set of clauses that can be resolved with C. Because of this, blocked clauses are referred to as being locally redundant. In this paper, we discuss powerful generalizations of blocked clauses that are still locally redundant, viz. set-blocked clauses and super-blocked clauses. We furthermore present complexity results for deciding whether a clause is set-blocked or super-blocked.

KR Conference 2012 Conference Paper

On the Small-Scope Hypothesis for Testing Answer-Set Programs

• Johannes Oetsch
• Michael Prischink
• Jörg Pührer
• Martin Schwengerer
• Hans Tompits

Though testing is the prevalent means to find errors in traditional software development, this subject has been addressed for ASP only recently (Janhunen et al. 2010; 2011; Febbraro et al. 2011). In particular, the small-scope hypothesis in traditional testing states that a high proportion of errors can be found by testing a program for all test inputs that are taken from some relatively small scope (Jackson and Damon 1996), i. e., by restricting the number of objects a test input is composed of. This suggests that it can be quite effective to test a program exhaustively for some restricted small scope instead of deliberately selecting test inputs from a larger one. A small-scope hypothesis in ASP would be a matter of interest for two reasons. First, it would allow to devise effective testing methods for uniform problem encodings (the prevailing representation mode ASP is used). For illustration, assume we encoded by means of ASP, using the rules below, the graph problem of testing whether a graph is disconnected, where problem instances are represented by facts over an input signature with predicates edge/2 and node/1: In software testing, the small-scope hypothesis states that a high proportion of errors can be found by testing a program for all test inputs within some small scope. In this paper, we evaluate the small-scope hypothesis for answer-set programming (ASP). To this end, we follow work in traditional testing and base our evaluation on mutation analysis. In fact, we show that a rather limited scope is sufficient for testing ASP encodings from a representative set of benchmark problems. Our experimental evaluation facilitates effective methods for testing in ASP. Also, it gives some justification to analyse programs at the propositional level after grounding them over a small domain.

ECAI Conference 2010 Conference Paper

On Testing Answer-Set Programs

• Tomi Janhunen
• Ilkka Niemelä
• Johannes Oetsch
• Jörg Pührer
• Hans Tompits

Answer-set programming (ASP) is a well-acknowledged paradigm for declarative problem solving, yet comparably little effort has been spent on the investigation of methods to support the development of answer-set programs. In particular, systematic testing of programs, constituting an integral part of conventional software development, has not been discussed for ASP thus far. In this paper, we fill this gap and develop notions enabling the structural testing of answer-set programs, i. e. , we address testing based on test cases that are chosen with respect to the internal structure of a given answer-set program. More specifically, we introduce different notions of coverage that measure to what extent a collection of test inputs covers certain important structural components of the program. In particular, we introduce metrics corresponding to path and branch coverage from conventional testing. We also discuss complexity aspects of the considered notions and give strategies how test inputs that yield increasing (up to total) coverage can be automatically generated.

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.

AIJ Journal 2008 Journal Article

Combining answer set programming with description logics for the Semantic Web

• Thomas Eiter
• Giovambattista Ianni
• Thomas Lukasiewicz
• Roman Schindlauer
• Hans Tompits

KR Conference 2008 Conference Paper

Embedding Approaches to Combining Rules and Ontologies into Autoepistemic Logic

• Jos de Bruijn
• Thomas Eiter
• Hans Tompits

The combination of rules and ontologies has a central role in the ongoing development of the Semantic Web. In previous work, autoepistemic logic (AEL) was advocated as a uniform host formalism to study different such combinations, enabling comparisons on a common basis. In this paper, we continue this line of research and investigate different embeddings of major proposals to combine rules and ontologies into first-order autoepistemic logic (FO-AEL). In particular, we present embeddings for dl-programs, r-hybrid knowledge bases, and hybrid MKNF knowledge bases, which are representatives of different combination types. We study the embeddings in the context of FO-AEL under the standard-names assumption, but we also discuss variants using the any- and all-names semantics. Our results provide interesting insights into the properties of the discussed combination formalisms.

KR Conference 2008 Conference Paper

Notions of Strong Equivalence for Logic Programs with Ordered Disjunction

• Wolfgang Faber
• Hans Tompits
• Stefan Woltran

Ordered disjunctions have been introduced as a simple, yet expressive approach for representing preferential knowledge by means of logic programs. The semantics for the resulting language is based on the answer-set semantics, but comes in different variants, depending on the particular interpretation of preference aggregation associated to the ordered disjunction connective. While in standard answer-set programming the question of when a program is to be considered equivalent to another received increasing attention in recent years, this problem has not been addressed for programs with ordered disjunctions so far. In this paper, we discuss the concept of strong equivalence in this setting. We introduce different versions of strong equivalence for programs with ordered disjunctions and provide model-theoretic characterisations, extending well-known ones for strong equivalence between ordinary logic programs. Furthermore, we discuss the relationships between the proposed notions and study their computational complexity.

IJCAI Conference 2007 Conference Paper

• Thomas Eiter
• Michael Fink
• Hans Tompits
• Stefan Woltran

Recent research in nonmonotonic logic programming under the answer-set semantics focuses on different notions of program equivalence. However, previous results do not address the important classes of stratified programs and its subclass of acyclic (i. e. , recursion-free) programs, although they are recognized as important tools for knowledge representation and reasoning. In this paper, we consider such programs, possibly augmented with constraints. Our results show that in the propositional setting, where reasoning is well-known to be polynomial, deciding strong and uniform equivalence is as hard as for arbitrary normal logic programs (and thus coNP-complete), but is polynomial in some restricted cases. Non-ground programs behave similarly. However, exponential lower bounds already hold for small programs (i. e. , with constantly many rules). In particular, uniform equivalence is undecidable even for small Horn programs plus a single negative constraint.

JELIA Conference 2006 Conference Paper

ccT: A Correspondence-Checking Tool for Logic Programs Under the Answer-Set Semantics

• Johannes Oetsch
• Martina Seidl
• Hans Tompits
• Stefan Woltran

Abstract In recent work, a general framework for specifying correspondences between logic programs under the answer-set semantics has been defined. The framework captures different notions of equivalence, including well-known ones like ordinary, strong, and uniform equivalence, as well as refined ones based on the projection of answer sets where not all parts of an answer set are of relevance. In this paper, we describe an implementation to verify program correspondences in this general framework. The system, called cc⊤, relies on linear-time constructible reductions to quantified propositional logic and uses extant solvers for the latter language as back-end inference engines.

KR Conference 2006 Conference Paper

Replacements in Non-Ground Answer-Set Programming

• Thomas Eiter
• Michael Fink
• Hans Tompits
• Patrick Traxler
• Stefan Woltran

In this paper, we propose a formal framework for specifying rule replacements in nonmonotonic logic programs within the answer-set programming paradigm. Of particular interest are replacement schemas retaining specific notions of equivalence, among them the prominent notions of strong and uniform equivalence, which have been introduced as theoretical tools for program optimization and verification. We derive some general properties of the replacement framework with respect to these notions of equivalence. Moreover, we generalize results about particular replacement schemas which have been established for ground programs to the non-ground case. Finally, we report a number of complexity results which address the problem of deciding how hard it is to apply a replacement to a given program. Our results provide an important step towards the development of effective optimization methods for non-ground answer-set programming, an issue which has not been addressed much so far.

IJCAI Conference 2005 Conference Paper

On Solution Correspondences in Answer-Set Programming

• Thomas Eiter
• Hans Tompits
• Stefan

We introduce a general framework for specifying program correspondence under the answer-set semantics. The framework allows to define different kinds of equivalence notions, including previously defined notions like strong and uniform equivalence, in which programs are extended with rules from a given context, and correspondence is determined by means of a binary relation. In particular, refined equivalence notions based on projected answer sets can be defined within this framework, where not all parts of an answer set are of relevance. We study general characterizations of inclusion and equivalence problems, introducing novel semantical structures. Furthermore, we deal with the issue of determining counterexamples for a given correspondence problem, and we analyze the computational complexity of correspondence checking.

AAAI Conference 2005 Conference Paper

Strong and Uniform Equivalence in Answer-Set Programming: Characterizations and Complexity Results for the Non-Ground Case

• Thomas Eiter
• Hans Tompits

Recent research in nonmonotonic logic programming under the answer-set semantics studies different notions of equivalence. In particular, strong and uniform equivalence are proposed as useful tools for optimizing (parts of) a logic program. While previous research mainly addressed propositional (i. e. , ground) programs, we deal here with the more general case of non-ground programs, and provide semantical characterizations capturing the essence of equivalence, generalizing the concepts of SE-models and UE-models, respectively, as originally introduced for propositional programs. We show that uniform equivalence is undecidable, and we give decidability results and precise complexity bounds for strong equivalence (thereby correcting a previous complexity bound for strong equivalence from the literature) as well as for uniform equivalence for finite vocabularies.

KR Conference 2004 Conference Paper

Combining Answer Set Programming with Description Logics for the Semantic Web

• Thomas Eiter
• Thomas Lukasiewicz
• Roman Schindlauer
• Hans Tompits

Towards the integration of rules and ontologies in the Semantic Web, we propose a combination of logic programming under the answer set semantics with the description logics SHIF(D) and SHOIN(D), which underly the Web ontology languages OWL Lite and OWL DL, respectively. This combination allows for building rules on top of ontologies but also, to a limited extent, building ontologies on top of rules. We introduce description logic programs (dl-programs), which consist of a description logic knowledge base L and a finite set of description logic rules (dl-rules) P. Such rules are similar to usual rules in logic programs with negation as failure, but may also contain queries to L, possibly default negated, in their bodies. We define Herbrand models for dl-programs, and show that satisfiable positive dl-programs have a unique least Herbrand model. More generally, consistent stratified dl-programs can be associated with a unique minimal Herbrand model that is characterized through iterative least Herbrand models. We then generalize the (unique) minimal Herbrand model semantics for positive and stratified dl-programs to a strong answer set semantics for all dl-programs, which is based on a reduction to the least model semantics of positive dl-programs. We also define a weak answer set semantics based on a reduction to the answer sets of ordinary logic programs. Strong answer sets are weak answer sets, and both properly generalize answer sets of ordinary normal logic programs. We then give fixpoint characterizations for the (unique) minimal Herbrand model semantics of positive and stratified dl-programs, and show how to compute these models by finite fixpoint iterations. Furthermore, we give a precise picture of the complexity of deciding strong and weak answer set existence for a dl-program.

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.

LPAR Conference 2004 Conference Paper

Nonmonotonic Description Logic Programs: Implementation and Experiments

• Thomas Eiter
• Giovambattista Ianni
• Roman Schindlauer
• Hans Tompits

Abstract The coupling of description logic reasoning systems with other reasoning formalisms (possibly over the Web) is becoming an important research issue and calls for advanced methods and algorithms. Recently, several notions of description logic programs have been introduced, combining rule-based semantics with description logics. Among them are nonmonotonic description logic programs (or dl-programs for short) which combine nonmonotonic logic programs with description logics under a generalized version of the answer-set and the well-founded semantics, respectively, which are the predominant semantics for nonmonotonic logic programs. In this paper, we consider some technical issues regarding an efficient implementation for both semantics, which has been realized in a working prototype exploiting the two state-of-art tools DLV and RACER. A major issue in this respect is efficient interfacing between the two reasoning systems at hand, for which we devised special methods. Such methods may fruitfully be used for the implementation of systems of similar nature. Reported experimentation activities with our prototype show that the methods we have developed are effective and are a key for highly optimized nonmonotonic dl-program engines.

NMR Workshop 2004 Conference Paper

On acyclic and head-cycle free nested logic programs

• Thomas Linke
• Hans Tompits
• Stefan Woltran

We define the class of head-cycle free nested logic programs, and its proper subclass of acyclic nested programs, generalising similar classes originally defined for disjunctive logic programs. We then extend several results known for acyclic and head-cycle free disjunctive programs under the stable model semantics to the nested case. Most notably, we provide a propositional semantics for the program classes under consideration. This generalises different extensions of Fages’ theorem, including a recent result by Erdem and Lifschitz for tight logic programs. We further show that, based on a shifting method, head-cycle free nested programs can be rewritten into normal programs in polynomial time and space, extending a similar technique for head-cycle free disjunctive programs. All this shows that head-cycle free nested programs constitute a subclass of nested programs possessing a lower computational complexity than arbitrary nested programs, providing the polynomial hierarchy does not collapse.

KR Conference 2004 Conference Paper

On Eliminating Disjunctions in Stable Logic Programming

• Thomas Eiter
• Michael Fink
• Hans Tompits
• Stefan Woltran

Disjunction is generally considered to add expressive power to logic programs under the stable model semantics, which have become a popular programming paradigm for knowledge representation and reasoning. However, disjunction is often not really needed, in that an equivalent program without disjunction can be given. In this paper, we consider the question, given a disjunctive logic program, P, under which conditions an equivalent normal (i. e., disjunction-free) logic program Q exists. In fact, we study this problem under different notions of equivalence, viz. for ordinary equivalence (considering the collections of all stable models of the programs) as well as for the more restrictive notions of strong and uniform equivalence. We resolve the issue for propositional programs on which we focus here, and present a simple, appealing semantic criterion from which all disjunctions can be eliminated under strong equivalence. Testing this criterion is coNP-complete, but the class of programs satisfying it has the same complexity as disjunctive logic programs in general. We also show that under ordinary and uniform equivalence, disjunctions can always be eliminated. In all cases, we give constructive methods to achieve this. However, we also provide evidence that disjunctive logic programs are a more succinct knowledge representation formalism than normal logic programs under all these notions of equivalence.

SAT Conference 2003 Conference Paper

Comparing Different Prenexing Strategies for Quantified Boolean Formulas

• Uwe Egly
• Martina Seidl
• Hans Tompits
• Stefan Woltran
• Michael Zolda

Abstract The majority of the currently available solvers for quantified Boolean formulas (QBFs) process input formulas only in prenex conjunctive normal form. However, the natural representation of practicably relevant problems in terms of QBFs usually results in formulas which are not in a specific normal form. Hence, in order to evaluate such QBFs with available solvers, suitable normal-form translations are required. In this paper, we report experimental results comparing different prenexing strategies on a class of structured benchmark problems. The problems under consideration encode the evaluation of nested counterfactuals over a propositional knowledge base, and span the entire polynomial hierarchy. The results show that different prenexing strategies influence the evaluation time in different ways across different solvers. In particular, some solvers are robust to the chosen strategies while others are not.

KR Conference 2002 Conference Paper

A Generic Approach for Knowledge-Based Information-Site Selection

• Thomas Eiter
• Michael Fink
• Giuliana Sabbatini
• Hans Tompits

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

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.

LPAR Conference 2001 Conference Paper

Reasoning about Evolving Nonmonotonic Knowledge Bases

• Thomas Eiter
• Michael Fink 0001
• Giuliana Sabbatini
• Hans Tompits

Abstract Recently, several approaches to updating knowledge bases modeled as extended logic programs (ELPs) have been introduced, ranging from basic methods to incorporate (sequences of) sets of rules into a logic program, to more elaborate methods which use an update policy for specifying how updates must be incorporated. In this paper, we introduce a framework for reasoning about evolving knowledge bases, which are represented as ELPs and maintained by an update policy. We describe a formal model which captures various update approaches, and define a logical language for expressing properties of evolving knowledge bases. We further investigate the semantical properties of knowledge states with respect to reasoning. In particular, we describe finitary characterizations of the evolution, and derive complexity results for our 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.

JELIA Conference 2000 Invited Paper

Considerations on Updates of Logic Programs

• Thomas Eiter
• Michael Fink 0001
• Giuliana Sabbatini
• Hans Tompits

Abstract Among others, Alferes et al. (1998) presented an approach for updating logic programs with sets of rules based on dynamic logic programs. We syntactically redefine dynamic logic programs and investigate their semantical properties, looking at them from perspectives such as a belief revision and abstract consequence relation view. Since the approach does not respect minimality of change, we refine its stable model semantics and present minimal stable models and strict stable models. We also compare the update approach to related work, and find that is equivalent to a class of inheritance programs independently defined by Buccafurri et al. (1999).

ECAI Conference 2000 Conference Paper

Logic Programs with Compiled Preferences

• James P. Delgrande
• Torsten Schaub
• Hans Tompits

AAAI Conference 2000 Conference Paper

Solving Advanced Reasoning Tasks Using Quantified Boolean Formulas

• Uwe Egly
• Hans Tompits

We consider the compilation of different reasoning tasks into the evaluation problem of quantified boolean formulas (QBFs) as an approach to develop prototype reasoning systems useful for, e. g. , experimental purposes. Such a method is a natural generalization of a similar technique applied to NP-problems and has been recently proposed by other researchers. More specifically, we present translations of several well-known reasoning tasks from the area of nonmonotonic reasoning into QBFs, and compare their implementation in the prototype system QUIP with established NMRprovers. The results show reasonable performance, and document that the QBF approach is an attractive tool for rapid prototyping of experimental knowledge-representation systems.