<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE article PUBLIC "-//TaxonX//DTD Taxonomic Treatment Publishing DTD v0 20100105//EN" "../../nlm/tax-treatment-NS0.dtd">
<article xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:tp="http://www.plazi.org/taxpub" article-type="research-article" dtd-version="3.0" xml:lang="en">
  <front>
    <journal-meta>
      <journal-id journal-id-type="publisher-id">109</journal-id>
      <journal-id journal-id-type="index">urn:lsid:arphahub.com:pub:3dc5f44e-8666-58db-bc76-a455210e8891</journal-id>
      <journal-title-group>
        <journal-title xml:lang="en">JUCS - Journal of Universal Computer Science</journal-title>
        <abbrev-journal-title xml:lang="en">jucs</abbrev-journal-title>
      </journal-title-group>
      <issn pub-type="ppub">0948-695X</issn>
      <issn pub-type="epub">0948-6968</issn>
      <publisher>
        <publisher-name>Journal of Universal Computer Science</publisher-name>
      </publisher>
    </journal-meta>
    <article-meta>
      <article-id pub-id-type="doi">10.3217/jucs-015-01-0112</article-id>
      <article-id pub-id-type="publisher-id">29296</article-id>
      <article-categories>
        <subj-group subj-group-type="heading">
          <subject>Research Article</subject>
        </subj-group>
        <subj-group subj-group-type="scientific_subject">
          <subject>F.4 - MATHEMATICAL LOGIC AND FORMAL LANGUAGES</subject>
          <subject>H.2 - DATABASE MANAGEMENT</subject>
        </subj-group>
      </article-categories>
      <title-group>
        <article-title>Weak Functional Dependencies: Full Propositional Expressiveness for the Database Practitioner</article-title>
      </title-group>
      <contrib-group content-type="authors">
        <contrib contrib-type="author" corresp="yes">
          <name name-style="western">
            <surname>Hartmann</surname>
            <given-names>Sven</given-names>
          </name>
          <email xlink:type="simple">sven.hartmann@tu-clausthal.de</email>
          <xref ref-type="aff" rid="A1">1</xref>
        </contrib>
        <contrib contrib-type="author" corresp="no">
          <name name-style="western">
            <surname>Link</surname>
            <given-names>Sebastian</given-names>
          </name>
          <xref ref-type="aff" rid="A2">2</xref>
        </contrib>
      </contrib-group>
      <aff id="A1">
        <label>1</label>
        <addr-line content-type="verbatim">Clausthal University of Technology, Clausthal, Germany</addr-line>
        <institution>Clausthal University of Technology</institution>
        <addr-line content-type="city">Clausthal</addr-line>
        <country>Germany</country>
      </aff>
      <aff id="A2">
        <label>2</label>
        <addr-line content-type="verbatim">Victoria University of Wellington, Wellington, New Zealand</addr-line>
        <institution>Victoria University of Wellington</institution>
        <addr-line content-type="city">Wellington</addr-line>
        <country>New Zealand</country>
      </aff>
      <author-notes>
        <fn fn-type="corresp">
          <p>Corresponding author: Sven Hartmann (<email xlink:type="simple">sven.hartmann@tu-clausthal.de</email>).</p>
        </fn>
        <fn fn-type="edited-by">
          <p>Academic editor: </p>
        </fn>
      </author-notes>
      <pub-date pub-type="collection">
        <year>2009</year>
      </pub-date>
      <pub-date pub-type="epub">
        <day>01</day>
        <month>01</month>
        <year>2009</year>
      </pub-date>
      <volume>15</volume>
      <issue>1</issue>
      <fpage>112</fpage>
      <lpage>156</lpage>
      <uri content-type="arpha" xlink:href="http://openbiodiv.net/13BCF0F1-E118-509D-BEA0-0F3CAFB93E50">13BCF0F1-E118-509D-BEA0-0F3CAFB93E50</uri>
      <uri content-type="zenodo_dep_id" xlink:href="https://zenodo.org/record/7000621">7000621</uri>
      <permissions>
        <copyright-statement>Sven Hartmann, Sebastian Link</copyright-statement>
        <license license-type="creative-commons-attribution" xlink:href="" xlink:type="simple">
          <license-p>This article is freely available under the J.UCS Open Content License.</license-p>
        </license>
      </permissions>
      <abstract>
        <label>Abstract</label>
        <p>We study inference systems of weak functional dependencies in relational and complex-value databases. Functional dependencies form a very common class of database constraints. Designers and administrators proficiently utilise them in everyday database practice. Functional dependencies correspond to the linear-time decidable fragment of Horn clauses in propositional logic. Weak functional dependencies take advantage of arbitrary clauses, and therefore represent full propositional reasoning about data in databases. Moreover, they can be specified in a way that is very similar to functional dependencies. In relational databases the class of weak functional dependencies is finitely axiomatisable and the associated implication problem is coNP-complete in general. Our first main result extends this axiomatisation to databases in which complex elements can be derived from atomic ones by finitely many nestings of record, list and disjoint union constructors. In particular, we construct two nested tuples that can serve as a counterexample relation for the implication of weak functional dependencies. We further apply this construction to show an equivalence to truth assignments that serve as counterexamples for the implication of propositional clauses. Hence, we characterise the implication of weak functional dependencies in complex-value databases in completely logical terms. Consequently, state-of-the-art SAT solvers can be applied to reason about weak functional dependencies in relational and complex-value databases.</p>
      </abstract>
    </article-meta>
  </front>
</article>
