Certified Graph View Maintenance with Regular Datalog

DOI10.1017/S1471068418000224MaRDI QIDQ4559800zbMATH OpenOpenAlexWikidataFDO

Authors Angela Bonifati, Stefania Dumbrava, Emilio Jesús Gallego Arias

Publication date 4 December 2018

Published in Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1804.10565

zbMATH Keywords

finite semanticsgraph queriesgraph viewsincremental maintenanceregular Datalogtheorem proving

Mathematics Subject Classification ID

Logic programming (68N17) Database theory (68P15) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Abstract: We employ the Coq proof assistant to develop a mechanically-certified framework for evaluating graph queries and incrementally maintaining materialized graph instances, also called views. The language we use for defining queries and views is Regular Datalog (RD) -- a notable fragment of non-recursive Datalog that can express complex navigational queries, with transitive closure as native operator. We first design and encode the theory of RD and then mechanize a RD-specific evaluation algorithm capable of fine-grained, incremental graph view computation, which we prove sound with respect to the declarative RD semantics. By using the Coq extraction mechanism, we test an Ocaml version of the verified engine on a set of preliminary benchmarks. Our development is particularly focused on leveraging existing verification and notational techniques to: a) define mechanized properties that can be easily understood by logicians and database researchers and b) attain formal verification with limited effort. Our work is the first step towards a unified, machine-verified, formal framework for dynamic graph query languages and their evaluation engines. This paper is under consideration for acceptance in TPLP.

Recommendations

• Datalog Rewritings of Regular Path Queries using Views
• Regular queries on graph databases
• Regular queries on graph databases
• Verification of evolving graph-structured data under expressive path constraints
• Maintenance of datalog materialisations revisited
• Managing Change in Graph-Structured Data Using Description Logics
• Path logics for querying graphs: combining expressiveness and efficiency
• Graph grammars for querying graph-like data
• Schema Compliant Consistency Management via Triple Graph Grammars and Integer Linear Programming
• Schema compliant consistency management via triple graph grammars and integer linear programming

Cites work

• A Coq formalization of the relational data model
• A machine-checked proof of the odd order theorem
• Certifying standard and stratified Datalog inference engines in SSReflect
• Extraction in Coq: An Overview
• scientific article; zbMATH DE number 784042 (Why is no real title available?)
• scientific article; zbMATH DE number 839556 (Why is no real title available?)
• On the computational complexity of dynamic graph problems
• Regular queries on graph databases

Cited in

(5)

• Certifying standard and stratified Datalog inference engines in SSReflect
• A Coq formalisation of SQL's execution engines
• Toward a verified relational database management system
• Verifying Datalog reasoning with Lean
• Stratified Datalog and Program Analysis

Describes a project that uses

Uses Software

• Coq
• OCaml
• OEuf
• Datalog
• HoTTSQL
• gMark

This page was built for publication: Certified Graph View Maintenance with Regular Datalog

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4559800)