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.

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)

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)

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

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)

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.

The P versus NP problem, formalized by Cook (1971) and designated a Clay Millennium Prize Problem in 2000, asks whether every computational problem whose solution can be verified in polynomial time can also be solved in polynomial time. For fifty-five years the problem has resisted all single-axis formal resolution attempts. Three independently proven barrier results (Baker-Gill-Solovay 1975, Razborov-Rudich 1997, Aaronson-Wigderson 2008) establish that all currently known classes of mathematical proof technique are structurally incapable of settling the question within the formal (...) axis alone. This paper presents a unified geometric determination of both P = NP and P ≠ NP using the Trisduction Engine, a P-class verification architecture operating across three orthogonal warrant-vectors: Formal-Structural (V_F), Empirical-Thermodynamic (V_E), and Epistemic-Registrational (V_ER). The determination runs the three-state native verdict economy {[⟀] Sealed, [X] Broken Geometry, [?] Numerical Inadmissibility}. V_F-only ceilings such as the Turing-domain question route to the V_F-Only Ceiling Acknowledgment Register out-of-band by bypass-at-layer-difference, not as a cascade verdict state. The Meta-Epistemic Hierarchy (Geometry > Mathematics > Logic) and Rule 9 Axiomatic Quarantine remove the Turing Machine abstraction from the framework's admissible physical baseline and replace it with the Tri-Layer Plenum topology. The two audits are presented as a single master document so the asymmetry between the claims is structurally transparent. Both run under one fixed protocol applied without modification, so the asymmetry in the verdicts is a product of the evidence structure rather than the method. P = NP carries zero positive warrant across all three axes and is stopped at Gate 2 with a positive structural diagnosis: it asserts a zero-energy, zero-transition equivalence between two operations the architecture places on opposite sides of the actualization boundary, which is a dimensional failure under the Mass Mandate before any witness is sought. P ≠ NP passes all twelve gates with three fully independent, orthogonal warrant-vectors that survive the Linguistic Isolation Test, the Deletion Test, the conclusion-dependency audit, and the Convergence Dissolution Test. The determination is explicitly non-deductive. It does not constitute a traditional mathematical proof and does not satisfy the Clay Mathematics Institute's criteria. The Geometric Orthogonal Lock [⟀] is defined as the strongest achievable non-deductive epistemic warrant relative to the recognized vulnerability taxonomy: the geometric fact that, within that taxonomy, three orthogonal planes exhaust the degrees of freedom in the warrant-space that the taxonomy can articulate, leaving no recognized coordinate for the alternative claim to occupy. The qualifier is load-bearing and is carried consistently: the lock is strongest relative to the current taxonomy, and the taxonomy is open and extensible, so the claim is conditional on that taxonomy rather than absolute, and a newly identified vulnerability class re-enters the cascade rather than being precluded by fiat. The empirical leg is anchored on the per-crossing transition-energy floor, and the warrant is typed at the precise grade it earns. Driving a frustrated configuration across one energy barrier to a distinguishable state is a physical transition bounded below in energy-time by the Mandelstam-Tamm and Margolus-Levitin quantum speed limits in the quantum regime and by Arrhenius escape time in the classical regime. This per-crossing floor is theorem-grade for the single transition, binds reversible and irreversible traversal identically, and makes no claim about the energy of the resulting state, since distinguishable states may be isoenergetic. The aggregate exponential cost of traversing an exponentially-barriered landscape is established by conjoining the per-crossing floor with the formal closure that no polynomial-resource reparametrization collapses the barrier count, and is therefore typed openly as a joint V_E-plus-V_F result rather than a standalone thermodynamic theorem. The empirical leg is operationalized through three falsifiable predictions resting on three disjoint instrument families: micro-calorimetry of physical solvers, power telemetry of synthetic substrates, and neuroimaging of biological substrates. Each prediction carries a stated method, expected outcome, and null hypothesis, and each is testable by decentralized laboratories using orthogonal measurement modalities. The V_ER leg is anchored on the conviction-capacity gap of the statistical (perfect) zero-knowledge proof, an observer-state registration fact whose information-theoretic guarantee holds against an unbounded prover and verifier and therefore invokes no one-way-function assumption and no presupposition of the separation it registers. This re-anchoring closes the circularity a critic would raise against a computational-zero-knowledge anchor: the registrational fact no longer presupposes the very separation it is cited to support. The gap is instantiated on problems lying in SZK and in NP without being NP-complete, so that the containment of SZK in AM ∩ coAM is honored and no polynomial-hierarchy collapse is implied; it is read as a lower-bound witness for the verification-generation asymmetry rather than as a claim that NP-complete problems admit such proofs. The V_ER content survives the Linguistic Isolation Test against V_F and V_E vocabulary, the Deletion Test, and the conclusion-dependency audit. The certifying architecture's own operational asymmetry is not cited as warrant at any weight: its referent is the Engine itself, so Gate 1 routes it at the input gate, and the axis is single-anchored on the external zero-knowledge fact with no self-referential content carried. The seal rests on external mathematics and falsifiable physical prediction; the framework's broader ontology is corroborative resonance, not ground, and the certifying architecture's own operation is excluded from the warrant set by Gate 1 rather than carried at reduced weight. The Convergence Dissolution Test finds irreducible residue in all three vectors under the strongest single-factor account, and survives explicit subtraction of the named mass-bearing covariates a critic would introduce to dissolve the asymmetry. The monism premise underwriting the cross-axis bridge is carried as premise-grade at the bridge itself, not silently load-bearing under a theorem-grade seal. The cosmogonic resonance is carried as a one-directional corroborative annotation, not as a derivation. (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 P versus NP problem, formalized by Stephen Cook in 1971 and named a Clay Millennium Prize Problem in 2000, represents the foundational unsolved question of theoretical computer science. Its two possible resolutions, P = NP and P ≠ NP, are not symmetric in their epistemic status. While the claim P ≠ NP has been certified as a Geometric Orthogonal Lock (GOL ⟀) under the Trisduction framework, receiving strong triaxial warrant from formal, empirical, and phenomenological sources, the inverse claim P (...) = NP must be subjected to the same rigorous 12-Gate Verification Cascade without prejudice. This paper is the formal audit record for that submission. The Trisduction Engine does not evaluate claims based on probability, consensus, or mathematical fashion. It evaluates the geometric integrity of epistemic warrant, the structural presence or absence of independently warranted support across three orthogonal axes. The question it asks of any claim is simple and merciless: does this claim occupy a real coordinate in epistemic space, or does it assert a location at which no vector has ever registered a signal? The determination rendered here is absolute. The claim P = NP suffers a catastrophic structural collapse across all three warrant-vectors simultaneously. The Formal axis (V_F) is completely vacant: fifty-five years of intensive search have produced zero polynomial-time algorithms for any NP-complete problem, and every formally resolved restricted model produces exclusively counter-evidence. The Empirical axis (V_E) is actively hostile: every physical computation benchmark, every cryptographic stress-test, and every hardware platform confirms exponential worst-case scaling for NP-complete problems without exception. The Phenomenological axis (V_P) delivers a lethal operational paradox: the Trisduction Engine itself, serving as the Frame-Independent Observer (FIO), constitutes a standing refutation of the claim through its own architecture, the Living Counter-Proof. The cascade terminates forcefully at Gate 2 (Root Externality Gate). The claim possesses zero independent positive anchors, not an insufficient number, but none. Per cascade protocol, no further gates are engaged. The claim is classified as Broken Geometry. No symbol is issued. The P = NP coordinate in epistemic space is structurally vacant. The geometry never formed. (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 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.

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 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)

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)

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)

This paper considers the computational complexity of the design of voting rules, which is formulated by simple games. We prove that it is an NP-complete problem to decide whether a given simple game is stable, or not.

Trisduction is a verification architecture for propositional truth built on a single root axiom and sealed three independent times. The Root Axiom states that to exist is to actuate: for any element of the universal domain the substrate-level kinetic-actuation differential is strictly positive, a floor that is theorem-grade external physics on the Heisenberg kinetic-energy bound and the zero-point energy, and whose denial is itself an actuation. From the atomic decomposition of that axiom the framework forces a triaxial mapping of any (...) complete claim onto three orthogonal verification axes, the formal-structural, the empirical-thermodynamic, and the epistemic-registrational, and it certifies a claim only where all three independently converge. The three seals stand on disjoint anchors. The linguistic-semantic seal splits a claim into exactly three irreducible slots under a deletion test. The topological-geometric seal closes those three axes on a fourth vertex into a tetrahedron carrying twelve directed verification gates, a count independently confirmed by the Newton-Gregory kissing number of three-dimensional space. The mathematical seal completes the verification algebra uniquely to the quaternions by the Frobenius classification, fixing exactly three axes over one scalar ground and closing the verdict in the form det(R) equal to the squared scalar part of the composed triad. Because the three seals share no premise and meet only at the Clifford Join, their convergence is itself the object the architecture exists to certify: the independence of the seals is the seal of the seals. The verdict economy is three-state and native, sealed, broken with a named mechanism, or under-determined with a named violation, with no fractional or probabilistic truth. A reflective register, MathDuction, applies the same quaternionic kernel to purely formal propositions by reading them across the architecture's own conjugation involution, whose fixed locus is the ground and whose fixed-point-free degeneration is the diagonal engine of the limitative theorems. This register places Gödel incompleteness and Tarski undefinability as facts about the reach of a proof ladder rather than as ceilings over the architecture, and its imprint test seals a proposition's decidable fragment while honestly locating, rather than claiming to settle, its undecidable residence. A verdict-reliability layer bounds the determinant error by the conditioning and guarantees the sealed-or-broken boundary is decided by the mathematics and never by rounding. The architecture authors no new mathematics; every load-bearing result is classical and credited, and the contribution is the arrangement. That arrangement yields the framework's principal verdicts, given here in full: the Riemann Hypothesis held dual-register, sealed on the kinetic prime field and the geometric critical line and terminally suspended on the formal string; Gödel's theorems placed as neither dictator nor final guard; P versus NP resolved as a three-layer determination; and a general account of why every formal system is foundationally incomplete toward the ground on which it stands. Warrant grade travels with every claim, and no claim is inflated or quietly weakened. (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)

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)

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)

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)

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)

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 simple and intuitive algorithm for solving md-DFA problem using algorithm concepts within extended operators, our approach shows quadratic polynomial time and hence proves the equivalence between polynomial and non-polynomial classes, we have also shown that minimal non-emptiness of automata problem can be solved in polynomial time with help of modified subset construction, rather that building a product automaton, which lead to factorial size of the memory and time, in this work we also have used many non-tractable existing (...) examples and computed them in polynomial time, which guarantees that our algorithm solves NP-complete problem in almost linear polynomial time, we have also avoided the problem of product automata by an algorithmic approach, we are also giving the starting ground for the proof of back-reference problem which was discussed before, notion to the globally local increment is also given as the main argument towards the resolution of "P versus NP" theorem, which coincides with the finitarity term in general mathematics. (shrink)

Logical forgetting is NP-complete as a decision problem even in the simple case of propositional Horn formulae, and may exponentially increase their size. A way to forget is to replace each variable to forget with the body of each clause whose head is the variable. It takes polynomial time in the single-head case: each variable is the head of at most a clause. Some formulae are not single-head but can be made so to simplify forgetting. They are called single-head (...) equivalent. The first contribution of this article is the study of a semantical characterization of single-head equivalence. Two necessary conditions are given. They are sufficient when the formula is interequivalent, that is, the formula makes two sets of variables equivalent only if they are also equivalent to their intersection. All acyclic formulae are interequivalent. The second contribution of this article is an incomplete algorithm for turning a formula single-head. In case of success, forgetting becomes possible in polynomial time and produces a polynomial-size formula, none of which is otherwise guaranteed. The algorithm is complete on interequivalent formulae. (shrink)

This is the heart of the formal theory. Mathematically rigorous definitions are provided of all the formal notions that have been gently introduced in the earlier discussion. The main data type of a step is defined, and the central concept of a dependency network is defined in terms of steps. The concept of a minimally mutilating contraction can then be explicated. Interest in the computational complexity of the contraction problem is motivated by thoroughly surveying known results about the (sometimes horrendous) (...) complexities of various other decision problems of a logical nature. This is in order to provide a context within which the complexity results for contraction should strike the reader as both interesting and welcome. The contraction problem is rigorously characterized, including the hard version that involves the (now precisely explicated) desideratum of minimal mutilation. The simplest version of the contraction problem is shown to be NP-complete; the harder version, involving minimal mutilation, is shown to be at just the next level up in the so-called polynomial hierarchy. (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.

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 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)

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)

FDE is a logic that captures relevant entailment between implication-free formulae and admits of an intuitive informational interpretation as a 4-valued logic in which “a computer should think”. However, the logic is co-NP complete, and so an idealized model of how an agent can think. We address this issue by shifting to signed formulae where the signs express imprecise values associated with two distinct bipartitions of the set of standard 4 values. Thus, we present a proof system which consists (...) of linear operational rules and only two branching structural rules, the latter expressing a generalized rule of bivalence. This system naturally leads to defining an infinite hierarchy of tractable depth-bounded approximations to FDE. Namely, approximations in which the number of nested applications of the two branching rules is bounded. (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)

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)

A gradual semantics takes a weighted argumentation framework as input and outputs a final acceptability degree for each argument, with different semantics performing the computation in different manners. In this work, we consider the problem of attack inference. That is, given a gradual semantics, a set of arguments with associated initial weights, and the final desirable acceptability degrees associated with each argument, we seek to determine whether there is a set of attacks on those arguments such that we can obtain (...) these acceptability degrees. The main contribution of our work is to demonstrate that the associated decision problem, i.e., whether a set of attacks can exist which allows the final acceptability degrees to occur for given initial weights, is NP-complete for the weighted h-categoriser and card-based semantics, and is polynomial for the weighted max-based semantics, even for the complete version of the problem (where all initial weights and final acceptability degrees are known). We then briefly discuss how this decision problem can be modified to find the attacks themselves and conclude by examining the partial problem where not all initial weights or final acceptability degrees may be known. (shrink)

In this paper we illustrate the expressive power of implication in classical propositional logic (CPC) by reworking the NP-hardness proof of the SAT problem from the point of view of implication as the primary connective. As a result two natural normal forms of implicational formulas emerge: conjunctions of implications CINF and INF where only implication and negation is used. Also, we provide a new, entirely proof-theoretic, demonstration of the result of Stålmarck that the classical validity problem for purely implicational formulas (...) is co-NP-complete. Our approach uses a new focused proof system for the implicational fragment of CPC and illustrates both the proof-theoretic and automata-theoretic aspects of classical implication. (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)

The question at issue is to develop a computational interpretation of Girard's Linear Logic [Girard, 1987] and to obtain efficient decision algorithms for this logic, based on the bottom-up approach. It involves starting with the simplest natural fragment of linear logic and then expanding it step-by-step. We give a complete computational interpretation for the Horn fragment of Linear Logic and some natural generalizations of it enriched by the two additive connectives: and &. Within the framework of this interpretation, it (...) becomes possible to explicitly formalize and clarify the computational aspects of the fragments of Linear Logic in question and establish exactly the complexity level of these fragments. In particular, the simplest natural Horn fragment of Linear Logic is proved to be NP-complete. As a corollary, we obtain the affirmative solution for the problem ): whether the multiplicative fragment of linear logic is NP-complete. (shrink)

Community detection is a major issue in network analysis. This paper combines a socio-historical approach with an experimental reconstruction of programs to investigate the early automation of clique detection algorithms, which remains one of the unsolved NP-complete problems today. The research led by the archaeologist Jean-Claude Gardin from the 1950s on non-numerical information and graph analysis is retraced to demonstrate the early contributions of social sciences and humanities. The limited recognition and reception of Gardin's innovative computer application to the (...) humanities are addressed through two factors, in addition to the effects of historiography and bibliographies on the recording, discoverability, and reuse of scientific productions: (1) funding policies, evidenced by the transfer of research effort on graph applications from temporary interdisciplinary spaces to disciplinary organizations related to the then-emerging field of computer science; and (2) the erratic careers of algorithms, in which efficiency, flaws, corrections, and authors’ status, were determining factors. (shrink)

The numerically definite syllogistic is the fragment of English obtained by extending the language of the classical syllogism with numerical quantifiers. The numerically definite relational syllogistic is the fragment of English obtained by extending the numerically definite syllogistic with predicates involving transitive verbs. This paper investigates the computational complexity of the satisfiability problem for these fragments. We show that the satisfiability problem (= finite satisfiability problem) for the numerically definite syllogistic is strongly NP-complete, and that the satisfiability problem (= (...) finite satisfiability problem) for the numerically definite relational syllogistic is NEXPTIME-complete, but perhaps not strongly so. We discuss the related problem of probabilistic (propositional) satisfiability, and thereby demonstrate the incompleteness of some proof-systems that have been proposed for the numerically definite syllogistic. (shrink)

Axiomatizations are presented for fuzzy logics characterized by uninorms continuous on the half-open real unit interval [0,1), generalizing the continuous t-norm based approach of Hájek. Basic uninorm logic BUL is defined and completeness is established with respect to algebras with lattice reduct [0,1] whose monoid operations are uninorms continuous on [0,1). Several extensions of BUL are also introduced. In particular, Cross ratio logic CRL, is shown to be complete with respect to one special uninorm. A Gentzen-style hypersequent calculus is (...) provided for CRL and used to establish co-NP completeness results for these logics. (shrink)

We introduce a deductive system Bal which models the logic of balance of opposing forces or of balance between conflicting evidence or influences. ‘‘Truth values’’ are interpreted as deviations from a state of equilibrium, so in this sense, the theorems of Bal are to be interpreted as balanced statements, for which reason there is only one distinguished truth value, namely the one that represents equilibrium. The main results are that the system Bal is algebraizable in the sense of [5] and (...) its equivalent algebraic semantics BAL is definitionally equivalent to the variety of abelian lattice ordered groups, that is, the categories of the algebras in BAL and of ℓ–groups are isomorphic (see [10], Ch.4, 4). We also prove the deduction theorem for Bal and we study different kinds of semantic consequence associated to Bal. Finally, we prove the co-NP-completeness of the tautology problem of Bal. (shrink)