Semiring Provenance in the Infinite

<!DOCTYPE html> <html lang="en"> <head> <meta charset="utf-8"> <meta http-equiv="X-UA-Compatible" content="IE=edge"> <meta name="google" content="notranslate"> <meta http-equiv="Content-Language" content="en"> <meta name="viewport" content="width=device-width, initial-scale=1"> <meta name="csrf-token" content="FLbkycuwsydVWiuEBSSgvjb2rpMIbs9eI54ns0Vp"> <link rel="canonical" href="https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Tannen.3"> <meta name="DC.Publisher" content="Schloss Dagstuhl – Leibniz-Zentrum für Informatik" > <meta name="DC.Title" xml:lang="en" content="Semiring Provenance in the Infinite" > <meta name="DC.Creator.PersonalName" content="Brinke, Sophie" > <meta name="DC.Creator.PersonalName" content="Grädel, Erich" > <meta name="DC.Creator.PersonalName" content="Mrkonjić, Lovro" > <meta name="DC.Creator.PersonalName" content="Naaf, Matthias" > <meta name="DC.Subject" content="Semiring semantics" > <meta name="DC.Subject" content="first-order logic" > <meta name="DC.Subject" content="semirings with infinitary operations" > <meta name="DC.Date.created" scheme="ISO8601" content="2024-06-07" > <meta name="DC.Date.issued" scheme="ISO8601" content="2024-06-07" > <meta name="DC.Date.modified" scheme="ISO8601" content="2024-06-07" > <meta name="DC.Type" content="InProceedings" > <meta name="DC.Format" scheme="IMT" content="application/pdf" > <meta name="DC.Identifier" scheme="urn:nbn:de" content="urn:nbn:de:0030-drops-200997" > <meta name="DC.Identifier" scheme="DOI" content="10.4230/OASIcs.Tannen.3" > <meta name="DC.Identifier" scheme="URL" content="https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Tannen.3" > <meta name="DC.Source" content="The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen (2024)" > <meta name="DC.Source.URI" content="https://drops.dagstuhl.de/entities/volume/OASIcs-volume-119" > <meta name="DC.Language" scheme="ISO639-1" content="en" > <meta name="DC.Description" xml:lang="en" content="Semiring provenance evaluates database queries or logical statements not just by true or false but by values in some commutative semiring. This permits to track which combinations of atomic facts are responsible for the truth of a statement, and to derive further information, for instance concerning costs, confidence scores, number of proof trees, or access levels to protected data. The focus of this approach, proposed and developed to a large extent by Val Tannen and his collaborators, has first been on (positive) database query languages, but has later been extended, again in collaboration with Val, to a systematic semiring semantics for first-order logic (and other logical systems), as well as to a method for the strategy analysis of games. So far, semiring provenance has been studied for finite structures. To extend the semiring provenance approach for first-order logic to infinite domains, the semirings need to be equipped with addition and multiplication operators over infinite collections of values. This needs solid algebraic foundations, and we study here the necessary and desirable properties of semirings with infinitary operations to provide a well-defined and informative provenance analysis over infinite domains. We show that, with suitable definitions for such infinitary semiring, large parts of the theory of semiring provenance can be succesfully generalised to infinite structures." > <meta name="DC.Rights" scheme="DCTERMS.URI" content="https://creativecommons.org/licenses/by/4.0/legalcode" > <meta name="citation_conference_title" content="The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen (2024)" > <meta name="citation_doi" content="10.4230/OASIcs.Tannen.3" > <meta name="citation_firstpage" content="3:1" > <meta name="citation_lastpage" content="3:26" > <meta name="citation_title" content="Semiring Provenance in the Infinite" > <meta name="citation_language" content="en" > <meta name="citation_keyword" content="Semiring semantics" > <meta name="citation_keyword" content="first-order logic" > <meta name="citation_keyword" content="semirings with infinitary operations" > <meta name="citation_author" content="Brinke, Sophie" > <meta name="citation_author_institution" content="RWTH Aachen University, Germany" > <meta name="citation_author" content="Grädel, Erich" > <meta name="citation_author_institution" content="RWTH Aachen University, Germany" > <meta name="citation_author" content="Mrkonjić, Lovro" > <meta name="citation_author_institution" content="RWTH Aachen University, Germany" > <meta name="citation_author" content="Naaf, Matthias" > <meta name="citation_author_institution" content="RWTH Aachen University, Germany" > <meta name="citation_date" content="2024" > <meta name="citation_keyword" xml:lang="en" content="Semiring semantics" > <meta name="citation_keyword" xml:lang="en" content="first-order logic" > <meta name="citation_keyword" xml:lang="en" content="semirings with infinitary operations" > <meta name="citation_abstract_html_url" content="https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Tannen.3" > <meta name="citation_pdf_url" content="https://drops.dagstuhl.de/storage/01oasics/oasics-vol119-tannens-festschrift/OASIcs.Tannen.3/OASIcs.Tannen.3.pdf" > <meta name="citation_reference" content="K. Dannert, E. Grädel, M. Naaf, and V. Tannen. Semiring provenance for fixed-point logic. In C. Baier and J. Goubault-Larrecq, editors, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), volume 183 of Leibniz International Proceedings in Informatics (LIPIcs), pages 17:1-17:22, Dagstuhl, 2021. URL: https://doi.org/10.4230/LIPIcs.CSL.2021.17." > <meta name="citation_reference" content="J. Foster, T. Green, and V. Tannen. Annotated XML: queries and provenance. In Proceedings of PODS 2008, pages 271-280, 2008. URL: https://doi.org/10.1145/1376916.1376954." > <meta name="citation_reference" content="B. Glavic. Data provenance. Foundations and Trends in Databases, 9(3-4):209-441, 2021. URL: https://doi.org/10.1561/1900000068." > <meta name="citation_reference" content="E. Grädel and V. Tannen. Semiring provenance for first-order model checking. arXiv:1712.01980 [cs.LO], 2017. URL: https://arxiv.org/abs/1712.01980." > <meta name="citation_reference" content="E. Grädel and V. Tannen. Provenance analysis for logic and games. Moscow Journal of Combinatorics and Number Theory, 9(3):203-228, 2020. Preprint available at https://arxiv.org/abs/1907.08470. URL: https://doi.org/10.2140/moscow.2020.9.203." > <meta name="citation_reference" content="E. Grädel and V. Tannen. Provenance analysis and semiring semantics for first-order logic. submitted for publication, 2024." > <meta name="citation_reference" content="T. Green, G. Karvounarakis, and V. Tannen. Provenance semirings. In Principles of Database Systems PODS, pages 31-40. ACM, 2007. URL: https://doi.org/10.1145/1265530.1265535." > <meta name="citation_reference" content="T. Green and V. Tannen. The semiring framework for database provenance. In Proceedings of PODS, pages 93-99. ACM, 2017. URL: https://doi.org/10.1145/3034786.3056125." > <meta name="citation_reference" content="G. Markowsky. Chain-complete posets and directed sets with applications. Algebra universalis, 6(1):53-68, 1976. URL: https://doi.org/10.1007/BF02485815." > <meta name="citation_reference" content="G. Markowsky. Free completely distributive lattices. Proceedings of the American Mathematical Society, 74(2):227-228, 1979. URL: https://doi.org/10.1090/S0002-9939-1979-0524290-9." > <meta name="citation_reference" content="M. Naaf. Logic, Semirings, and Fixed Points. PhD thesis, RWTH Aachen University, 2024. Forthcoming." > <meta name="citation_publisher" content="Schloss Dagstuhl – Leibniz-Zentrum für Informatik" > <script type="application/ld+json"> { "@context": "https://schema.org/", "@type": "WebPage", "mainEntity": { "@type": "ScholarlyArticle", "url": "https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Tannen.3", "headline": "Semiring Provenance in the Infinite", "name": "Semiring Provenance in the Infinite", "abstract": "Semiring provenance evaluates database queries or logical statements not just by true or false but by values in some commutative semiring. This permits to track which combinations of atomic facts are responsible for the truth of a statement, and to derive further information, for instance concerning costs, confidence scores, number of proof trees, or access levels to protected data. The focus of this approach, proposed and developed to a large extent by Val Tannen and his collaborators, has first been on (positive) database query languages, but has later been extended, again in collaboration with Val, to a systematic semiring semantics for first-order logic (and other logical systems), as well as to a method for the strategy analysis of games.\r\nSo far, semiring provenance has been studied for finite structures. To extend the semiring provenance approach for first-order logic to infinite domains, the semirings need to be equipped with addition and multiplication operators over infinite collections of values. This needs solid algebraic foundations, and we study here the necessary and desirable properties of semirings with infinitary operations to provide a well-defined and informative provenance analysis over infinite domains. We show that, with suitable definitions for such infinitary semiring, large parts of the theory of semiring provenance can be succesfully generalised to infinite structures.", "keywords": [ "Semiring semantics", "first-order logic", "semirings with infinitary operations" ], "author": [ { "@type": "Person", "name": "Brinke, Sophie", "givenName": "Sophie", "familyName": "Brinke", "email": "mailto:brinke@logic.rwth-aachen.de", "sameAs": "https://orcid.org/0009-0005-2865-0069", "affiliation": "RWTH Aachen University, Germany" }, { "@type": "Person", "name": "Gr\u00e4del, Erich", "givenName": "Erich", "familyName": "Gr\u00e4del", "email": "mailto:graedel@logic.rwth-aachen.de", "sameAs": "https://orcid.org/0000-0002-8950-9991", "affiliation": "RWTH Aachen University, Germany" }, { "@type": "Person", "name": "Mrkonji\u0107, Lovro", "givenName": "Lovro", "familyName": "Mrkonji\u0107", "email": "mailto:mrkonjic@logic.rwth-aachen.de", "sameAs": "https://orcid.org/0000-0001-8812-7185", "affiliation": "RWTH Aachen University, Germany" }, { "@type": "Person", "name": "Naaf, Matthias", "givenName": "Matthias", "familyName": "Naaf", "email": "mailto:naaf@logic.rwth-aachen.de", "sameAs": "https://orcid.org/0000-0002-1099-5713", "affiliation": "RWTH Aachen University, Germany" } ], "position": 3, "dateCreated": "2024-06-07", "datePublished": "2024-06-07", "isAccessibleForFree": true, "license": "https://creativecommons.org/licenses/by/4.0/legalcode", "copyrightHolder": [ { "@type": "Person", "name": "Brinke, Sophie", "givenName": "Sophie", "familyName": "Brinke", "email": "mailto:brinke@logic.rwth-aachen.de", "sameAs": "https://orcid.org/0009-0005-2865-0069", "affiliation": "RWTH Aachen University, Germany" }, { "@type": "Person", "name": "Gr\u00e4del, Erich", "givenName": "Erich", "familyName": "Gr\u00e4del", "email": "mailto:graedel@logic.rwth-aachen.de", "sameAs": "https://orcid.org/0000-0002-8950-9991", "affiliation": "RWTH Aachen University, Germany" }, { "@type": "Person", "name": "Mrkonji\u0107, Lovro", "givenName": "Lovro", "familyName": "Mrkonji\u0107", "email": "mailto:mrkonjic@logic.rwth-aachen.de", "sameAs": "https://orcid.org/0000-0001-8812-7185", "affiliation": "RWTH Aachen University, Germany" }, { "@type": "Person", "name": "Naaf, Matthias", "givenName": "Matthias", "familyName": "Naaf", "email": "mailto:naaf@logic.rwth-aachen.de", "sameAs": "https://orcid.org/0000-0002-1099-5713", "affiliation": "RWTH Aachen University, Germany" } ], "copyrightYear": "2024", "creativeWorkStatus": "Published", "inLanguage": "en-US", "identifier": "https://doi.org/10.4230/OASIcs.Tannen.3", "publisher": { "@type": "Organization", "name": "Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik", "alternateName": [ "Schloss Dagstuhl - Leibniz Center for Informatics", "Schloss Dagstuhl - LZI GmbH" ], "identifier": "https://ror.org/00k4h2615", "sameAs": [ "https://isni.org/isni/0000000100093196", "https://www.dagstuhl.de", "https://de.wikipedia.org/wiki/Leibniz-Zentrum_f%C3%BCr_Informatik" ], "department": { "@type": "Organization", "name": "Dagstuhl Publishing", "logo": { "@type": "ImageObject", "url": "https://www.dagstuhl.de/storage/media/0005/5660/publishing-logo.jpg" }, "contactPoint": { "@type": "ContactPoint", "contactType": "customer support", "email": "mailto:publishing@dagstuhl.de", "url": "https://www.dagstuhl.de/en/publishing/team" } }, "contactPoint": { "@type": "ContactPoint", "contactType": "customer support", "email": "mailto:lzi@dagstuhl.de", "url": "https://www.dagstuhl.de/en/institute/team" } }, "citation": [ "https://doi.org/10.4230/LIPIcs.CSL.2021.17", "https://doi.org/10.1145/1376916.1376954", "https://doi.org/10.1561/1900000068", "https://arxiv.org/abs/1712.01980", "https://doi.org/10.2140/moscow.2020.9.203", "https://doi.org/10.1145/1265530.1265535", "https://doi.org/10.1145/3034786.3056125", "https://doi.org/10.1007/BF02485815", "https://doi.org/10.1090/S0002-9939-1979-0524290-9" ], "pageStart": "3:1", "pageEnd": "3:26", "accessMode": "textual", "accessModeSufficient": "textual", "thumbnailUrl": "https://drops.dagstuhl.de/storage/01oasics/oasics-vol119-tannens-festschrift/thumbnails/OASIcs.Tannen.3/OASIcs.Tannen.3.png", "potentialAction": { "@type": "ReadAction", "target": { "@type": "EntryPoint", "urlTemplate": "https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Tannen.3", "actionPlatform": [ "https://schema.org/DesktopWebPlatform", "https://schema.org/AndroidPlatform", "https://schema.org/IOSPlatform" ] } }, "isPartOf": { "@type": "PublicationVolume", "@id": "https://drops.dagstuhl.de/entities/volume/OASIcs-volume-119", "url": "https://drops.dagstuhl.de/entities/volume/OASIcs-volume-119", "volumeNumber": 119, "name": "The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen", "dateCreated": "2024-06-07", "datePublished": "2024-06-07", "editor": [ { "@type": "Person", "name": "Amarilli, Antoine", "givenName": "Antoine", "familyName": "Amarilli", "email": "mailto:a3nm@a3nm.net", "sameAs": "https://orcid.org/0000-0002-7977-4441", "affiliation": "T\u00e9l\u00e9com Paris, France" }, { "@type": "Person", "name": "Deutsch, Alin", "givenName": "Alin", "familyName": "Deutsch", "email": "mailto:abdeutsch@ucsd.edu", "affiliation": "University of California, San Diego, USA" } ], "isAccessibleForFree": true, "publisher": { "@type": "Organization", "name": "Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik", "alternateName": [ "Schloss Dagstuhl - Leibniz Center for Informatics", "Schloss Dagstuhl - LZI GmbH" ], "identifier": "https://ror.org/00k4h2615", "sameAs": [ "https://isni.org/isni/0000000100093196", "https://www.dagstuhl.de", "https://de.wikipedia.org/wiki/Leibniz-Zentrum_f%C3%BCr_Informatik" ], "department": { "@type": "Organization", "name": "Dagstuhl Publishing", "logo": { "@type": "ImageObject", "url": "https://www.dagstuhl.de/storage/media/0005/5660/publishing-logo.jpg" }, "contactPoint": { "@type": "ContactPoint", "contactType": "customer support", "email": "mailto:publishing@dagstuhl.de", "url": "https://www.dagstuhl.de/en/publishing/team" } }, "contactPoint": { "@type": "ContactPoint", "contactType": "customer support", "email": "mailto:lzi@dagstuhl.de", "url": "https://www.dagstuhl.de/en/institute/team" } }, "isPartOf": { "@type": "BookSeries", "url": "https://drops.dagstuhl.de/entities/series/OASIcs", "name": "Open Access Series in Informatics", "issn": "2190-6807", "isAccessibleForFree": true, "publisher": { "@type": "Organization", "name": "Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik", "alternateName": [ "Schloss Dagstuhl - Leibniz Center for Informatics", "Schloss Dagstuhl - LZI GmbH" ], "identifier": "https://ror.org/00k4h2615", "sameAs": [ "https://isni.org/isni/0000000100093196", "https://www.dagstuhl.de", "https://de.wikipedia.org/wiki/Leibniz-Zentrum_f%C3%BCr_Informatik" ], "department": { "@type": "Organization", "name": "Dagstuhl Publishing", "logo": { "@type": "ImageObject", "url": "https://www.dagstuhl.de/storage/media/0005/5660/publishing-logo.jpg" }, "contactPoint": { "@type": "ContactPoint", "contactType": "customer support", "email": "mailto:publishing@dagstuhl.de", "url": "https://www.dagstuhl.de/en/publishing/team" } }, "contactPoint": { "@type": "ContactPoint", "contactType": "customer support", "email": "mailto:lzi@dagstuhl.de", "url": "https://www.dagstuhl.de/en/institute/team" } }, "hasPart": "https://drops.dagstuhl.de/entities/volume/OASIcs-volume-119" } } } } </script> <link rel="alternate" type="application/xml" title="Semiring Provenance in the Infinite / XML" href="https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Tannen.3/metadata/xml"> <link rel="alternate" type="application/x-bibtex" title="Semiring Provenance in the Infinite / BibTeX" href="https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Tannen.3/metadata/bibtex/download"> <link rel="alternate" type="application/ld+json" title="Semiring Provenance in the Infinite / Schema.org" href="https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Tannen.3/metadata/schema-org"> <link rel="alternate" type="application/xml" title="Semiring Provenance in the Infinite / OAI-DublinCore" href="/oai/?verb=GetRecord&metadataPrefix=oai_dc&identifier=20099"> <title>Semiring Provenance in the Infinite</title> <link rel="icon" href="https://drops.dagstuhl.de/favicon.ico"> <link rel="stylesheet" href="https://drops.dagstuhl.de/css/app.css?drops-core-2025-01-23.1"> </head> <body> <nav class="navbar main fixed-top navbar-expand-lg navbar-light bg-light"> <div class="container-fluid"> <a class="navbar-brand" href="https://www.dagstuhl.de"> <img class="lzi-logo" src="https://drops.dagstuhl.de/images/LZI-Logo.jpg" width="84" height="62" alt="Schloss Dagstuhl - LZI - Logo"> </a> <button class="navbar-toggler" type="button" data-bs-toggle="collapse" data-bs-target="#navbarSupportedContent" aria-controls="navbarSupportedContent" aria-expanded="false" aria-label="Toggle navigation"> <span class="navbar-toggler-icon"></span> </button> <div class="collapse navbar-collapse" id="navbarSupportedContent"> <ul class="navbar-nav me-auto mb-2 mb-lg-0"> <li class="nav-item" style="white-space: nowrap"> <a class="nav-link" href="https://drops.dagstuhl.de"> <i class="bi bi-house large-icon"></i> DROPS </a> </li> <li class="nav-item dropdown"> <a class="nav-link dropdown-toggle" href="#" id="navbarDropdownSeries" role="button" data-bs-toggle="dropdown" aria-expanded="false"> <i class="bi bi-journals large-icon"></i> Series </a> <ul class="dropdown-menu" aria-labelledby="navbarDropdown"> <li><a class="dropdown-item" href="https://drops.dagstuhl.de/entities/series/LIPIcs"> LIPIcs – Leibniz International Proceedings in Informatics </a> </li> <li><a class="dropdown-item" href="https://drops.dagstuhl.de/entities/series/OASIcs"> OASIcs – Open Access Series in Informatics </a> </li> <li><a class="dropdown-item" href="https://drops.dagstuhl.de/entities/series/DFU"> Dagstuhl Follow-Ups </a> </li> <li><a class="dropdown-item" href="https://drops.dagstuhl.de/entities/series/DagAnnRep"> Schloss Dagstuhl Jahresbericht </a> </li> <li class="dropdown-divider"></li> <li> <a class="dropdown-item" href="/#discontinued-series">Discontinued Series</a> </li> </ul> </li> <li class="nav-item dropdown"> <a class="nav-link dropdown-toggle" href="#" id="navbarDropdownJournals" role="button" data-bs-toggle="dropdown" aria-expanded="false" data-fix-width=" JournalsXXXXX "> <i class="bi bi-journal large-icon"></i> Journals </a> <ul class="dropdown-menu" aria-labelledby="navbarDropdown"> <li><a class="dropdown-item" href="https://drops.dagstuhl.de/entities/journal/DARTS"> DARTS – Dagstuhl Artifacts Series </a> </li> <li><a class="dropdown-item" href="https://drops.dagstuhl.de/entities/journal/DagRep"> Dagstuhl Reports </a> </li> <li><a class="dropdown-item" href="https://drops.dagstuhl.de/entities/journal/DagMan"> Dagstuhl Manifestos </a> </li> <li><a class="dropdown-item" href="https://drops.dagstuhl.de/entities/journal/LITES"> LITES – Leibniz Transactions on Embedded Systems </a> </li> <li><a class="dropdown-item" href="https://drops.dagstuhl.de/entities/journal/TGDK"> TGDK – Transactions on Graph Data and Knowledge </a> </li> </ul> </li> <li class="nav-item dropdown"> <a class="nav-link dropdown-toggle" href="#" id="navbarDropdownConferences" role="button" data-bs-toggle="dropdown" aria-expanded="false"> <i class="bi bi-people large-icon"></i> Conferences </a> <ul class="dropdown-menu conference-dropdown" aria-labelledby="navbarDropdown"> <div class="row"> <div class="col-sm-4 nav-conference-col"> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/AFT"> AFT </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/AIB"> AIB </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/AofA"> AofA </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/APPROX"> APPROX </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/ATMOS"> ATMOS </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/CALCO"> CALCO </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/CCC"> CCC </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/CONCUR"> CONCUR </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/COSIT"> COSIT </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/CP"> CP </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/CPM"> CPM </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/CSL"> CSL </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/DISC"> DISC </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/DITAM"> DITAM </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/DNA"> DNA </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/ECOOP"> ECOOP </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/ECRTS"> ECRTS </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/ESA"> ESA </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/FAB"> FAB </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/FMBC"> FMBC </a> </li> </div> <div class="col-sm-4 nav-conference-col"> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/FORC"> FORC </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/FSCD"> FSCD </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/FSTTCS"> FSTTCS </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/FUN"> FUN </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/GD"> GD </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/GIScience"> GIScience </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/ICALP"> ICALP </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/ICDT"> ICDT </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/ICPEC"> ICPEC </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/IPEC"> IPEC </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/iPMVM"> iPMVM </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/ISAAC"> ISAAC </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/ITC"> ITC </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/ITCS"> ITCS </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/ITP"> ITP </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/LDK"> LDK </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/MFCS"> MFCS </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/Microservices"> Microservices </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/NG-RES"> NG-RES </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/OPODIS"> OPODIS </a> </li> </div> <div class="col-sm-4 nav-conference-col"> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/PARMA"> PARMA </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/RANDOM"> RANDOM </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/SAND"> SAND </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/SAT"> SAT </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/SEA"> SEA </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/SLATE"> SLATE </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/SNAPL"> SNAPL </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/SoCG"> SoCG </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/STACS"> STACS </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/SWAT"> SWAT </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/TIME"> TIME </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/Tokenomics"> Tokenomics </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/TQC"> TQC </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/TYPES"> TYPES </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/WABI"> WABI </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/WCET"> WCET </a> </li> </div> </div> </ul> </li> <li class="nav-item dropdown"> <a class="nav-link dropdown-toggle" href="#" id="navbarDropdownArtifacts" role="button" data-bs-toggle="dropdown" aria-expanded="false"> <i class="bi bi-braces-asterisk large-icon"></i> Artifacts </a> <ul class="dropdown-menu" aria-labelledby="navbarDropdown"> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/collection/supplementary-materials"> Supplementary Materials (Software, Datasets, ...) </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/collection/dblp"> dblp Artifacts </a> </li> <li class="dropdown-divider"></li> <li> <a class="dropdown-item" href="/entities/journal/DARTS"> DARTS (Evaluated Artifacts) </a> </li> </ul> </li> </ul> <form class="navbar-search d-flex" action="https://drops.dagstuhl.de/search" method="post"> <input type="hidden" name="_token" value="FLbkycuwsydVWiuEBSSgvjb2rpMIbs9eI54ns0Vp" autocomplete="off"> <div class="input-group"> <input class="form-control" type="search" placeholder="Search" aria-label="Search" name="term" autocomplete="off" maxlength="600"> <button class="btn btn-outline-success" type="submit"> <i class="bi bi-search" style="color: #000"></i> </button> </div> </form> <ul class="navbar-nav nav-metadata"> <li class="nav-item dropdown"> <a class="nav-link dropdown-toggle" id="navbarDropdownMetadata" role="button" data-bs-toggle="dropdown" aria-expanded="false"> <i class="bi bi-database-down large-icon"></i><span class="nav-text-metadata">Metadata Export</span> </a> <ul class="dropdown-menu dropdown-metadata" aria-labelledby="navbarDropdownMetadata"> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/metadata">Metadata Export</a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/oai?verb=Identify" target="_blank">OAI Interface</a> </li> </ul> </li> </ul> </div> </div> </nav> <div id="app" data-release="drops-core-2025-01-23.1" class="container "> <div id="_top-of-page"></div> <div class="fixed-search-button"><i class="bi bi-search"></i></div> <div class="document-details"> <section class="mt-3 mb-5 title"> <div class="entity-type document"> <div class="row"> <div class="col-lg-3 entity-type-name"> <i class="bi bi-file-earmark"></i> Document <img src="https://drops.dagstuhl.de/images/open-access-logo.png" width="80" alt="Open Access Logo" style="transform: translate(1em, -0.2em);"> </div> <div class="col-lg-9"> <input id="doi" type="text" style="position: fixed; top: -50vh" value="https://doi.org/10.4230/OASIcs.Tannen.3"> <div class="sharing-section"> <span class="permalink"> <span> <code><span class="hide-mobile">https://doi.org/</span>10.4230/OASIcs.Tannen.3</code> <span class="btn btn-clipboard copy-to-clipboard" title="Copy to clipboard" data-selector="doi"> <i class="bi bi-clipboard" aria-hidden="true"></i> <i class="bi bi-check -hidden" aria-hidden="true"></i> </span> </span> </span> <span class="sharing-buttons"> <a class="btn sharing-btn facebook" href="https://facebook.com/sharer/sharer.php?u=https%3A%2F%2Fdoi.org%2F10.4230%2FOASIcs.Tannen.3" target="_blank" rel="noopener" aria-hidden="true"> <i class="bi bi-facebook"></i> </a> <a class="btn sharing-btn reddit" href="https://www.reddit.com/submit?url=https%3A%2F%2Fdoi.org%2F10.4230%2FOASIcs.Tannen.3&title=Semiring+Provenance+in+the+Infinite" target="_blank" rel="noopener" aria-hidden="true"> <i class="bi bi-reddit"></i> </a> <a class="btn sharing-btn twitter" href="https://twitter.com/intent/tweet/?text=Semiring+Provenance+in+the+Infinite&url=https%3A%2F%2Fdoi.org%2F10.4230%2FOASIcs.Tannen.3" target="_blank" rel="noopener" aria-hidden="true"> <svg xmlns="http://www.w3.org/2000/svg" width="16" height="16" fill="currentColor" class="bi bi-twitter-x" viewBox="0 0 16 16"> <path d="M12.6.75h2.454l-5.36 6.142L16 15.25h-4.937l-3.867-5.07-4.425 5.07H.316l5.733-6.57L0 .75h5.063l3.495 4.633L12.601.75Zm-.86 13.028h1.36L4.323 2.145H2.865l8.875 11.633Z"/> </svg> </a> <a class="btn sharing-btn email" href="mailto:?subject=Semiring+Provenance+in+the+Infinite&body=https%3A%2F%2Fdoi.org%2F10.4230%2FOASIcs.Tannen.3" target="_self" rel="noopener" aria-hidden="true"> <svg xmlns="http://www.w3.org/2000/svg" width="16" height="16" viewBox="0 0 24 24" fill="currentColor"> <path d="M22 4H2C.9 4 0 4.9 0 6v12c0 1.1.9 2 2 2h20c1.1 0 2-.9 2-2V6c0-1.1-.9-2-2-2zM7.25 14.43l-3.5 2c-.08.05-.17.07-.25.07-.17 0-.34-.1-.43-.25-.14-.24-.06-.55.18-.68l3.5-2c.24-.14.55-.06.68.18.14.24.06.55-.18.68zm4.75.07c-.1 0-.2-.03-.27-.08l-8.5-5.5c-.23-.15-.3-.46-.15-.7.15-.22.46-.3.7-.14L12 13.4l8.23-5.32c.23-.15.54-.08.7.15.14.23.07.54-.16.7l-8.5 5.5c-.08.04-.17.07-.27.07zm8.93 1.75c-.1.16-.26.25-.43.25-.08 0-.17-.02-.25-.07l-3.5-2c-.24-.13-.32-.44-.18-.68s.44-.32.68-.18l3.5 2c.24.13.32.44.18.68z"/> </svg> </a> </span> <span class="sharing-buttons"> <span class="dropdown"> <a class="btn sharing-btn metadata dropdown-toggle" href="#" role="button" data-bs-toggle="dropdown" aria-expanded="false"><i class="bi bi-download"></i></a> <ul class="dropdown-menu dropdown-menu-end"> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Tannen.3/metadata/xml"> Export XML </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Tannen.3/metadata/acm-xml"> Export ACM-XML </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Tannen.3/metadata/doaj-xml"> Export DOAJ-XML </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Tannen.3/metadata/schema-org"> Export Schema.org </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Tannen.3/metadata/bibtex"> Export BibTeX </a> </li> </ul> </span> </span> </div> </div> </div> </div> <hr> <h1>Semiring Provenance in the Infinite</h1> <h3 class="mt-2 authors"> Authors <a href="#author-details" style="font-size: 0.8em; padding-right: 1em"><i class="bi bi-info-circle"></i></a> <span class="author"> <a href="https://drops.dagstuhl.de/search/documents?author=Brinke, Sophie" class="name">Sophie Brinke</a> <a href="https://orcid.org/0009-0005-2865-0069"><img class="orcid-logo" src="https://drops.dagstuhl.de/images/orcid.png" alt="ORCID-Logo"></a>, </span> <span class="author"> <a href="https://drops.dagstuhl.de/search/documents?author=Grädel, Erich" class="name">Erich Grädel</a> <a href="https://orcid.org/0000-0002-8950-9991"><img class="orcid-logo" src="https://drops.dagstuhl.de/images/orcid.png" alt="ORCID-Logo"></a>, </span> <span class="author"> <a href="https://drops.dagstuhl.de/search/documents?author=Mrkonjić, Lovro" class="name">Lovro Mrkonjić</a> <a href="https://orcid.org/0000-0001-8812-7185"><img class="orcid-logo" src="https://drops.dagstuhl.de/images/orcid.png" alt="ORCID-Logo"></a>, </span> <span class="author"> <a href="https://drops.dagstuhl.de/search/documents?author=Naaf, Matthias" class="name">Matthias Naaf</a> <a href="https://orcid.org/0000-0002-1099-5713"><img class="orcid-logo" src="https://drops.dagstuhl.de/images/orcid.png" alt="ORCID-Logo"></a> </span> </h3> <hr> <ul class="mt-4"> <li> <span style="margin-right: 10px; ">Part of:</span> <span style="white-space: nowrap"> <i class="bi bi-book-half"></i> Volume: </span> <a href="https://drops.dagstuhl.de/entities/volume/OASIcs-volume-119">The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen (Tannen's Festschrift)</a> <br> <span style="margin-right: 10px; visibility: hidden;">Part of:</span> <span style="white-space: nowrap"> <i class="bi bi-journals"></i> Series: </span> <a href="https://drops.dagstuhl.de/entities/series/OASIcs">Open Access Series in Informatics (OASIcs)</a> <br> <span style="margin-right: 10px; visibility: hidden;">Part of:</span> <span style="white-space: nowrap"> <i class="bi bi-people"></i> Conference: </span> <a href="https://drops.dagstuhl.de/entities/conference/Tannen">Festschrift Val Tannen </a> </li> <li class="mt-2">License:   <a href="https://creativecommons.org/licenses/by/4.0/legalcode"> <img class="license-logo" src="https://drops.dagstuhl.de/images/cc-by.png" alt="CC-BY Logo"> Creative Commons Attribution 4.0 International license </a> </li> <li>Publication Date: 2024-06-07 </li> </ul> <hr> </section> <a class="fixed-pdf-button" href="https://drops.dagstuhl.de/storage/01oasics/oasics-vol119-tannens-festschrift/OASIcs.Tannen.3/OASIcs.Tannen.3.pdf"><i class="bi bi-file-earmark-pdf-fill" style="color:red"></i> PDF </a> <div class="row mt-2"> <div class="col-lg-4 mt-2"> <section class="thumbnail"> <a href="https://drops.dagstuhl.de/storage/01oasics/oasics-vol119-tannens-festschrift/OASIcs.Tannen.3/OASIcs.Tannen.3.pdf"><img src="https://drops.dagstuhl.de/storage/01oasics/oasics-vol119-tannens-festschrift/thumbnails/OASIcs.Tannen.3/OASIcs.Tannen.3.png" alt="Thumbnail PDF"></a> </section> <section class="files mt-5"> <h2>File</h2> <div class="content"> <div> <a href="https://drops.dagstuhl.de/storage/01oasics/oasics-vol119-tannens-festschrift/OASIcs.Tannen.3/OASIcs.Tannen.3.pdf"><i class="bi bi-file-earmark-pdf-fill" style="color:red"></i> OASIcs.Tannen.3.pdf</a> <ul> <li>Filesize: 0.72 MB</li> <li>26 pages</li> </ul> </div> </div> </section> <section class="identifiers mt-3"> <h2>Document Identifiers</h2> <div class="content"> <ul> <li><b>DOI:</b> <a href="https://doi.org/10.4230/OASIcs.Tannen.3">10.4230/OASIcs.Tannen.3</a></li> <li><b>URN:</b> <a href="https://nbn-resolving.org/process-urn-form?identifier=urn:nbn:de:0030-drops-200997&verb=FULL">urn:nbn:de:0030-drops-200997</a></li> </ul> </div> </section> <section class="authors mt-3" id="author-details"> <h2>Author Details</h2> <div class="author person-details"> <div> <i class="bi bi-person-fill"></i> <span class="name"><b>Sophie Brinke</b></span> <a href="https://orcid.org/0009-0005-2865-0069"><img class="orcid-logo" src="https://drops.dagstuhl.de/images/orcid.png" alt="ORCID-Logo"></a> <a href="mailto:brinke@logic.rwth-aachen.de"><i class="bi bi-envelope"></i></a> <a href="https://drops.dagstuhl.de/search/documents?author=Brinke, Sophie"><small><i class="bi bi-search"></i></small></a> </div> <ul> <li class="affiliation">RWTH Aachen University, Germany </li> </ul> </div> <div class="author person-details"> <div> <i class="bi bi-person-fill"></i> <span class="name"><b>Erich Grädel</b></span> <a href="https://orcid.org/0000-0002-8950-9991"><img class="orcid-logo" src="https://drops.dagstuhl.de/images/orcid.png" alt="ORCID-Logo"></a> <a href="mailto:graedel@logic.rwth-aachen.de"><i class="bi bi-envelope"></i></a> <a href="https://drops.dagstuhl.de/search/documents?author=Grädel, Erich"><small><i class="bi bi-search"></i></small></a> </div> <ul> <li class="affiliation">RWTH Aachen University, Germany </li> </ul> </div> <div class="author person-details"> <div> <i class="bi bi-person-fill"></i> <span class="name"><b>Lovro Mrkonjić</b></span> <a href="https://orcid.org/0000-0001-8812-7185"><img class="orcid-logo" src="https://drops.dagstuhl.de/images/orcid.png" alt="ORCID-Logo"></a> <a href="mailto:mrkonjic@logic.rwth-aachen.de"><i class="bi bi-envelope"></i></a> <a href="https://drops.dagstuhl.de/search/documents?author=Mrkonjić, Lovro"><small><i class="bi bi-search"></i></small></a> </div> <ul> <li class="affiliation">RWTH Aachen University, Germany </li> </ul> </div> <div class="author person-details"> <div> <i class="bi bi-person-fill"></i> <span class="name"><b>Matthias Naaf</b></span> <a href="https://orcid.org/0000-0002-1099-5713"><img class="orcid-logo" src="https://drops.dagstuhl.de/images/orcid.png" alt="ORCID-Logo"></a> <a href="mailto:naaf@logic.rwth-aachen.de"><i class="bi bi-envelope"></i></a> <a href="https://drops.dagstuhl.de/search/documents?author=Naaf, Matthias"><small><i class="bi bi-search"></i></small></a> </div> <ul> <li class="affiliation">RWTH Aachen University, Germany </li> </ul> </div> </section> </div> <div class="col-lg-8 mt-2"> <section class="cite-as mt-3"> <h2>Cite As <span class="btn btn-primary btn-xs" style="float: right" data-bs-toggle="modal" data-bs-target="#bibtex-modal">Get BibTex</span></h2> <div class="content"> Sophie Brinke, Erich Grädel, Lovro Mrkonjić, and Matthias Naaf. Semiring Provenance in the Infinite. In The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen. Open Access Series in Informatics (OASIcs), Volume 119, pp. 3:1-3:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) <a href="https://doi.org/10.4230/OASIcs.Tannen.3">https://doi.org/10.4230/OASIcs.Tannen.3</a> </div> <div class="modal fade" id="bibtex-modal" tabindex="-1" aria-labelledby="bibtexModalLabel" aria-hidden="true"> <div class="modal-dialog modal-dialog-centered"> <div class="modal-content"> <div class="modal-header"> <h5 class="modal-title" id="bibtexModalLabel">BibTex</h5> <button type="button" class="btn-close" data-bs-dismiss="modal" aria-label="Close"></button> </div> <div class="modal-body"> <pre class="bibtex">@InProceedings{brinke_et_al:OASIcs.Tannen.3, author = {Brinke, Sophie and Gr\"{a}del, Erich and Mrkonji\'{c}, Lovro and Naaf, Matthias}, title = {{Semiring Provenance in the Infinite}}, booktitle = {The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen}, pages = {3:1--3:26}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-95977-320-1}, ISSN = {2190-6807}, year = {2024}, volume = {119}, editor = {Amarilli, Antoine and Deutsch, Alin}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Tannen.3}, URN = {urn:nbn:de:0030-drops-200997}, doi = {10.4230/OASIcs.Tannen.3}, annote = {Keywords: Semiring semantics, first-order logic, semirings with infinitary operations} }</pre> <div style="overflow: hidden"> <textarea style="position: absolute; top: -400vh" id="bibtex-input">@InProceedings{brinke_et_al:OASIcs.Tannen.3, author = {Brinke, Sophie and Gr\"{a}del, Erich and Mrkonji\'{c}, Lovro and Naaf, Matthias}, title = {{Semiring Provenance in the Infinite}}, booktitle = {The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen}, pages = {3:1--3:26}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-95977-320-1}, ISSN = {2190-6807}, year = {2024}, volume = {119}, editor = {Amarilli, Antoine and Deutsch, Alin}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Tannen.3}, URN = {urn:nbn:de:0030-drops-200997}, doi = {10.4230/OASIcs.Tannen.3}, annote = {Keywords: Semiring semantics, first-order logic, semirings with infinitary operations} }</textarea> </div> </div> <div class="modal-footer"> <button type="button" class="btn btn-secondary" data-bs-dismiss="modal">Close</button> <button type="button" class="btn btn-primary copy-to-clipboard" data-selector="bibtex-input"><i class="bi bi-clipboard"></i> Copy BibTex To Clipboard<span class="bi bi-check -hidden" style="padding-left: 1em; font-weight: bold"></span></button> </div> </div> </div> </div> </section> <section class="abstract"> <h2>Abstract</h2> <pre class="content" style="white-space: -moz-pre-wrap; white-space: -o-pre-wrap; word-wrap: break-word; white-space: pre-wrap;">Semiring provenance evaluates database queries or logical statements not just by true or false but by values in some commutative semiring. This permits to track which combinations of atomic facts are responsible for the truth of a statement, and to derive further information, for instance concerning costs, confidence scores, number of proof trees, or access levels to protected data. The focus of this approach, proposed and developed to a large extent by Val Tannen and his collaborators, has first been on (positive) database query languages, but has later been extended, again in collaboration with Val, to a systematic semiring semantics for first-order logic (and other logical systems), as well as to a method for the strategy analysis of games. So far, semiring provenance has been studied for finite structures. To extend the semiring provenance approach for first-order logic to infinite domains, the semirings need to be equipped with addition and multiplication operators over infinite collections of values. This needs solid algebraic foundations, and we study here the necessary and desirable properties of semirings with infinitary operations to provide a well-defined and informative provenance analysis over infinite domains. We show that, with suitable definitions for such infinitary semiring, large parts of the theory of semiring provenance can be succesfully generalised to infinite structures.</pre> </section> <section class="subject-classifications mt-3"> <h2>Subject Classification</h2> <div class="acm-subject-classifications"> <h5>ACM Subject Classification</h5> <div class="content"> <ul> <li>Theory of computation → Finite Model Theory</li> </ul> </div> </div> <div class="keywords "> <h5>Keywords</h5> <div class="content"> <ul class="list-style-comma"> <li>Semiring semantics</li> <li>first-order logic</li> <li>semirings with infinitary operations</li> </ul> </div> </div> </section> <section class="metrics mt-3"> <h2>Metrics</h2> <div class="content"> <ul> <li> <a href="#" class="btn-statistics" data-entity="document/10.4230/OASIcs.Tannen.3" data-title="Semiring Provenance in the Infinite"> <i class="bi bi-graph-up"></i> Access Statistics </a> </li> <li> Total Accesses (updated on a weekly basis) <div class="stats-total"> <div class="stats total-downloads"> <div class="circle"> <div class="number" data-number="0">0</div> </div> <div class="label">PDF Downloads</div> </div> <div class="stats total-metadata-views"> <div class="circle"> <div class="number" data-number="0">0</div> </div> <div class="label">Metadata Views</div> </div> </div>  </li> </ul> </div> </section> <div class="offcanvas offcanvas-bottom" tabindex="-1" id="statistics-offcanvas" aria-labelledby="statistics-offcanvas"> <div class="offcanvas-header"> <h5 class="offcanvas-title"></h5> <button type="button" class="btn-close text-reset" data-bs-dismiss="offcanvas" aria-label="Close"></button> </div> <div class="offcanvas-body small" data-context=""> <div style="margin-top: 20vh" class="centered-loader"><div class="loader"></div></div> <iframe class="-hidden"></iframe> </div> </div> <section class="references mt-3"> <h2>References</h2> <div class="content"> <ol> <li> <span> K. Dannert, E. Grädel, M. Naaf, and V. Tannen. Semiring provenance for fixed-point logic. In C. Baier and J. Goubault-Larrecq, editors, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), volume 183 of Leibniz International Proceedings in Informatics (LIPIcs), pages 17:1-17:22, Dagstuhl, 2021. URL: <a href="https://doi.org/10.4230/LIPIcs.CSL.2021.17">https://doi.org/10.4230/LIPIcs.CSL.2021.17</a>. </span> </li> <li> <span> J. Foster, T. Green, and V. Tannen. Annotated XML: queries and provenance. In Proceedings of PODS 2008, pages 271-280, 2008. URL: <a href="https://doi.org/10.1145/1376916.1376954">https://doi.org/10.1145/1376916.1376954</a>. </span> </li> <li> <span> B. Glavic. Data provenance. Foundations and Trends in Databases, 9(3-4):209-441, 2021. URL: <a href="https://doi.org/10.1561/1900000068">https://doi.org/10.1561/1900000068</a>. </span> </li> <li> <span> E. Grädel and V. Tannen. Semiring provenance for first-order model checking. arXiv:1712.01980 [cs.LO], 2017. URL: <a href="https://arxiv.org/abs/1712.01980">https://arxiv.org/abs/1712.01980</a>. </span> </li> <li> <span> E. Grädel and V. Tannen. Provenance analysis for logic and games. Moscow Journal of Combinatorics and Number Theory, 9(3):203-228, 2020. Preprint available at https://arxiv.org/abs/1907.08470. URL: <a href="https://doi.org/10.2140/moscow.2020.9.203">https://doi.org/10.2140/moscow.2020.9.203</a>. </span> </li> <li> <span> E. Grädel and V. Tannen. Provenance analysis and semiring semantics for first-order logic. submitted for publication, 2024. <a href="https://scholar.google.com/scholar?hl=en&q=E. Grädel and V. Tannen. Provenance analysis and semiring semantics for first-order logic. submitted for publication, 2024." target="_blank" title="Google Scholar"><img style="opacity: 0.5" src="https://drops.dagstuhl.de/images/google-scholar.dark.16x16.png" alt="Google Scholar"></a> </span> </li> <li> <span> T. Green, G. Karvounarakis, and V. Tannen. Provenance semirings. In Principles of Database Systems PODS, pages 31-40. ACM, 2007. URL: <a href="https://doi.org/10.1145/1265530.1265535">https://doi.org/10.1145/1265530.1265535</a>. </span> </li> <li> <span> T. Green and V. Tannen. The semiring framework for database provenance. In Proceedings of PODS, pages 93-99. ACM, 2017. URL: <a href="https://doi.org/10.1145/3034786.3056125">https://doi.org/10.1145/3034786.3056125</a>. </span> </li> <li> <span> G. Markowsky. Chain-complete posets and directed sets with applications. Algebra universalis, 6(1):53-68, 1976. URL: <a href="https://doi.org/10.1007/BF02485815">https://doi.org/10.1007/BF02485815</a>. </span> </li> <li> <span> G. Markowsky. Free completely distributive lattices. Proceedings of the American Mathematical Society, 74(2):227-228, 1979. URL: <a href="https://doi.org/10.1090/S0002-9939-1979-0524290-9">https://doi.org/10.1090/S0002-9939-1979-0524290-9</a>. </span> </li> <li> <span> M. Naaf. Logic, Semirings, and Fixed Points. PhD thesis, RWTH Aachen University, 2024. Forthcoming. <a href="https://scholar.google.com/scholar?hl=en&q=M. Naaf. Logic, Semirings, and Fixed Points. PhD thesis, RWTH Aachen University, 2024. Forthcoming." target="_blank" title="Google Scholar"><img style="opacity: 0.5" src="https://drops.dagstuhl.de/images/google-scholar.dark.16x16.png" alt="Google Scholar"></a> </span> </li> </ol> </div> </section> </div> </div> </div> </div> <span class="_feedback-button"> <i class="bi bi-question-circle"></i> <span class="text">Questions / Remarks / Feedback</span> </span> <div class="_feedback-form -hidden"> <span class="_feedback-close">X</span> <p>Feedback for Dagstuhl Publishing</p> <div> <textarea class="form-control" name="_feedback"></textarea> <input class="form-control" type="text" name="name" autocomplete="off" placeholder="Name (optional)" maxlength="60"> <input class="form-control" type="email" name="email" autocomplete="off" placeholder="Email (optional)" maxlength="60"> <br> <button class="btn btn-sm btn-default">Send</button> </div> </div> <div class="alert alert-success _feedback-success -hidden"> <span class="glyphicon glyphicon-ok"></span> <h3>Thanks for your feedback!</h3> <div>Feedback submitted</div> <button class="btn btn-white _feedback-done">OK</button> </div> <div class="alert alert-danger _feedback-error -hidden"> <span class="glyphicon glyphicon-remove"></span> <h3>Could not send message</h3> <div>Please try again later or send an <a href="mailto:publishing@dagstuhl.de">E-mail</a></div> <button class="btn btn-white _feedback-done">OK</button> </div> <a class="scroll-up-button -hidden" href="#_top-of-page"> <i class="bi bi-arrow-up-circle"></i> </a> <footer class="page-footer dark"> <div class="container"> <h5>About DROPS</h5> <p>Schloss Dagstuhl - Leibniz Center for Informatics has been operating the Dagstuhl Research Online Publication Server (short: DROPS) since 2004. DROPS enables publication of the latest research findings in a fast, uncomplicated manner, in addition to providing unimpeded, open access to them. All the requisite metadata on each publication is administered in accordance with general guidelines pertaining to online publications (cf. Dublin Core). This enables the online publications to be authorized for citation and made accessible to a wide readership on a permanent basis. Access is free of charge for readers following the open access idea which fosters unimpeded access to scientific publications. </p> <ul style="margin-top: -0.5em"> <li><a href="https://drops.dagstuhl.de/docs/about">More about DROPS</a></li> </ul> </div> <div class="container"> <div class="row"> <div class="col-lg-6"> <h5>Instructions for Authors</h5> <div class="row"> <div class="col-sm-6"> <b>Dagstuhl Series</b><br> <ul> <li><a href="https://submission.dagstuhl.de/series/details/lipics#author">LIPIcs</a></li> <li><a href="https://submission.dagstuhl.de/series/details/oasics#author">OASIcs</a></li> <li><a href="https://submission.dagstuhl.de/series/details/dfu#author">Dagstuhl Follow-Ups</a></li> </ul> </div> <div class="col-sm-6"> <b>Dagstuhl Journals</b><br> <ul> <li><a href="https://submission.dagstuhl.de/series/details/darts#author">DARTS – Dagstuhl Artifacts Series</a></li> <li><a href="https://submission.dagstuhl.de/series/details/dagrep#author">Dagstuhl Reports</a></li> <li><a href="https://submission.dagstuhl.de/series/details/dagman#author">Dagstuhl Manifestos</a></li> <li><a href="https://submission.dagstuhl.de/series/details/lites#author">LITES</a></li> <li><a href="https://submission.dagstuhl.de/series/details/tgdk#author">TGDK – Transactions on Graph Data and Knowledge</a></li> </ul> </div> </div> </div> <div class="col-lg-6"> <h5>Instructions for Editors</h5> <div class="row"> <div class="col-sm-6"> <b>Dagstuhl Series</b><br> <ul> <li><a href="https://submission.dagstuhl.de/series/details/lipics#editor">LIPIcs</a></li> <li><a href="https://submission.dagstuhl.de/series/details/oasics#editor">OASIcs</a></li> <li><a href="https://submission.dagstuhl.de/series/details/dfu#editor">Dagstuhl Follow-Ups</a></li> </ul> </div> <div class="col-sm-6"> <b>Dagstuhl Journals</b><br> <ul> <li><a href="https://submission.dagstuhl.de/series/details/darts#editor">DARTS – Dagstuhl Artifacts Series</a></li> <li><a href="https://submission.dagstuhl.de/series/details/dagrep#editor">Dagstuhl Reports</a></li> <li><a href="https://submission.dagstuhl.de/series/details/dagman#editor">Dagstuhl Manifestos</a></li> <li><a href="https://submission.dagstuhl.de/series/details/lites#editor">LITES</a></li> <li><a href="https://submission.dagstuhl.de/series/details/tgdk#editor">TGDK – Transactions on Graph Data and Knowledge</a></li> </ul> </div> </div> </div> </div> </div> </footer> <div class="copyright"> © 2023-2024 <a href="https://www.dagstuhl.de">Schloss Dagstuhl – LZI GmbH</a> <a href="https://drops.dagstuhl.de/docs/about">About DROPS</a> <a href="https://drops.dagstuhl.de/docs/imprint">Imprint</a> <a href="https://drops.dagstuhl.de/docs/privacy">Privacy</a> <a href="https://www.dagstuhl.de/en/publishing/team">Contact</a> </div> <script type="text/javascript" src="https://drops.dagstuhl.de/js/jquery-3.6.0.min.js"></script> <script type="text/javascript" src="https://drops.dagstuhl.de/js/app.js?drops-core-2025-01-23.1"></script> <script type="text/javascript" src="https://drops.dagstuhl.de/js/popper.min.js"></script> <script type="text/javascript" src="https://drops.dagstuhl.de/js/circle-progress.js"></script> <script type="text/javascript"> $(document).ready(function() { const view = { statsServer: 'https://drops-stats.dagstuhl.de', animationStarted: false, isScrolledIntoView: function (elem) { const rect = elem.getBoundingClientRect(); const elemTop = rect.top; //const elemBottom = rect.bottom; // const elemHeight = rect.height; return (elemTop >= 0) && (elemTop <= window.innerHeight); }, progressCircle: function ($el) { $el.find('.circle').circleProgress({ value: 1, size: 80, fill: { color: '#555' }, animation: { duration: 1200 } }); }, countUp: function($el) { $el.find('.number').each(function() { const $this = $(this); const number = parseInt($this.attr('data-number')); let suffix = ''; if (number > 90000) { $this.text(Math.ceil(number/1000)+' k'); suffix = ' k'; } else if (number > 90000000) { $this.text(Math.ceil(number/1000000)+' m'); suffix = ' m'; } else { $this.text(Math.ceil(number)) } $({ Counter: 0 }).animate({ Counter: $this.text().replace(suffix, '').replace(',', '') }, { duration: 1000, easing: 'swing', step: function() { $this.text(Math.ceil(this.Counter).toString().replace(/\B(?=(\d{3})+(?!\d))/g, ",") + suffix); } }); }); }, checkVisibility: function() { const $container = $('.stats-total'); if (view.isScrolledIntoView($container[0])) { if (!view.animationStarted) { view.animationStarted = true; view.progressCircle($container); setTimeout(function() { view.countUp($container) }, 200); } } }, initialize: function() { $.ajax({ type: 'get', url: view.statsServer + '/api/external/drops2/document/10.4230/OASIcs.Tannen.3/-/stats', success: function (result) { $('.total-downloads .number').attr('data-number', result.total.downloads); $('.total-metadata-views .number').attr('data-number', result.total.clicks); window.addEventListener('scroll', view.checkVisibility); view.checkVisibility(); }, error: function () { $('.total-downloads .number').text(0); $('.total-metadata-views .number').text(0); window.addEventListener('scroll', view.checkVisibility); view.checkVisibility(); } }); } }; view.initialize(); }); </script> <script type="text/javascript"> $(document).ready(function() { const statistics = { statsServer: 'https://drops-stats.dagstuhl.de', showStatistics: function(e) { e.preventDefault(); const $offCanvas = $('#statistics-offcanvas'); const $iframe = $offCanvas.find('iframe'); const $loader = $offCanvas.find('.centered-loader'); $iframe.addClass('-hidden'); $loader.removeClass('-hidden'); $iframe[0].onload = function () { $iframe.removeClass('-hidden'); $loader.addClass('-hidden'); }.bind(this); const modeParameter = ''; const $target = $(e.currentTarget); const entityId = $target.attr('data-entity'); const title = $target.attr('data-title'); const embedUrl = statistics.statsServer + '/embed/external/drops2/' + entityId + modeParameter; let context = $offCanvas.find('.offcanvas-body').attr('data-context'); if (context === title) { context = ''; } if (context !== '') { context += '<br>'; } $offCanvas.find('.offcanvas-title').html(context + '<h2 style="font-weight: bold">' + title + '</h2>'); $offCanvas.offcanvas('show'); $offCanvas.find('iframe').attr('src', embedUrl); return false; }, initialize: function() { $('.btn-statistics').on('click', this.showStatistics); } }; statistics.initialize(); }); </script> <script type="text/javascript"> function _enableFeedback() { var $feedbackButton = $('._feedback-button, .fixed-beta-button'); var $feedbackClose = $('._feedback-close'); var $feedbackForm = $('._feedback-form'); var $feedbackSubmit = $('._feedback-form button'); var $textarea = $feedbackForm.find('textarea'); var $feedbackSuccess = $('._feedback-success'); var $feedbackError = $('._feedback-error'); var $feedbackDoneButton = $('._feedback-done'); $feedbackButton.addClass('_show'); $feedbackButton.on('click', function () { $feedbackButton.addClass('-hidden'); $feedbackForm.removeClass('-hidden'); $textarea.focus(); }); $feedbackClose.on('click', function () { $feedbackSuccess.addClass('-hidden'); $feedbackForm.addClass('-hidden'); $feedbackButton.removeClass('-hidden'); }); $feedbackDoneButton.on('click', function () { $feedbackError.addClass('-hidden'); $feedbackSuccess.addClass('-hidden'); $feedbackForm.addClass('-hidden'); $feedbackButton.removeClass('-hidden'); }); $feedbackSubmit.on('click', function () { var message = $textarea.val(); if (message === undefined) { message = ''; } if (message.trim() !== '') { $.ajax({ url: '/api/v1/feedback', type: 'post', data: { content: message, context: window.location.href, name: $('input[name="name"]').val(), email: $('input[name="email"]').val(), }, success: function (result) { if (result === 'success') { $textarea.val(''); $feedbackSuccess.removeClass('-hidden'); } else { $feedbackError.removeClass('-hidden'); } }, error: function () { $feedbackError.removeClass('-hidden'); } }); } }); } var _defer_counter = 0; function _defer(method) { if (window.jQuery) { method(); } else { if (_defer_counter < 20) { setTimeout(function () { _defer(method); console.log(_defer_counter); _defer_counter++; }, 500); } } } setTimeout(function() { _defer(_enableFeedback); }, 1000); </script> <script type="text/javascript"> $(document).ready(function() { const app = { maxScrollPos: window.innerWidth < 500 ? 100 // mobile : 400, // desktop $el : { navbarSearch: $('nav .navbar-search'), fixedSearchButton: $('.fixed-search-button'), copyToClipboard: $('.copy-to-clipboard') }, methods: { hideMenuOnScroll: function(scrollPos) { const $menu = $('nav.navbar.main'); const $stickySearch = $('.search.sticky'); const $banner = $('#_banner'); const $fixedSearchButton = $('.fixed-search-button'); if (scrollPos > app.maxScrollPos) { $menu.addClass('-hide'); $banner.addClass('-hide'); $stickySearch.addClass('-top'); $fixedSearchButton.addClass('-show'); } else { app.methods.showMenu(null, false); } }, showMenu: function(e, focus) { const $menu = $('nav.navbar.main'); const $stickySearch = $('.search.sticky'); const $banner = $('#_banner'); const $fixedSearchButton = $('.fixed-search-button'); $menu.removeClass('-hide'); $banner.removeClass('-hide'); $stickySearch.removeClass('-top'); $fixedSearchButton.removeClass('-show'); if (focus !== false) { $('.navbar-search').find('input[name="term"]').focus(); } }, showUpLinkOnScroll: function(scrollPos) { const $upLink = $('.scroll-up-button'); if (scrollPos > app.maxScrollPos) { $upLink.removeClass('-hidden'); } else { $upLink.addClass('-hidden'); } }, scrollHandler: function() { const scrollPos = $(document).scrollTop(); app.methods.hideMenuOnScroll(scrollPos); app.methods.showUpLinkOnScroll(scrollPos); }, copyToClipboard: function(e) { e.preventDefault(); const $current = $(e.currentTarget); // console.log($current.attr('data-selector')); const element = $('#'+$current.attr('data-selector'))[0]; console.log(element); element.select(); document.execCommand("copy"); const $success = $current.find('.bi-check'); $success.removeClass('-hidden'); setTimeout(function() { $success.addClass('-hidden'); }, 1000); }, initTooltips: function() { const tooltipTriggerList = [].slice.call(document.querySelectorAll('[data-bs-toggle="tooltip"]')) const tooltipList = tooltipTriggerList.map(function (tooltipTriggerEl) { return new bootstrap.Tooltip(tooltipTriggerEl) }); }, expandSearch: function() { app.$el.navbarSearch.addClass('expanded'); }, collapseSearch: function(e) { if (!$(e.currentTarget).is('button.btn-outline-success')) { app.$el.navbarSearch.removeClass('expanded'); } }, initDeepLinksTabs: function() { app.methods.initTabLinks(); const innerAnchors =[]; $('.tab-pane').find('[id]').each(function() { innerAnchors.push(this.getAttribute('id')); }); const anchors = []; $('a[role="tab"]').each(function() { anchors.push($(this).attr('aria-controls')); }); innerAnchors.forEach(function(anchor) { if ($('#'+anchor).length > 0) { anchors.push(anchor); } }); if (anchors.length === 0) { return; } let selectedAnchor = window.location.hash.substring(1); if (anchors.indexOf(selectedAnchor) === -1) { $('#publications-tab').tab('show'); window.scrollTo(0,0); return; } if (selectedAnchor !== 'publications') { const innerAnchorIndex = innerAnchors.indexOf(selectedAnchor); // anchor sits inside tab -> open the tab first, then scroll to anchor if (innerAnchorIndex > -1) { const $tab = $('#'+selectedAnchor).closest('.tab-pane'); console.log($tab); try { $('#'+$tab.attr('id')+'-tab').tab('show'); } catch (e) { } setTimeout(function () { $('#' + selectedAnchor)[0].scrollIntoView(); }, 800); } else { try { $('#' + selectedAnchor + '-tab').tab('show'); } catch (e) { } window.scrollTo(0, 0); } } }, initTabLinks: function() { $('[data-tab-link]').on('click', function(e) { e.preventDefault(); const $target = $(e.currentTarget); document.location.href = $target.attr('href'); document.location.reload(); }); }, }, initialize: function() { $(window).on('scroll', app.methods.scrollHandler); $(window).on('scroll-to-top', function() { window.scrollTo(0,0) }); $(document).trigger('scroll'); // set correct status for scroll-related parts (navbar/back-to-top) on page reload app.$el.copyToClipboard.on('click', app.methods.copyToClipboard); app.$el.fixedSearchButton.on('click', app.methods.showMenu); app.$el.navbarSearch.find('input').on('click', app.methods.expandSearch) app.$el.navbarSearch.find('input').on('blur', app.methods.collapseSearch); app.methods.initTooltips(); app.methods.initDeepLinksTabs(); } }; app.initialize(); }); </script> </body> </html>

CINXE.COM

Semiring Provenance in the Infinite