We consider a deterministic rewrite system for combinatory logic over combinators , and . Terms will be represented by graphs so that reduction of a duplicator will cause the duplicated expression to be "shared" rather than copied. To each normalizing term we assign a weighting which is the number of reduction steps necessary to reduce the expression to normal form. A lambda-expression may be represented by several distinct expressions in combinatory logic, and two combinatory logic expressions are considered equivalent if (...) they represent the same lambda-expression (up to --equivalence). The problem of minimizing the number of reduction steps over equivalent combinator expressions (i.e., the problem of finding the "fastest running" combinator representation for a specific lambda-expression) is proved to be NP-complete by reduction from the "Hitting Set" problem. (shrink)

In this paper the questions remaining open about NP-completeness of multiplicative and Horn fragments of the Linear Logic and the Linear Logic with the weakening rule are answered.

I investigate the problem of contracting a dependency-network with respect to any of its nodes. The resulting contraction must not contain the node in question, but must also be a minimal mutilation of the original network. Identifying successful and minimally mutilating contractions of dependency-networks is non-trivial, especially when non-well-founded networks are to be taken into account. I prove that the contraction problem is NP-complete.1.

System image is an extension of multiplicative linear logic with the rules mix, nullary mix, and a self-dual, noncommutative logical operator, called seq. While the rules mix and nullary mix extend the deductive system, the operator seq extends the language of image. Due to the operator seq, system image extends the applications of image to those where the sequential composition is crucial, e.g., concurrency theory. System image is an extension of image with the rules mix and nullary mix. In this (...) paper, by relying on the fact that system image is a conservative extension of system image, I show that system image is NP-complete by encoding the 3-Partition problem in image. I provide a simple completeness proof of this encoding by resorting to a novel proof theoretical method for reducing nondeterminism in proof search, which is also of independent interest. (shrink)

Maps and territory suggest problems which have to do with the opening of pathways in some poorly explored domain.

An NP-hardness proof for non-local Multicomponent Tree Adjoining Grammar (MCTAG) by Rambow and Satta (1st International Workshop on Tree Adjoining Grammers 1992 ), based on Dahlhaus and Warmuth (in J Comput Syst Sci 33:456–472, 1986 ), is extended to some linguistically relevant restrictions of that formalism. It is found that there are NP-hard grammars among non-local MCTAGs even if any or all of the following restrictions are imposed: (i) lexicalization: every tree in the grammar contains a terminal; (ii) dominance links: (...) every tree set contains at most two trees, and in every such tree set, there is a link between the foot node of one tree and the root node of the other tree, indicating that the former node must dominate the latter in the derived tree. This is the version of MCTAG proposed in Becker et al. (Proceedings of the 5th conference of the European chapter of the Association for Computational Linguistics 1991 ) to account for German long-distance scrambling. This result restricts the field of possible candidates for an extension of Tree Adjoining Grammar that would be both mildly context-sensitive and linguistically adequate. (shrink)

A new proof is presented of Tsotsos' result that the VISUAL MATCH problem is NP-complete when no (high-level) constraints are imposed on the search space. Like the proof given by Tsotsos, it is based on the polynomial reduction of the NP-complete problem KNAPSACK to VISUAL MATCH. Tsotsos' proof, however, involves limited-precision real numbers, which introduces an extra degree of complexity to his treatment. The reduction of KNAPSACK to VISUAL MATCH presented here makes no use of limited-precision numbers, leading (...) to a simpler and more direct proof of the result. (shrink)

Kevin T. Kelly. Version Spaces, Structural Descriptions and NP-Completeness.

A pool resolution proof is a dag-like resolution proof which admits a depth-first traversal tree in which no variable is used as a resolution variable twice on any branch. The problem of determining whether a given dag-like resolution proof is a valid pool resolution proof is shown to be NP-complete.

We investigate why similar extensions of first-order logic using operators corresponding to NP-complete decision problems apparently differ in expressibility: the logics capture either NP or LNP. It had been conjectured that the complexity class captured is NP if and only if the operator is monotone. We show that this conjecture is false. However, we provide evidence supporting a revised conjecture involving finite variations of monotone problems.

We show that arbitrary tautologies of Johansson’s minimal propositional logic are provable by “small” polynomial-size dag-like natural deductions in Prawitz’s system for minimal propositional logic. These “small” deductions arise from standard “large” tree-like inputs by horizontal dag-like compression that is obtained by merging distinct nodes labeled with identical formulas occurring in horizontal sections of deductions involved. The underlying geometric idea: if the height, h(∂), and the total number of distinct formulas, ϕ(∂), of a given tree-like deduction ∂ of a minimal (...) tautology ρ are both polynomial in the length of ρ, |ρ|, then the size of the horizontal dag-like compression ∂ᶜ is at most h(∂)×ϕ(∂), and hence polynomial in |ρ|. That minimal tautologies ρ are provable by tree-like natural deductions ∂ with |ρ|-polynomial h(∂) and ϕ(∂) follows via embedding from Hudelmaier’s result that there are analogous sequent calculus deductions of sequent ⇒ρ. The notion of dag-like provability involved is more sophisticated than Prawitz’s tree-like one and its complexity is not clear yet. Our approach nevertheless provides a convergent sequence of NP lower approximations of PSPACE-complete validity of minimal logic. (shrink)

In this paper we investigate the problem of testing the coherence of an assessment of conditional probability following a purely logical setting. In particular we will prove that the coherence of an assessment of conditional probability χ can be characterized by means of the logical consistency of a suitable theory T χ defined on the modal-fuzzy logic FP k (RŁΔ) built up over the many-valued logic RŁΔ. Such modal-fuzzy logic was previously introduced in Flaminio (Lecture Notes in Computer Science, vol. (...) 3571, 2005) in order to treat conditional probability by means of a list of simple probabilities following the well known (smart) ideas exposed by Halpern (Proceedings of the eighth conference on theoretical aspects of rationality and knowledge, pp 17–30, 2001) and by Coletti and Scozzafava (Trends Logic 15, 2002). Roughly speaking, such logic is obtained by adding to the language of RŁΔ a list of k modalities for “probably” and axioms reflecting the properties of simple probability measures. Moreover we prove that the satisfiability problem for modal formulas of FP k (RŁΔ) is NP-complete. Finally, as main result of this paper, we prove FP k (RŁΔ) in order to prove that the problem of establishing the coherence of rational assessments of conditional probability is NP-complete. (shrink)

We upgrade [3] to a complete proof of the conjecture NP = PSPACE that is known as one of the fundamental open problems in the mathematical theory of computational complexity; this proof is based on [2]. Since minimal propositional logic is known to be PSPACE complete, while PSPACE to include NP, it suffices to show that every valid purely implicational formula ρ has a proof whose weight and time complexity of the provability involved are both polynomial in the (...) weight of ρ. As is [3], we use proof theoretic approach. Recall that in [3] we considered any valid ρ in question that had a “short” tree-like proof π in the Hudelmaier-style cutfree sequent calculus for minimal logic. The “shortness” means that the height of π and the total weight of different formulas occurring in it are both polynomial in the weight of ρ. However, the size, and hence also the weight, of π could be exponential in that of ρ. To overcome this trouble we embedded π into Prawitz’s proof system of natural deductions containing single formulas, instead of sequents. As in π, the height and the total weight of different formulas of the resulting tree-like natural deduction ∂1 were polynomial, although the size of ∂1 still could be exponential, in the weight of ρ. In our next, crucial move, ∂1 was deterministically compressed into a “small”, although multipremise, dag-like deduction ∂ whose horizontal levels contained only mutually different formulas, which made the whole weight polynomial in that of ρ. However, ∂ required a more complicated verification of the underlying provability of ρ. In this paper we present a nondeterministic compression of ∂ into a desired standard dag-like deduction ∂0 that deterministically proves ρ in time and space polynomial in the weight of ρ.2 Together with [3] this completes the proof of NP = PSPACE.Natural deductions are essential for our proof. Tree-to-dag horizontal compression of π merging equal sequents, instead of formulas, is not sufficient, since the total number of different sequents in π might be exponential in the weight of ρ – even assuming that all formulas occurring in sequents are subformulas of ρ. On the other hand, we need Hudelmaier’s cutfree sequent calculus in order to control both the height and total weight of different formulas of the initial tree-like proof π, since standard Prawitz’s normalization although providing natural deductions with the subformula property does not preserve polynomial heights. It is not clear yet if we can omit references to π even in the proof of the weaker result NP = coNP. (shrink)

Computational complexity is a discipline of computer science and mathematics which classifies computational problems depending on their inherent difficulty, i.e. categorizes algorithms according to their performance, and relates these classes to each other. P problems are a class of computational problems that can be solved in polynomial time using a deterministic Turing machine while solutions to NP problems can be verified in polynomial time, but we still do not know whether they can be solved in polynomial time as well. A (...) solution for the so-called NP-complete problems will also be a solution for any other such problems. Its artificial-intelligence analogue is the class of AI-complete problems, for which a complete mathematical formalization still does not exist. In this chapter we will focus on analysing computational classes to better understand possible formalizations of AI-complete problems, and to see whether a universal algorithm, such as a Turing test, could exist for all AI-complete problems. In order to better observe how modern computer science tries to deal with computational complexity issues, we present several different deep-learning strategies involving optimization methods to see that the inability to exactly solve a problem from a higher order computational class does not mean there is not a satisfactory solution using state-of-the-art machine-learning techniques. Such methods are compared to philosophical issues and psychological research regarding human abilities of solving analogous NP-complete problems, to fortify the claim that we do not need to have an exact and correct way of solving AI-complete problems to nevertheless possibly achieve the notion of strong AI. (shrink)

Motivated by constraint satisfaction problems, Feder and Vardi (SIAM Journal of Computing, 28, 57–104, 1998) set out to search for fragments of satisfying the dichotomy property: every problem definable in is either in P or else NP-complete. Feder and Vardi considered in this connection two logics, strict NP (or SNP) and monadic, monotone, strict NP without inequalities (or MMSNP). The former consists of formulas of the form , where is a quantifier-free formula in a relational vocabulary; and the latter (...) is the fragment of SNP whose formulas involve only negative occurrences of relation symbols, only monadic second-order quantifiers, and no occurrences of the equality symbol. It remains an open problem whether MMSNP enjoys the dichotomy property. In the present paper, SNP and MMSNP are characterized in terms of partially ordered connectives. More specifically, SNP is characterized using the logic D of partially ordered connectives introduced in Blass and Gurevich (Annals of Pure and Applied Logic, 32, 1–16, 1986), Sandu and Väänänen (Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 38, 361–372 1992), and MMSNP employing a generalization C of D introduced in the present paper. (shrink)

We show the completeness of a Hilbert-style system LK defined by M. Valiev involving the knowledge operator K dedicated to the reasoning with incomplete information. The completeness proof uses a variant of Makinson's canonical model construction. Furthermore we prove that the theoremhood problem for LK is co-NP-complete, using techniques similar to those used to prove that the satisfiability problem for propositional S5 is NP-complete.

The construction we are discussing is a recent American English construction with an individual-denoting noun phrase in the predicate position modified by a degree modifier that typically occurs with gradable adjectives, as in 'This is so Obama!' We attempt to look deeper into the structure and compositional semantics of this construction, and though we do not provide a complete analysis of it, we believe that the study of this construction can contribute to questions of gradable predicate semantics, multidimensionality, degree (...) constructions and proper name semantics. (shrink)

We start with a simple proof of Leivant's normal form theorem for ∑11 formulas over finite successor structures. Then we use that normal form to prove the following:1. over all finite structures, every ∑21 formula is equivalent to a ∑21 formula whose first-order part is a Boolean combination of existential formulas, and2. over finite successor structures, the Kolaitis-Thakur hierarchy of minimization problems collapses completely and the Kolaitis-Thakur hierarchy of maximization problems collapses partially.The normal form theorem for ∑21 fails if ∑21 (...) is replaced with ∑11 or if infinite structures are allowed. (shrink)

We propose a technical reformulation of the measurement problem of quantum mechanics, which is based on the postulate that the final state of a measurement is classical; this accords with experimental practice as well as with Bohr’s views. Unlike the usual formulation (in which the post-measurement state is a unit vector in Hilbert space), our version actually opens the possibility of admitting a purely technical solution within the confines of conventional quantum theory (as opposed to solutions that either modify this (...) theory, or introduce unusual and controversial interpretative rules and/or ontologies). To that effect, we recall a remarkable phenomenon in the theory of Schrödinger operators (discovered in 1981 by Jona-Lasinio, Martinelli, and Scoppola), according to which the ground state of a symmetric double-well Hamiltonian (which is paradigmatically of Schrödinger’s Cat type) becomes exponentially sensitive to tiny perturbations of the potential as ħ→0. We show that this instability emerges also from the textbook wkb approximation, extend it to time-dependent perturbations, and study the dynamical transition from the ground state of the double well to the perturbed ground state (in which the cat is typically either dead or alive, depending on the details of the perturbation). Numerical simulations show that adiabatically arising perturbations may (quite literally) cause the collapse of the wave-function in the classical limit. Thus, at least in the context of a simple mathematical model, we combine the technical and conceptual virtues of decoherence (which fails to solve the measurement problem but launches the key idea that perturbations may come from the environment) with those of dynamical collapse models à la grw (which do solve the measurement problem but are ad hoc), without sharing their drawbacks: single measurement outcomes are obtained (instead of merely diagonal reduced density matrices), and no modification of quantum mechanics is needed. (shrink)

We give resource bounded versions of the Completeness Theorem for propositional and predicate logic. For example, it is well known that every computable consistent propositional theory has a computable complete consistent extension. We show that, when length is measured relative to the binary representation of natural numbers and formulas, every polynomial time decidable propositional theory has an exponential time (EXPTIME) complete consistent extension whereas there is a nondeterministic polynomial time (NP) decidable theory which has no polynomial time (...) class='Hi'>complete consistent extension when length is measured relative to the binary representation of natural numbers and formulas. It is well known that a propositional theory is axiomatizable (respectively decidable) if and only if it may be represented as the set of infinite paths through a computable tree (respectively a computable tree with no dead ends). We show that any polynomial time decidable theory may be represented as the set of paths through a polynomial time decidable tree. On the other hand, the statement that every polynomial time decidable, relative to the tally representation of natural numbers and formulas, is equivalent to P = NP. For predicate logic, we develop a complexity theoretic version of the Henkin construction to prove a complexity theoretic version of the Completeness Theorem. Our results imply that that any polynomial space decidable theory △ possesses a polynomial space computable model which is exponential space decidable and thus △ has an exponential space complete consistent extension. Similar results are obtained for other notions of complexity. (shrink)

We describe new results in parametrized complexity theory. In particular, we prove a number of concrete hardness results for W[P], the top level of the hardness hierarchy introduced by Downey and Fellows in a series of earlier papers. We also study the parametrized complexity of analogues of PSPACE via certain natural problems concerning k-move games. Finally, we examine several aspects of the structural complexity of W [P] and related classes. For instance, we show that W[P] can be characterized in terms (...) of the DTIME ) and NP. (shrink)

The current study investigated the adaptations which occur in visual search behaviour as a function of expertise in rugby union players when completing attacking scenarios. Ten experienced players and ten novice players completed 2 vs. 1 attacking game scenarios. Starting with the ball in hand and wearing a mobile eye tracker throughout, participants were required to score a try against a defender. The scenarios allowed for a pass to their supporting player or trying to run past the defender. No between (...) group differences were found in fixating on the supporting attacking player. However, EP increased the length and frequency looking at the area immediately ahead of the supporting player, particularly when executing a spin pass. NP fixated longer and more frequently at the defender, whilst EP fixated more frequently in the space the supporting player would run into in Switch and Dummy Switch scenarios. More successful passes were completed and tries scored by EP compared to NP. Differences in visual search behaviour between experienced and NP suggest that the experts extract information from areas directly related to guiding the motor action; the space immediately ahead of the support player to pass the ball in. Contrastingly, novices use a more allocentric perspective where the actions from the defender are used to guide their motor actions. (shrink)

We analyze the cognitive strategies underlying performance in the Number task, a Math game that requires both arithmetic fluency and mathematical creativity. In this game all elements in a set of numbers have to be used precisely once to create a target number with basic arithmetic operations. We argue that some instances of this game are NP complete, by showing its relation to the well-known Partition problem. We propose heuristics based on the distinction in forward and backward reasoning. The (...) Number Game is part of Math Garden, a popular online educational platform for practicing and monitoring math skills using innovations in computerized adaptive testing. These educational games generate enormous amounts of rich data on children's cognitive development. We found converging evidence for the use of forward proximity heuristics in the data of Math Garden, consisting of more than 20 million answers to 1,700 items. Item difficulties and the structure of correct answers were analyzed. (shrink)

A dichotomy result of Sevenster (2014) [29] completely classified the quantifier prefixes of regular Independence-Friendly (IF) logic according to the patterns of quantifier dependence they contain. On one hand, prefixes that contain “Henkin” or “signalling” patterns were shown to characterize fragments of IF logic that capture NP-complete problems; all the remaining prefixes were shown instead to be essentially first-order. In the present paper we develop the machinery which is needed in order to extend the results of Sevenster to non-prenex, (...) regular IF sentences. This involves shifting attention from quantifier prefixes to a (rather general) class of syntactical tree prefixes. We partially classify the fragments of regular IF logic that are thus determined by syntactical trees; in particular, a) we identify four classes of tree prefixes that are neither signaling nor Henkin, and yet express NP-complete problems and other second-order concepts; and b) we give more general criteria for checking the first-orderness of an IF sentence. (shrink)

We analyze the cognitive strategies underlying performance in the Number task, a Math game that requires both arithmetic fluency and mathematical creativity. In this game all elements in a set of numbers have to be used precisely once to create a target number with basic arithmetic operations. We argue that some instances of this game are NP complete, by showing its relation to the well-known Partition problem. We propose heuristics based on the distinction in forward and backward reasoning. The (...) Number Game is part of Math Garden, a popular online educational platform for practicing and monitoring math skills using innovations in computerized adaptive testing. These educational games generate enormous amounts of rich data on children's cognitive development. We found converging evidence for the use of forward proximity heuristics in the data of Math Garden, consisting of more than 20 million answers to 1,700 items. Item difficulties and the structure of correct answers were analyzed. (shrink)

The problem is addressed of establishing the satisfiability of prenex formulas involving a single universal quantifier, in diversified axiomatic set theories. A rather general decision method for solving this problem is illustrated through the treatment of membership theories of increasing strength, ending with a subtheory of Zermelo-Fraenkel which is already complete with respect to the ∀*∀ class of sentences. NP-hardness and NP-completeness results concerning the problems under study are achieved and a technique for restricting the universal quantifier is presented.

Local deterministic string-to-string transductions arise in natural language processing (NLP) tasks such as letter-to-sound translation or pronunciation modeling. This class of transductions is a simple generalization of morphisms of free monoids; learning local transductions is essentially the same as inference of certain monoid morphisms. However, learning even a highly restricted class of morphisms, the so-called fine morphisms, leads to intractable problems: deciding whether a hypothesized fine morphism is consistent with observations is an NP-complete problem; and maximizing classification accuracy of (...) the even smaller class of alphabetic substitution morphisms is APX-hard. These theoretical results provide some justification for using the kinds of heuristics that are commonly used for this learning task. (shrink)

Design and analysis of algorithms can be a difficult subject for students due to its sometimes-abstract nature and its use of a wide variety of mathematical tools. Here the author, an experienced and successful textbook writer, makes the subject as straightforward as possible in an up-to-date textbook incorporating various new developments appropriate for an introductory course. This text presents the main techniques of algorithm design, namely, divide-and-conquer algorithms, greedy algorithms, dynamic programming algorithms, and backtracking. Graph algorithms are studied in detail, (...) and a careful treatment of the theory of NP-completeness is presented. In addition, the text includes useful introductory material on mathematical background including order notation, algorithm analysis and reductions, and basic data structures. This will serve as a useful review and reference for students who have covered this material in a previous course. Features The first three chapters provide a mathematical review, basic algorithm analysis, and data structures. Detailed pseudocode descriptions of the algorithms along with illustrative algorithms are included. Proofs of correctness of algorithms are included when appropriate. The book presents a suitable amount of mathematical rigor. After reading and understanding the material in this book, students will be able to apply the basic design principles to various real-world problems that they may encounter in their future professional careers. (shrink)

In computer science, an algorithm is an unambiguous specification of how to solve a class of problems. Algorithms can perform calculation, data processing and automated reasoning tasks. As an effective method, an algorithm can be expressed within a finite amount of space and time and in a well-defined formal language for calculating a function. Starting from an initial state and initial input (perhaps empty), the instructions describe a computation that, when executed, proceeds through a finite number of well-defined successive states, (...) eventually producing "output" and terminating at a final ending state. The transition from one state to the next is not necessarily deterministic; some algorithms, known as randomized algorithms, incorporate random input. This book introduces a set of concepts in solving problems computationally such as Growth of Functions; Backtracking; Divide and Conquer; Greedy Algorithms; Dynamic Programming; Elementary Graph Algorithms; Minimal Spanning Tree; Single-Source Shortest Paths; All Pairs Shortest Paths; Flow Networks; Polynomial Multiplication, to ways of solving NP-Complete Problems, supported with comprehensive, and detailed problems and solutions, making it an ideal resource to those studying computer science, computer engineering and information technology. (shrink)

In the dissertation we study the complexity of generalized quantifiers in natural language. Our perspective is interdisciplinary: we combine philosophical insights with theoretical computer science, experimental cognitive science and linguistic theories. -/- In Chapter 1 we argue for identifying a part of meaning, the so-called referential meaning (model-checking), with algorithms. Moreover, we discuss the influence of computational complexity theory on cognitive tasks. We give some arguments to treat as cognitively tractable only those problems which can be computed in polynomial time. (...) Additionally, we suggest that plausible semantic theories of the everyday fragment of natural language can be formulated in the existential fragment of second-order logic. -/- In Chapter 2 we give an overview of the basic notions of generalized quantifier theory, computability theory, and descriptive complexity theory. -/- In Chapter 3 we prove that PTIME quantifiers are closed under iteration, cumulation and resumption. Next, we discuss the NP-completeness of branching quantifiers. Finally, we show that some Ramsey quantifiers define NP-complete classes of finite models while others stay in PTIME. We also give a sufficient condition for a Ramsey quantifier to be computable in polynomial time. -/- In Chapter 4 we investigate the computational complexity of polyadic lifts expressing various readings of reciprocal sentences with quantified antecedents. We show a dichotomy between these readings: the strong reciprocal reading can create NP-complete constructions, while the weak and the intermediate reciprocal readings do not. Additionally, we argue that this difference should be acknowledged in the Strong Meaning hypothesis. -/- In Chapter 5 we study the definability and complexity of the type-shifting approach to collective quantification in natural language. We show that under reasonable complexity assumptions it is not general enough to cover the semantics of all collective quantifiers in natural language. The type-shifting approach cannot lead outside second-order logic and arguably some collective quantifiers are not expressible in second-order logic. As a result, we argue that algebraic (many-sorted) formalisms dealing with collectivity are more plausible than the type-shifting approach. Moreover, we suggest that some collective quantifiers might not be realized in everyday language due to their high computational complexity. Additionally, we introduce the so-called second-order generalized quantifiers to the study of collective semantics. -/- In Chapter 6 we study the statement known as Hintikka's thesis: that the semantics of sentences like ``Most boys and most girls hate each other'' is not expressible by linear formulae and one needs to use branching quantification. We discuss possible readings of such sentences and come to the conclusion that they are expressible by linear formulae, as opposed to what Hintikka states. Next, we propose empirical evidence confirming our theoretical predictions that these sentences are sometimes interpreted by people as having the conjunctional reading. -/- In Chapter 7 we discuss a computational semantics for monadic quantifiers in natural language. We recall that it can be expressed in terms of finite-state and push-down automata. Then we present and criticize the neurological research building on this model. The discussion leads to a new experimental set-up which provides empirical evidence confirming the complexity predictions of the computational model. We show that the differences in reaction time needed for comprehension of sentences with monadic quantifiers are consistent with the complexity differences predicted by the model. -/- In Chapter 8 we discuss some general open questions and possible directions for future research, e.g., using different measures of complexity, involving game-theory and so on. -/- In general, our research explores, from different perspectives, the advantages of identifying meaning with algorithms and applying computational complexity analysis to semantic issues. It shows the fruitfulness of such an abstract computational approach for linguistics and cognitive science. (shrink)

We propose two alternatives to Xu’s axiomatization of Chellas’s STIT. The first one simplifies its presentation, and also provides an alternative axiomatization of the deliberative STIT. The second one starts from the idea that the historic necessity operator can be defined as an abbreviation of operators of agency, and can thus be eliminated from the logic of Chellas’s STIT. The second axiomatization also allows us to establish that the problem of deciding the satisfiability of a STIT formula without temporal operators (...) is NP-complete in the single-agent case, and is NEXPTIME-complete in the multiagent case, both for the deliberative and Chellas’s STIT. (shrink)

Since it was first proposed by Moses, Shoham, and Tennenholtz, the social laws paradigm has proved to be one of the most compelling approaches to the offline coordination of multiagent systems. In this paper, we make four key contributions to the theory and practice of social laws in multiagent systems. First, we show that the Alternating-time Temporal Logic (atl) of Alur, Henzinger, and Kupferman provides an elegant and powerful framework within which to express and understand social laws for multiagent systems. (...) Second, we show that the effectiveness, feasibility, and synthesis problems for social laws may naturally be framed as atl model checking problems, and that as a consequence, existing atl model checkers may be applied to these problems. Third, we show that the complexity of the feasibility problem in our framework is no more complex in the general case than that of the corresponding problem in the Shoham–Tennenholtz framework (it is np-complete). Finally, we show how our basic framework can easily be extended to permit social laws in which constraints on the legality or otherwise of some action may be explicitly required. We illustrate the concepts and techniques developed by means of a running example. (shrink)

By a fragment of a natural language we mean a subset of thatlanguage equipped with semantics which translate its sentences intosome formal system such as first-order logic. The familiar conceptsof satisfiability and entailment can be defined for anysuch fragment in a natural way. The question therefore arises, for anygiven fragment of a natural language, as to the computational complexityof determining satisfiability and entailment within that fragment. Wepresent a series of fragments of English for which the satisfiabilityproblem is polynomial, NP-complete, (...) EXPTIME-complete,NEXPTIME-complete and undecidable. Thus, this paper represents a casestudy in how to approach the problem of determining the logicalcomplexity of various natural language constructions. In addition, wedraw some general conclusions about the relationship between naturallanguage and formal logic. (shrink)

Linear logic, introduced by Girard, is a refinement of classical logic with a natural, intrinsic accounting of resources. This accounting is made possible by removing the ‘structural’ rules of contraction and weakening, adding a modal operator and adding finer versions of the propositional connectives. Linear logic has fundamental logical interest and applications to computer science, particularly to Petri nets, concurrency, storage allocation, garbage collection and the control structure of logic programs. In addition, there is a direct correspondence between polynomial-time computation (...) and proof normalization in a bounded form of linear logic. In this paper we show that unlike most other propositional logics, full propositional linear logic is undecidable. Further, we prove that without the modal storage operator, which indicates unboundedness of resources, the decision problem becomes PSPACE-complete. We also establish membership in NP for the multiplicative fragment, NP-completeness for the multiplicative fragment extended with unrestricted weakening, and undecidability for fragments of noncommutative propositional linear logic. (shrink)

We provide a Kripke semantics for a STIT logic with the "next" operator. As the atemporal group STIT is undecidable and unaxiomatizable, we are interested in strict fragments of atemporal group STIT. First we prove that the satisfiability problem of a formula of the fragment made up of individual coalitions plus the grand coalition is also NEXPTIME-complete. We then generalize this result to a fragment where coalitions are in a given lattice. We also prove that if we restrict the (...) language to nested coalitions the satisfiability problem is NP-complete if the number of agents is fixed and PSPACE-complete if the number of agents is variable. Finally we embed individual STIT with the "next" operator into a fragment of atemporal group STIT. (shrink)