The number of variables used by a first-order query is a fundamental measure which has been studied in numerous contexts, and which is known to be highly relevant to the task of query evaluation. In this article, we study this measure in the context of existential positive queries. Building on previous work, we present a combinatorial quantity defined on existential positive queries; we show that this quantity not only characterizes the minimum number of variables needed to express a given existential positive query by another existential positive query, but also that it characterizes the minimum number of variables needed to express a given existential positive query, over all first-order queries. Put differently and loosely, we show that for any existential positive query, no variables can ever be saved by moving out of existential positive logic to first-order logic. One component of this theorem’s proof is the construction of a winning strategy for a certain Ehrenfeucht-Fraiissé type game.

A structure enjoys the Herbrand property if, whenever it satisfies an equality between some terms, these terms are unifiable. On such structures the expressive power of equalities becomes trivial, as their semantic satisfiability is reduced to a purely syntactic check. In this work, we introduce the notion of Herbrand property and develop it in a finite model-theoretic perspective. We provide, indeed, a canonical realization of the new concept by what we call quasi-Herbrand models and observe that, in stark contrast with the naive implementation of the property via standard Herbrand models, their universe can be finite even in presence of functions in the vocabulary. We exploit this feature to decide and collapse the general and finite version of the satisfiability and entailment problems for previously unsettled fragments of first-order logic. We take advantage of the Herbrand property also to establish novel and tight complexity results for the aforementioned decision questions. In particular, we show that the finite containment problem for quantified conjunctive queries is NPTIME-complete, tightening along two dimensions the known 3EXPTIME upper bound for the general version of the problem (Chen, Madelaine, and Martin, LICS'08). We finally present an alternative view on this result by generalizing to such queries the classic characterization of conjunctive query containment via polynomial-time verifiable homomorphisms (Chandra and Merlin, STOC'77).

The evaluation of a query over a probabilistic database boils down to computing the probability of a suitable Boolean function, the lineage of the query over the database. The method of query compilation approaches the task in two stages: first, the query lineage is implemented (compiled) in a circuit form where probability computation is tractable; and second, the desired probability is computed over the compiled circuit. A basic theoretical quest in query compilation is that of identifying pertinent classes of queries whose lineages admit compact representations over increasingly succinct, tractable circuit classes.

We present new results on the size of OBDD representations of structurally characterized classes of CNF formulas. First, we prove that variable convex formulas (that is, formulas with incidence graphs that are convex with respect to the set of variables) have polynomial OBDD size. Second, we prove an exponential lower bound on the OBDD size of a family of CNF formulas with incidence graphs of bounded degree. We obtain the first result by identifying a simple sufficient condition—which we call the few subterms property—for a class of CNF formulas to have polynomial OBDD size, and show that variable convex formulas satisfy this condition. To prove the second result, we exploit the combinatorial properties of expander graphs; this approach allows us to establish an exponential lower bound on the OBDD size of formulas satisfying strong syntactic restrictions.

Introduced by Darwiche (2011), sentential decision diagrams (SDDs) are essentially as tractable as ordered binary decision diagrams (OBDDs), but tend to be more succinct in practice. This makes SDDs a prominent representation language, with many applications in artificial intelligence and knowledge compilation. We prove that SDDs are more succinct than OBDDs also in theory, by constructing a family of boolean functions where each member has polynomial SDD size but exponential OBDD size. This exponential separation improves a quasipolynomial separation recently established by Razgon (2014), and settles an open problem in knowledge compilation (Darwiche, 2011).

We study the problem of checking whether an existential sentence (i.e., a first-order sentence in prefix form built using existential quantifiers and all Boolean connectives) is true in a finite partially ordered set (a poset). A poset is a reflexive, antisymmetric, and transitive digraph. The problem encompasses the fundamental embedding problem of finding an isomorphic copy of a poset as an induced substructure of another poset. Model checking existential logic is already NP-hard on a fixed poset; thus, we investigate structural properties of posets yielding conditions for fixed-parameter tractability when the problem is parameterized by the sentence. We identify width as a central structural property (the width of a poset is the maximum size of a subset of pairwise incomparable elements); our main algorithmic result is that model checking existential logic on classes of finite posets of bounded width is fixed-parameter tractable. We observe a similar phenomenon in classical complexity, in which we prove that the isomorphism problem is polynomial-time tractable on classes of posets of bounded width; this settles an open problem in order theory. We surround our main algorithmic result with complexity results on less restricted, natural neighboring classes of finite posets, establishing its tightness in this sense. We also relate our work with (and demonstrate its independence of) fundamental fixed-parameter tractability results for model checking on digraphs of bounded degree and bounded clique-width.

We study the computational problem of checking whether a logical sentence is true in a finite abelian group. We prove that model checking first-order sentences on finite abelian groups is fixed-parameter tractable, when parameterized by the size of the sentence. We also prove that model checking monadic second-order sentences on finite abelian groups finitely presented by integer matrices is not fixed-parameter tractable (under standard assumptions in parameterized complexity).

Existential positive queries are logical sentences built from conjunction, disjunction, and existential quantification, and are also known as select-project-join-union queries in data-base theory, where they are recognized as a basic and fundamental class of queries. It is known that the number of variables needed to express an existential positive query is the crucial parameter determining the complexity of evaluating it on a database, and is hence a natural measure from the perspective of query optimization and rewriting. In this artcle, we study the complexity of the natural decision problem associated to this measure, which we call the expressibility problem: Given an existential positive query and a number k, can the query be expressed using k (or fewer) variables? We precisely determine the complexity of the expressibility problem, showing that it is complete for the level Πp2 of the polynomial hierarchy. Moreover, we prove that the expressibility problem is undecidable in positive logic (that is, existential positive logic plus universal quantification), thus establishing existential positive logic as a maximal syntactic fragment where expressibility is decidable.

Journal Article Finite RDP-algebras: duality, coproducts and logic Get access Simone Bova, Simone Bova Department of Mathematics, 1326 Stevenson Center, Vanderbilt University, Nashville, TN 37240, USA.E-mail: [email protected] Search for other works by this author on: Oxford Academic Google Scholar Diego Valota Diego Valota Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, Milan, Italy.E-mail: [email protected] Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 22, Issue 3, June 2012, Pages 417–450, https://doi.org/10.1093/logcom/exr006 Published: 25 May 2011 Article history Received: 03 February 2010 Published: 25 May 2011

This paper is divided into two parts. In the present Part I, our main objective is to analyse Mamdani-type fuzzy control systems in logical terms, with special emphasis on the fuzzy inference process. To that end, we provide our own inference procedure, cast in the language of standard many-valued logics. We give an ample discussion of the logical meaning of our procedure. We eventually show how to fully recover Mamdani-type fuzzy inference from the latter. In this sense, then, our proposal may be regarded as a logical interpretation of Mamdani-type fuzzy inference. In Part II of this paper, we report on the results of an experiment on the technical analysis of the financial markets based on fuzzy techniques. The core algorithm implements the inference procedure described in this first part of the paper. In Part II, we will argue that the experimental results support the claim that our present theoretical analysis provides a sound interpretation of Mamdani-type fuzzy inference.

This paper is divided into two parts. In Part I, our main objective was to analyse Mamdani-type fuzzy control systems in logical terms, with special emphasis on the fuzzy inference process. To that end, we provided our own inference procedure, cast in the language of standard many-valued logics. We gave an ample discussion of the logical meaning of our procedure. We eventually showed how to fully recover Mamdani-type fuzzy inference from the latter. In this sense, then, our proposal in Part I may be regarded as a logical interpretation of Mamdani-type fuzzy inference. In the present Part II of this paper, we report on the results of an experiment on the technical analysis of the financial markets based on fuzzy techniques. The core algorithm implements the inference procedure described in the first part of the paper. The experimental results support the claim that our theoretical analysis in Part I provides a sound interpretation of Mamdani-type fuzzy inference.

We introduce a proof system for Hájek's logic BL based on a relational hypersequents framework. We prove that the rules of our logical calculus, called RHBL , are sound and invertible with respect to any valuation of BL into a suitable algebra, called (ω)[0,1]. Refining the notion of reduction tree that arises naturally from RHBL , we obtain a decision algorithm for BL provability whose running time upper bound is 2 O ( n ) , where n is the number of connectives of the input formula. Moreover, if a formula is unprovable, we exploit the constructiveness of a polynomial time algorithm for leaves validity for providing a procedure to build countermodels in (ω)[0, 1]. Finally, since the size of the reduction tree branches is O ( n 3 ), we can describe a polynomial time verification algorithm for BL unprovability.