Reasoning formally about database queries and updates

DOI10.1007/978-3-030-30942-8_33MaRDI QIDQ6535969zbMATHFDO

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

Publication date 14 March 2024

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)

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

Cites work

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

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)