Reasoning formally about database queries and updates

DOI10.1007/978-3-030-30942-8_33zbMATH Open1539.68091MaRDI QIDQ6535969FDOQ6535969

Authors: Jon Haël Brenas, Rachid Echahed, Martin Strecker 

Publication date: 14 March 2024

Recommendations

• On specifying database updates
• An axiom system for database transactions
• Database Theory - ICDT 2005
• Specification and verification of database dynamics
• scientific article; zbMATH DE number 3874667

zbMATH Keywords

modal logicprogram verificationautomated theorem provinggraph transformations

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Database theory (68P15) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Modal languages and bounded fragments of predicate logic
• Concrete semantics. With Isabelle/HOL
• Foundations of XML processing. The tree-automata approach.
• On the Restraining Power of Guards
• Title not available (Why is that?)
• On the automated verification of web applications with embedded SQL
• Frontiers of tractability for typechecking simple XML transformations
• Weakest Preconditions for High-Level Programs
• Verifiable properties of database transactions
• Integrity checking and maintenance in relational and deductive databases and beyond
• Managing Change in Graph-Structured Data Using Description Logics
• Title not available (Why is that?)
• Ensuring correctness of model transformations while remaining decidable
• A Hoare-like calculus using the \(\mathrm{SROIQ}^{\sigma }\) logic on transformations of graphs

Cited In (1)

• A rule-based procedure for graph query solving

This page was built for publication: Reasoning formally about database queries and updates

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