Abstract Answer Set Programming with Quantifiers (ASP(Q)) has been introduced to provide a natural extension of ASP modeling to problems in the polynomial hierarchy (PH). However, ASP(Q) lacks a method for encoding in an elegant and compact way problems requiring a polynomial number of calls to an oracle in $\Sigma _n^p$ (that is, problems in $\Delta _{n+1}^p$ ). Such problems include, in particular, optimization problems. In this paper, we propose an extension of ASP(Q), in which component programs may contain weak constraints. Weak constraints can be used both for expressing local optimization within quantified component programs and for modeling global optimization criteria. We showcase the modeling capabilities of the new formalism through various application scenarios. Further, we study its computational properties obtaining complexity results and unveiling non-obvious characteristics of ASP(Q) programs with weak constraints.

status: Published

The first issue of the journal Theory and Practice of Logic Programming, or TPLP, was published in January 2001.This issue, the last one in the present volume, and the following issue, the first one in the next volume, comprise a collection of papers commemorating and celebrating the twentieth anniversary of the journal.This celebratory collection comes with about one year delay due to the COVID-19 pandemic (but also, if we were to be entirely honest, because of a common human tendency to put things off).Whatever the true reason for the delay, the collection is finally here.We hope and expect it will prove to be a demonstration of the vitality of logic programming, and of a broad range of research directions it spawned in the past and continues to generate today.Logic programming appeared as a scientific subarea of computer science in the early 1970s as a result of the happy confluence of research on automated theorem proving in first-order logic and the original implementation of the Prolog programming language.The presence of these two original sources of inspiration has been distinctly felt over the years.On the one hand, logic programming attracted theoreticians pursuing deeper and highly nuanced understanding of the semantics of logic programs; on the other hand, it drew in researchers whose goal was to advance the repertoire of logic programming tools by refining, perfecting, and expanding Prolog, proposing and implementing new computational paradigms for logic programming, and developing methods to build and analyze logic programs.Moreover, and it also goes back to its very origins, logic programming attracted researchers interested in applications such as natural language processing, database querying, constraint solving, planning, learning, and knowledge representation, to name but a few.

The problem of fair division of indivisible goods is a fundamental problem of resource allocation in multi-agent systems, also studied extensively in social choice. Recently, the problem was generalized to the case when goods form a graph and the goal is to allocate goods to agents so that each agent’s bundle forms a connected subgraph. For the maximin share fairness criterion, researchers proved that if goods form a tree, an allocation offering each agent a bundle of at least her maximin share value always exists. Moreover, it can be found in polynomial time. In this paper we consider the problem of maximin share allocations of goods on a cycle. Despite the simplicity of the graph, the problem turns out to be significantly harder than its tree version. We present cases when maximin share allocations of goods on cycles exist and provide in this case results on allocations guaranteeing each agent a certain fraction of her maximin share. We also study algorithms for computing maximin share allocations of goods on cycles.

Lifting a preference order on elements of some universe to a preference order on subsets of this universe is often guided by postulated properties the lifted order should have. Well-known impossibility results pose severe limits on when such liftings exist if all non-empty subsets of the universe are to be ordered. The extent to which these negative results carry over to other families of sets is not known. In this paper, we consider families of sets that induce connected subgraphs in graphs. For such families, common in applications, we study whether lifted orders satisfying the well-studied axioms of dominance and (strict) independence exist for every or, in another setting, for some underlying order on elements (strong and weak orderability). We characterize families that are strongly and weakly orderable under dominance and strict independence, and obtain a tight bound on the class of families that are strongly orderable under dominance and independence.

Abstract Answer Set Programming (ASP) is a logic programming paradigm featuring a purely declarative language with comparatively high modeling capabilities. Indeed, ASP can model problems in NP in a compact and elegant way. However, modeling problems beyond NP with ASP is known to be complicated, on the one hand, and limited to problems in $\[\Sigma _2^P\]$ on the other. Inspired by the way Quantified Boolean Formulas extend SAT formulas to model problems beyond NP, we propose an extension of ASP that introduces quantifiers over stable models of programs. We name the new language ASP with Quantifiers (ASP(Q)). In the paper we identify computational properties of ASP(Q); we highlight its modeling capabilities by reporting natural encodings of several complex problems with applications in artificial intelligence and number theory; and we compare ASP(Q) with related languages. Arguably, ASP(Q) allows one to model problems in the Polynomial Hierarchy in a direct way, providing an elegant expansion of ASP beyond the class NP.

The problem of fair division of indivisible goods is a fundamental problem of social choice. Recently, the problem was extended to the setting when goods form a graph and the goal is to allocate goods to agents so that each agent's bundle forms a connected subgraph. Researchers proved that, unlike in the original problem (which corresponds to the case of the complete graph in the extended setting), in the case of the goods-graph being a tree, allocations offering each agent a bundle of or exceeding her maximin share value always exist. Moreover, they can be found in polynomial time. We consider here the problem of maximin share allocations of goods on a cycle. Despite the simplicity of the graph, the problem turns out be significantly harder than its tree version. We present cases when maximin share allocations of goods on cycles exist and provide results on allocations guaranteeing each agent a certain portion of her maximin share. We also study algorithms for computing maximin share allocations of goods on cycles.

Lifting a preference order on elements of some universe to a preference order on subsets of this universe is often guided by postulated properties the lifted order should have. Well-known impossibility results pose severe limits on when such liftings exist if all non-empty subsets of the universe are to be ordered. The extent to which these negative results carry over to other families of sets is not known. In this paper, we consider families of sets that induce connected subgraphs in graphs. For such families, common in applications, we study whether lifted orders satisfying the well-studied axioms of dominance and (strict) independence exist for every or, in another setting, only for some underlying order on elements (strong and weak orderability). We characterize families that are strongly and weakly orderable under dominance and strict independence, and obtain a tight bound on the class of families that are strongly orderable under dominance and independence.

We propose a model of random quantified boolean formulas and their natural random disjunctive logic program counterparts. The model extends the standard models for random SAT and 2QBF. We provide theoretical bounds for the phase transition region in the new model, and show experimentally the presence of the easy-hard-easy pattern. Importantly, we show that the model is well suited for assessing solvers tuned to real-world instances. Moreover, to the best of our knowledge, our model and results on random disjunctive logic programs are the first of their kind.

Integrating diverse formalisms into modular knowledge representation systems offers increased expressivity, modeling convenience, and computational benefits. We introduce the concepts of abstract inference modules and abstract modular inference systems to study general principles behind the design and analysis of model generating programs, or solvers , for integrated multi-logic systems. We show how modules and modular systems give rise to transition graphs , which are a natural and convenient representation of solvers, an idea pioneered by the SAT community. These graphs lend themselves well to extensions that capture such important solver design features as learning. In the paper, we consider two flavors of learning for modular formalisms, local and global. We illustrate our approach by showing how it applies to answer set programming, propositional logic, multi-logic systems based on these two formalisms and, more generally, to satisfiability modulo theories.

Modularity is an essential aspect of knowledge representation theory and practice. It has received substantial attention. We introduce model-based modular systems, an abstract framework for modular knowledge representation formalisms, similar in scope to multi-context systems but employing a simpler information-flow mechanism. We establish the precise relationship between the two frameworks, showing that they can simulate each other. We demonstrate that recently introduced modular knowledge representation formalisms integrating logic programming with satisfiability and, more generally, with constraint satisfaction can be cast as modular systems in our sense. These results show that our formalism offers a simple unifying framework for studies of modularity in knowledge representation.

We introduce partial lexicographic preference trees (PLPtrees) as a formalism for compact representations of preferences over combinatorial domains. Our main results concern the problem of passive learning of PLP-trees. Specifically, forseveral classes of PLP-trees, we study how to learn (i) a PLP-tree consistent with a dataset of examples, possibly subject to requirements on the size of the tree, and (ii) a PLP-tree correctly ordering as many of the examples as possible in case the dataset of examples is inconsistent. We establish complexity of these problems and, in all cases where the problem is in the class P, propose polynomial time algorithms.

Abstract Disjunctive Answer Set Programming is a powerful declarative programming paradigm with complexity beyond NP. Identifying classes of programs for which the consistency problem is in NP is of interest from the theoretical standpoint and can potentially lead to improvements in the design of answer set programming solvers. One of such classes consists of dual-normal programs, where the number of positive body atoms in proper rules is at most one. Unlike other classes of programs, dual-normal programs have received little attention so far. In this paper we study this class. We relate dual-normal programs to propositional theories and to normal programs by presenting several inter-translations. With the translation from dual-normal to normal programs at hand, we introduce the novel class of body-cycle free programs, which are in many respects dual to head-cycle free programs. We establish the expressive power of dual-normal programs in terms of SE- and UE-models, and compare them to normal programs. We also discuss the complexity of deciding whether dual-normal programs are strongly and uniformly equivalent.

Abstract Propositional formulas that are equivalent in intuitionistic logic, or in its extension known as the logic of here-and-there, have the same stable models. We extend this theorem to propositional formulas with infinitely long conjunctions and disjunctions and show how to apply this generalization to proving properties of aggregates in answer set programming.

Abstract We study the framework of abductive logic programming extended with integrity constraints. For this framework, we introduce a new measure of the simplicity of an explanation based on its degree of arbitrariness: the more arbitrary the explanation, the less appealing it is, with explanations having no arbitrariness — they are called constrained — being the preferred ones. In the paper, we study basic properties of constrained explanations. For the case when programs in abductive theories are stratified we establish results providing a detailed picture of the complexity of the problem to decide whether constrained explanations exist.

We introduce abstract preference frameworks to study general properties common across a variety of preference formalisms. In particular, we study strong equivalence in preference formalisms and their separability. We identify abstract postulates on preference frameworks, satisfied by most of the currently studied preference formalisms, that lead to characterizations of both properties of interest.

We introduce the framework of qualitative optimization problems (or, simply, optimization problems) to represent preference theories. The formalism uses separate modules to describe the space of outcomes to be compared (the generator) and the preferences on outcomes (the selector). We consider two types of optimization problems. They differ in the way the generator, which we model by a propositional theory, is interpreted: by the standard propositional logic semantics, and by the equilibrium-model (answer-set) semantics. Under the latter interpretation of generators, optimization problems directly generalize answer-set optimization programs proposed previously. We study strong equivalence of optimization problems, which guarantees their interchangeability within any larger context. We characterize several versions of strong equivalence obtained by restricting the class of optimization problems that can be used as extensions and establish the complexity of associated reasoning tasks. Understanding strong equivalence is essential for modular representation of optimization problems and rewriting techniques to simplify them without changing their inherent properties.

Abstract We study active integrity constraints and revision programming, two formalisms designed to describe integrity constraints on databases and to specify policies on preferred ways to enforce them. Unlike other more commonly accepted approaches, these two formalisms attempt to provide a declarative solution to the problem. However, the original semantics of founded repairs for active integrity constraints and justified revisions for revision programs differ. Our main goal is to establish a comprehensive framework of semantics for active integrity constraints, to find a parallel framework for revision programs, and to relate the two. By doing so, we demonstrate that the two formalisms proposed independently of each other and based on different intuitions when viewed within a broader semantic framework turn out to be notational variants of each other. That lends support to the adequacy of the semantics we develop for each of the formalisms as the foundation for a declarative approach to the problem of database update and repair. In the paper, we also study computational properties of the semantics we consider and establish results concerned with the concept of the minimality of change and the invariance under the shifting transformation.

Abstract A fundamental task for propositional logic is to compute models of propositional formulas. Programs developed for this task are called satisfiability solvers. We show that transition systems introduced by Nieuwenhuis, Oliveras, and Tinelli to model and analyze satisfiability solvers can be adapted for solvers developed for two other propositional formalisms: logic programming under the answer-set semantics, and the logic PC(ID). We show that in each case the task of computing models can be seen as “satisfiability modulo answer-set programming,” where the goal is to find a model of a theory that also is an answer set of a certain program. The unifying perspective we develop shows, in particular, that solvers clasp and minisat(id) are closely related despite being developed for different formalisms, one for answer-set programming and the latter for the logic PC(ID).

Abstract We present trichotomy results characterizing the complexity of reasoning with disjunctive logic programs. To this end, we introduce a certain definition schema for classes of programs based on a set of allowed arities of rules. We show that each such class of programs has a finite representation, and for each of the classes definable in the schema, we characterize the complexity of the existence of an answer set problem. Next, we derive similar characterizations of the complexity of skeptical and credulous reasoning with disjunctive logic programs. Such results are of potential interest. On the one hand, they reveal some reasons responsible for the hardness of computing answer sets. On the other hand, they identify classes of problem instances, for which the problem is “easy” (in P) or “easier than in general” (in NP). We obtain similar results for the complexity of reasoning with disjunctive programs under the supported-model semantics.

We study methods to specify preferences among subsets of a set (auniverse). The methods we focus on are of two types. The first one assumes the universe comes with a preference relation on its elements and attempts to lift that relation to subsets of the universe. That approach has limited expressivity but results in orderings that capture interesting general preference principles. The second method consists of developing formalisms allowing the user to specify "atomic" improvements, and generating from them preferences on the powerset of the universe. We show that the particular formalism we propose is expressive enough to capture the lifted preference relations of the first approach, and generalizes propositional CP-nets. We discuss the importance of domain-independent methods for specifying preferences on sets for knowledge representation formalisms, selecting the formalism of argumentation frameworks as an illustrative example.

Abstract A recent framework of relativized hyperequivalence of programs offers a unifying generalization of strong and uniform equivalence. It seems to be especially well suited for applications in program optimization and modular programming due to its flexibility that allows us to restrict, independently of each other, the head and body alphabets in context programs. We study relativized hyperequivalence for the three semantics of logic programs given by stable, supported, and supported minimal models. For each semantics, we identify four types of contexts, depending on whether the head and body alphabets are given directly or as thecomplementof a given set. Hyperequivalence relative to contexts where the head and body alphabets are specified directly has been studied before. In this paper, we establish the complexity of deciding relativized hyperequivalence with respect to the three other types of context programs.

We investigate the computational complexity of testing dominance and consistency in CP-nets. Previously, the complexity of dominance has been determined for restricted classes in which the dependency graph of the CP-net is acyclic. However, there are preferences of interest that define cyclic dependency graphs; these are modeled with general CP-nets. In our main results, we show here that both dominance and consistency for general CP-nets are PSPACE-complete. We then consider the concept of strong dominance, dominance equivalence and dominance incomparability, and several notions of optimality, and identify the complexity of the corresponding decision problems. The reductions used in the proofs are from STRIPS planning, and thus reinforce the earlier established connections between both areas.

Abstract We introduce and study logic programs whose clauses are built out ofmonotone constraint atoms. We show that the operational concept of the one-step provability operator generalizes to programs with monotone constraint atoms, but the generalization involves nondeterminism. Our main results demonstrate that our formalism is a common generalization of (1) normal logic programming with its semantics of models, supported models and stable models, (2) logic programming with weight atomslparseprograms) with the semantics of stable models, as defined by Niemelä, Simons and Soininen, and (3) of disjunctive logic programming with the possible-model semantics of Sakama and Inoue.

We study properties of programs with monotone and convex constraints. We extend to these formalisms concepts and results from normal logic programming. They include the notions of strong and uniform equivalence with their characterizations, tight programs and Fages Lemma, program completion and loop formulas. Our results provide an abstract account of properties of some recent extensions of logic programming with aggregates, especially the formalism of lparse programs. They imply a method to compute stable models of lparse programs by means of off-the-shelf solvers of pseudo-boolean constraints, which is often much faster than the smodels system.

The answer-set programming (ASP) paradigm is a way of using logic to solve search problems. Given a search problem, to solve it one designs a logic theory so that models of this theory represent problem solutions. To compute a solution to the problem, one computes a model of the theory. Several answer-set programming formalisms have been developed on the basis of logic programming with the semantics of answer sets. In this article we show that predicate logic also gives rise to effective implementations of the ASP paradigm, similar in spirit to logic programming with the answer-set semantics and with a similar scope of applicability. Specifically, we propose two logics based on predicate calculus as formalisms for encoding search problems. We show that the expressive power of these logics is given by the class NPMV. We demonstrate their use in programming and discuss computational approaches to model finding. To address this latter issue, we follow a two-pronged approach. On the one hand, we show that the problem can be reduced to that of computing models of propositional theories and, more generally, of collections of pseudo-Boolean constraints. Consequently, programs (solvers) developed in the areas of propositional and pseudo-Boolean satisfiability can be used to compute models of theories in our logics. On the other hand, we develop native solvers designed specifically to exploit features of our formalisms. We present experimental results demonstrating the computational effectiveness of the overall approach.

We propose and study algorithms to compute minimal models, stable models and answer sets of $t$ -CNF theories, and normal and disjunctive $t$ -programs. We are especially interested in algorithms with non-trivial worst-case performance bounds. The bulk of the paper is concerned with the classes of 2- and 3-CNF theories, and normal and disjunctive 2- and 3-programs, for which we obtain significantly stronger results than those implied by our general considerations. We show that one can find all minimal models of 2-CNF theories and all answer sets of disjunctive 2-programs in time $O(m1\mbox{.}4422\mbox{..}^n)$ . Our main results concern computing stable models of normal 3-programs, minimal models of 3-CNF theories and answer sets of disjunctive 3-programs. We design algorithms that run in time $O(m1\mbox{.}6701\mbox{..}^n)$ , in the case of the first problem, and in time $O(mn^2 2\mbox{.}2782\mbox{..}^n)$ , in the case of the latter two. All these bounds improve by exponential factors the best algorithms known previously. We also obtain closely related upper bounds on the number of minimal models, stable models and answer sets a $t$ -CNF theory, a normal $t$ -program or a disjunctive $t$ -program may have.

Abstract Logic programming requires that the programmer convert a problem into a set of constraints based on predicates. Choosing the predicates and introducing appropriate constraints can be intricate and error prone. If the problem domain is structured enough, we can let the programmer express the problem in terms of more abstract, higher‐level constraints. A compiler can then convert the higher‐level program into a logic‐programming formalism. The compiler writer can experiment with alternative low‐level representations of the higher‐level constraints in order to achieve a high‐quality translation. The programmer can then take advantage of both a reduction in complexity and an improvement in runtime speed for all problems within the domain. We apply this analysis to the domain of tabular constraint‐satisfaction problems. Examples of such problems include logic puzzles solvable on a hatch grid and combinatorial problems such as graph coloring and independent sets. The proper abstractions for these problems are rows, columns, entries, and their interactions. We present a higher‐level language, Constraint Lingo, dedicated to problems in this domain. We also describe how we translate programs from Constraint Lingo into lower‐level logic formalisms such as the logic of propositional schemata. These translations require that we choose among competing lower‐level representations in order to produce efficient results. The overall effectiveness of our approach depends on the appropriateness of Constraint Lingo, our ability to translate Constraint Lingo programs into high‐quality representations in logic formalisms, and the efficiency with which logic engines can compute answer sets. We comment on our computational experience with these tools in solving both graph problems and logic puzzles. Copyright © 2004 John Wiley & Sons, Ltd.

We study algorithms for computing stable models of logic programs and derive estimates on their worst-case performance that are asymptotically better than the trivial bound of $O(m 2^n)$ , where $m$ is the size of an input program and $n$ is the number of its atoms. For instance, for programs whose clauses consist of at most two literals (counting the head) we design an algorithm to compute stable models that works in time $O(m\times 1.44225^n)$ . We present similar results for several broader classes of programs. Finally, we study the applicability of the techniques developed in the paper to the analysis of the performance of smodels.

A decision problem is called parameterized if its input is a pair of strings. One of these strings is referred to as a parameter . The following problem is an example of a parameterized decision problem with k serving as a parameter: given a propositional logic program P and a nonnegative integer k , decide whether P has a stable model of size no more than k . Parameterized problems that are NP-complete often become solvable in polynomial time if the parameter is fixed. The problem to decide whether a program P has a stable model of size no more than k , where k is fixed and not a part of input, can be solved in time O ( mn k ), where m is the size of P and n is the number of atoms in P . Thus, this problem is in the class P. However, algorithms with the running time given by a polynomial of order k are not satisfactory even for relatively small values of k .The key question then is whether significantly better algorithms (with the degree of the polynomial not dependent on k ) exist. To tackle it, we use the framework of fixed-parameter complexity. We establish the fixed-parameter complexity for several parameterized decision problems involving models, supported models, and stable models of logic programs. We also establish the fixed-parameter complexity for variants of these problems resulting from restricting attention to definite Horn programs and to purely negative programs. Most of the problems considered in the paper have high fixed-parameter complexity. Thus, it is unlikely that fixing bounds on models (supported models, stable models) will lead to fast algorithms to decide the existence of such models.

In this paper, we focus on the problem of existence and computing of small and large stable models. We show that for every fixed integer k, there is a linear-time algorithm to decide the problem LSM (large stable models problem): does a logic program P have a stable model of size at least [mid ]P[mid ]−k? In contrast, we show that the problem SSM (small stable models problem) to decide whether a logic program P has a stable model of size at most k is much harder. We present two algorithms for this problem but their running time is given by polynomials of order depending on k. We show that the problem SSM is fixed-parameter intractable by demonstrating that it is W[2]-hard. This result implies that it is unlikely an algorithm exists to compute stable models of size at most k that would run in time O(mc), where m is the size of the program and c is a constant independent of k. We also provide an upper bound on the fixed-parameter complexity of the problem SSM by showing that it belongs to the class W[3].

In this paper constructions leading to the formation of belief sets by agents are studied. The focus is on the situation when possible belief sets are built incrementally in stages. An infinite sequence of theories that represents such a process is called a reasoning trace. A set of reasoning traces describing all possible reasoning scenarios for the agent is called a reasoning frame. Default logic by Reiter is not powerful enough to represent reasoning frames. In the paper a generalization of default logic of Reiter is introduced by allowing infinite sets of justifications. This formalism is called infinitary default logic. In the main result of the paper it is shown that every reasoning frame can be represented by an infinitary default theory. A similar representability result for antichains of theories (belief frames) is also presented.

The well-founded semantics is one of the most widely studied and used semantics of logic programs with negation. In the case of finite propositional programs, it can be computed in polynomial time, more specifically, in O([mid ]At(P)[mid ] × size(P)) steps, where size(P) denotes the total number of occurrences of atoms in a logic program P. This bound is achieved by an algorithm introduced by Van Gelder and known as the alternating-fixpoint algorithm. Improving on the alternating-fixpoint algorithm turned out to be difficult. In this paper we study extensions and modifications of the alternating-fixpoint approach. We then restrict our attention to the class of programs whose rules have no more than one positive occurrence of an atom in their bodies. For programs in that class we propose a new implementation of the alternating-fixpoint method in which false atoms are computed in a top-down fashion. We show that our algorithm is faster than other known algorithms and that for a wide class of programs it is linear and so, asymptotically optimal.

We study properties of rough sets, that is, approximations to sets of records in a database or, more formally, to subsets of the universe of an information system. A rough set is a pair 〈L, U〉 such that L, U are definable in the information system and L ⊆ U. In the paper, we introduce a language, called the language of inclusion-exclusion, to describe incomplete specifications of (unknown) sets. We use rough sets in order to define a semantics for theories in the inclusion-exclusion language. We argue that our concept of a rough set is closely related to that introduced by Pawlak. We show that rough sets can be ordered by the knowledge ordering (denoted $\preceq$ kn )- We prove that Pawlak's rough sets are characterized as $\preceq$ kn -greatest approximations. We show that for any consistent (that is, satisfiable) theory T in the language of inclusion-exclusion there exists a $\preceq$ kn -greatest rough set approximating all sets X that satisfy T. For some classes of theories in the language of inclusion-exclusion, we provide algorithmic ways to find this best approximation. We also state a number of miscellaneous results and discuss some open problems.

In this paper we investigate the complexity of problems concerned with approximating the stable model semantics. We show that under rather weak assumptions it is NP-hard to decide whether the size of a polynomially computable approximation is within

We establish the complexity of decision problems associated with the nonmonotonic modal logic S4. We prove that the problem of existence of an S4-expansion for a given set A of premisses is ΣP2-complete. Similarly, we show that for a given formula Φ and a set A of premisses, it is ΣP2-complete to decide whether Φ belongs to at least one S4-expansion for A, and it is πP2-complete to decide whether Φ belongs to all S4-expansions for A. This refutes a conjecture of Gottlob that these problems are PSPACE-complete. An interesting aspect of these results is that reasoning (testing satisfiability and provability) in the monotonic modal logic S4 is PSPACE-complete. To the best of our knowledge, the nonmonotonic logic S4 is the first example of a nonmonotonic formalism which is computationally easier than the monotonic logic that underlies it (assuming PSPACE does not collapse to ΣP2).

Many nonmonotonic formalism, including default logic, logic programming with stable models, and autoepistemic logic, can be represented faithfully by means of modal nonmonotonic logics in the family proposed by McDermott and Doyle. In this paper properties of logics in this family are thoroughly investigated. We present several results on characterization of expansions. These results are applicable to a wide class of nonmonotonic modal logics. Using these characterization results, algorithms for computing expansions for finite theories are developed. Perhaps the most important finding of this paper is that the structure of the family of modal nonmonotonic logics is much simpler than that of the family of underlying modal (monotonic) logics. Namely, it is often the case that different monotonic modal logics collapse to the same nonmonotonic system. We exhibit four families of logics whose nonmonotonic variants coincide: 5-KD45, TW5-SW5, N-WK , and W5-D4WB . These nonmonotonic logics naturally represent logics related to commonsense reasoning and knowledge representation such as autoepistemic logic, reflexive autoepistemic logic, default logic, and truth maintenance with negation.

The authors present part of a complete solution of a two-terminal net routing problem for certain non-convex grids without holes that they call channel graphs. They present an algorithm for embedding a non-even channel graph routing problem in an even channel graph routing problem. They refer to the algorithm as EMBED. EMBED runs in time O(b), where b is the number of vertices on the boundary, and is similar to an algorithm described by M. Becker and K. Mehlhorn (1986) for planar graphs. Due to the restrictions the authors place on the shape of channel graph routing problems they are able to obtain a lower complexity for their algorithm than that of the Becker and Mehlhorn algorithm. Their algorithm has complexity O(bn), where n is the number of vertices in the graph.>

In this paper we discuss the pure logic of necessitation N, a modal logic containing classical propositional calculus, with modus ponens and necessitation as inference rules, but without any axioms for manipulating modalities. We develop a theory of the logic N. We propose a sound and complete Kripke-like semantics for N and build a tableaux system for testing whether a formula is provable from a theory in the logic N. An alternative method to compute modal-free consequences of a finite theory is also given. Our main motivation to consider the logic N comes from the area of nonmonotonic reasoning. The nonmonotonic variant of N seems to be particularly useful in investigations of knowledge sets built when only partial information is available. In particular, this logic N is deeply connected with the default logic. In this paper, we apply our results to problems in nonmonotonic reasoning and we design algorithms for building the nonmonotonic consequence operator associated with N.

This paper is part of a complete solution of the two-terminal net routing problem for certain non-convex grids without holes that the authors call Z-grids, that part being the embedding of a non-even Z-grid routing problem in an even Z-grid routing problem. This embedding algorithm runs in time O(b), where b is the size of the boundary.>

Autoepistemic logic is one of the principal modes of nonmonotonic reasoning. It unifies several other modes of nonmonotonic reasoning and has important application in logic programming. In the paper, a theory of autoepistemic logic is developed. This paper starts with a brief survey of some of the previously known results. Then, the nature of nonmonotonicity is studied by investigating how membership of autoepistemic statements in autoepistemic theories depends on the underlying objective theory. A notion similar to set-theoretic forcing is introduced. Expansions of autoepistemic theories are also investigated. Expansions serve as sets of consequences of an autoepistemic theory and they can also be used to define semantics for logic programs with negation. Theories that have expansions are characterized, and a normal form that allows the description of all expansions of a theory is introduced. Our results imply algorithms to determine whether a theory has a unique expansion. Sufficient conditions (stratification) that imply existence of a unique expansion are discussed. The definition of stratified theories is extended and (under some additional assumptions) efficient algorithms for testing whether a theory is stratified are proposed. The theorem characterizing expansions is applied to two classes of theories, K 1 -theories and ae-programs. In each case, simple hypergraph characterization of expansions of theories from each of these classes is given. Finally, connections with stable model semantics for logic programs with negation is discussed. In particular, it is proven that the problem of existence of stable models is NP-complete.— Authors' Abstract