Certified Graph View Maintenance with Regular Datalog

DOI10.1017/S1471068418000224zbMath1451.68086arXiv1804.10565OpenAlexW2963205449MaRDI QIDQ4559800

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

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

theorem provingincremental maintenancegraph queriesfinite semanticsgraph viewsregular Datalog

Mathematics Subject Classification ID

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

Uses Software

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

Cites Work

• On the computational complexity of dynamic graph problems
• Certifying standard and stratified Datalog inference engines in SSReflect
• Regular queries on graph databases
• Extraction in Coq: An Overview
• A Machine-Checked Proof of the Odd Order Theorem
• A Coq Formalization of the Relational Data Model
• Unnamed Item
• Unnamed Item

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