{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T00:06:36Z","timestamp":1778198796900,"version":"3.51.4"},"reference-count":47,"publisher":"Oxford University Press (OUP)","issue":"5","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,10,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In database theory, the term database transformation was used to refer to a unifying treatment for computable queries and updates. Recently, it was shown that non-deterministic database transformations can be captured exactly by a variant of ASMs, the so-called Database Abstract State Machines (DB-ASMs). In this article we present a logic for DB-ASMs, extending the logic of Nanchen and St\u00e4rk for ASMs. In particular, we develop a rigorous proof system for the logic for DB-ASMs, which is proven to be sound and complete. The most difficult challenge to be handled by the extension is a proper formalization capturing non-determinism of database transformations and all its related features such as consistency, update sets or multisets associated with DB-ASM rules. As the database part of a state of database transformations is a finite structure and DB-ASMs are restricted by allowing quantifiers only over the database part of a state, we resolve this problem by taking update sets explicitly into the logic, i.e. by using an additional modal operator $[X]$, where $X$ is interpreted as an update set $\\Delta$ generated by a DB-ASM rule. The DB-ASM logic provides a powerful verification tool to study properties of database transformations.<\/jats:p>","DOI":"10.1093\/jigpal\/jzx021","type":"journal-article","created":{"date-parts":[[2017,6,6]],"date-time":"2017-06-06T11:19:44Z","timestamp":1496747984000},"page":"700-740","source":"Crossref","is-referenced-by-count":14,"title":["A complete logic for Database Abstract State Machines1"],"prefix":"10.1093","volume":"25","author":[{"given":"Flavio","family":"Ferrarotti","sequence":"first","affiliation":[{"name":"Software Competence Center Hagenberg, Austria."}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Klaus-Dieter","family":"Schewe","sequence":"additional","affiliation":[{"name":"Software Competence Center Hagenberg, Austria."}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Loredana","family":"Tec","sequence":"additional","affiliation":[{"name":"RISC Software GmbH, Austria."}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qing","family":"Wang","sequence":"additional","affiliation":[{"name":"Research School of Computer Science, The Australian National University, Canberra, Australia."}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2017,7,6]]},"reference":[{"key":"2020022409593837900_B1","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1145\/67544.66941","article-title":"Object identity as a query language primitive.","volume-title":"Proceedings of the 1989 ACM SIGMOD International Conference on Management of Data","author":"Abiteboul","year":"1989"},{"key":"2020022409593837900_B2","doi-asserted-by":"crossref","first-page":"260","DOI":"10.1145\/28659.28688","article-title":"A transcation language complete for database update and specification.","author":"Abiteboul","year":"1987","journal-title":"Proceedings of the Sixth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems"},{"key":"2020022409593837900_B3","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1016\/0022-0000(91)90032-Z","article-title":"Datalog extensions for database queries and updates.","volume":"43","author":"Abiteboul","year":"1991","journal-title":"J. Comput. Syst. Sci."},{"key":"2020022409593837900_B4","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/978-1-4615-5137-9_2","article-title":"Identification as a primitive of data models.","volume-title":"Fundamentals of Information Systems","author":"Beeri","year":"1999"},{"key":"2020022409593837900_B5","doi-asserted-by":"crossref","first-page":"578","DOI":"10.1145\/937555.937561","article-title":"Abstract state machines capture parallel algorithms.","volume":"4","author":"Blass","year":"2003","journal-title":"ACM Transactions on Computational Logic"},{"key":"2020022409593837900_B6","first-page":"1","article-title":"Abstract state machines capture parallel algorithms: correction and extension.","volume":"9","author":"Blass","year":"2008","journal-title":"ACM Transactions on Computation Logic"},{"key":"2020022409593837900_B7","doi-asserted-by":"crossref","first-page":"1093","DOI":"10.2178\/jsl\/1190150152","article-title":"On polynomial time computation over unordered structures.","volume":"67","author":"Blass,","year":"2002","journal-title":"The Journal of Symbolic Logic"},{"key":"2020022409593837900_B8","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BFb0055494","article-title":"The state of change: a survey.","volume-title":"International Seminar on Logic Databases and the Meaning of Change, Transactions and Change in Logic Databases","author":"Bonner","year":"1998"},{"key":"2020022409593837900_B9","volume-title":"Abstract State Machines. A Method for High-Level System Design and Analysis","author":"B\u00f6rger","year":"2003"},{"key":"2020022409593837900_B10","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-18216-7","volume-title":"Abstract State Machines: A Method for High-Level System Design and Analysis","author":"B\u00f6rger","year":"2003"},{"key":"2020022409593837900_B11","doi-asserted-by":"crossref","first-page":"612","DOI":"10.1109\/SFCS.1989.63543","article-title":"An optimal lower bound on the number of variables for graph identification.","volume-title":"Proceedings of the 30th Annual Symposium on Foundations of Computer Science","author":"Cai,","year":"1989"},{"key":"2020022409593837900_B12","doi-asserted-by":"crossref","first-page":"156","DOI":"10.1016\/0022-0000(80)90032-X","article-title":"Computable queries for relational data bases.","volume":"21","author":"Chandra","year":"1980","journal-title":"Journal of Computer and System Sciences"},{"key":"2020022409593837900_B13","article-title":"MLPM: Defining a semantics and axiomatization for specifying the reasoning process of knowledge-based systems.","volume-title":"Proceedings of the 12th European Conference on Artificial Intelligence (ECAI-96)","author":"Fensel","year":"1996"},{"key":"2020022409593837900_B14","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1093\/jigpal\/jzt025","article-title":"Expressing properties in second- and third-order logic: hypercube graphs and SATQBF.","volume":"22","author":"Ferrarotti,","year":"2014","journal-title":"Logic Journal of the IGPL"},{"key":"2020022409593837900_B15","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1016\/j.tcs.2016.08.013","article-title":"A new thesis concerning synchronised parallel computing - simplified parallel ASM thesis.","volume":"649","author":"Ferrarotti,","year":"2016","journal-title":"Theoretical Computer Science"},{"key":"2020022409593837900_B16","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1006\/inco.1997.2675","article-title":"Metafinite model theory.","volume":"140","author":"Gr\u00e4del","year":"1998","journal-title":"Information and Computation"},{"key":"2020022409593837900_B17","first-page":"231","article-title":"Inductive definability with counting on finite structures.","volume-title":"Selected Papers from the Workshop on Computer Science Logic","author":"Gr\u00e4del","year":"1993"},{"key":"2020022409593837900_B18","doi-asserted-by":"crossref","first-page":"340","DOI":"10.1007\/978-1-4471-3229-5_19","article-title":"Reasoning about dynamic features in specification languages - a modal view on creation and modification.","volume-title":"Proceedings of the International Workshop on Semantics of Specification Languages (SoSL)","author":"Groenboom","year":"1994"},{"key":"2020022409593837900_B19","article-title":"A formalization of evolving algebras.","volume-title":"Proceedings of Accolade95","author":"Groenboom","year":"1995"},{"key":"2020022409593837900_B20","first-page":"317","article-title":"A new thesis (abstracts).","volume":"6","author":"Gurevich.","year":"1985","journal-title":"American Mathematical Society"},{"key":"2020022409593837900_B21","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1145\/343369.343384","article-title":"Sequential abstract state machines capture sequential algorithms.","volume":"1","author":"Gurevich.","year":"2000","journal-title":"ACM Transactions on Computational Logic"},{"key":"2020022409593837900_B22","doi-asserted-by":"crossref","first-page":"6","DOI":"10.1007\/978-3-540-24627-5_2","article-title":"Abstract state machines: an overview of the project.","author":"Gurevich.","year":"2004","journal-title":"International Symposium on Foundations of Information and Knowledge Systems"},{"key":"2020022409593837900_B23","doi-asserted-by":"crossref","first-page":"880","DOI":"10.1145\/502090.502100","article-title":"Logics with aggregate operators.","volume":"48","author":"Hella,","year":"2001","journal-title":"Journal of the ACM"},{"key":"2020022409593837900_B24","doi-asserted-by":"crossref","first-page":"81","DOI":"10.2307\/2266967","article-title":"Completeness in the theory of types.","volume":"15","author":"Henkin.","year":"1950","journal-title":"Journal of Symbolic Logic"},{"key":"2020022409593837900_B25","doi-asserted-by":"crossref","DOI":"10.4324\/9780203290644","volume-title":"A New Introduction to Modal Logic","author":"Hughes","year":"1996"},{"key":"2020022409593837900_B26","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1109\/PSCT.1987.10319271","article-title":"Expressibility as a complexity measure: results and directions.","author":"Immerman.","year":"1987","journal-title":"Proceedings of Second Conference on Structure in Complexity Theory"},{"key":"2020022409593837900_B27","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1093\/oso\/9780198537465.003.0004","article-title":"Higher order logic.","volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming, Volume2, Deduction Methodologies","author":"Leivant.","year":"1994"},{"key":"2020022409593837900_B28","author":"Nanchen.","year":"2007","journal-title":"Verifying Abstract State Machines"},{"key":"2020022409593837900_B29","doi-asserted-by":"crossref","first-page":"147","DOI":"10.2307\/2275602","article-title":"The expressive power of fixed-point logic with counting.","volume":"61","author":"Martin","year":"1996","journal-title":"Journal of Symbolic Logic"},{"key":"2020022409593837900_B30","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-21676-7","volume-title":"Bounded Variable Logics and Counting \u2013 A Study in Finite Models","author":"Otto.","year":"1997"},{"key":"2020022409593837900_B31","article-title":"A logic of modification and creation.","volume-title":"Logical Perspectives on Language and Information","author":"Renardel de Lavalette.","year":"2001"},{"key":"2020022409593837900_B32","first-page":"49","article-title":"Fundamental concepts of object oriented databases.","volume":"11","author":"Schewe","year":"1993","journal-title":"Acta Cybernetica"},{"key":"2020022409593837900_B33","first-page":"765","article-title":"A customised ASM thesis for database transformations.","volume":"19","author":"Schewe","year":"2010","journal-title":"Acta Cybernetica"},{"key":"2020022409593837900_B34","article-title":"Extending Dynamic Logic for Reasoning about Evolving Algebras.","volume-title":"Technical Report 49\/95","author":"Sch\u00f6negge.","year":"1995"},{"key":"2020022409593837900_B35","volume-title":"Logics of Database Updates","author":"Spruit.","year":"1994"},{"key":"2020022409593837900_B36","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/978-1-4471-3554-8_7","article-title":"Dynamic database logic: the first-order case.","volume-title":"Modelling Database Dynamics","author":"Spruit,","year":"1993"},{"key":"2020022409593837900_B37","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1093\/logcom\/5.1.27","article-title":"Axiomatization, declarative semantics and operational semantics of passive and active updates in logic databases.","volume":"5","author":"Spruit,","year":"1995","journal-title":"Journal of Logic and Computation"},{"key":"2020022409593837900_B38","doi-asserted-by":"crossref","first-page":"591","DOI":"10.1016\/S0304-3975(00)00289-9","article-title":"Regular database update logics.","volume":"254","author":"Spruit,","year":"2001","journal-title":"Theoretical Computer Science"},{"key":"2020022409593837900_B39","first-page":"980","article-title":"A logic for abstract state machines.","volume":"7","author":"St\u00e4rk","year":"2001","journal-title":"Journal of Universal Computer Science"},{"key":"2020022409593837900_B40","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1016\/S0168-0072(00)00055-5","article-title":"On the expressibility and the computability of untyped queries.","volume":"108","author":"Turull Torres.","year":"2001","journal-title":"Annals of Pure and Applied Logic"},{"key":"2020022409593837900_B41","first-page":"485","article-title":"Relational databases and homogeneity in logics with counting.","volume":"17","author":"Turull Torres.","year":"2006","journal-title":"Acta Cybernetica"},{"key":"2020022409593837900_B42","volume-title":"Formal Aspects of Object Identity in Database Manipulation","author":"Van den Bussche.","year":"1993"},{"key":"2020022409593837900_B43","first-page":"3","article-title":"Non-deterministic aspects of object-creating database transformations.","volume-title":"Selected Papers from the Fourth International Workshop on Foundations of Models and Languages for Data and Objects","author":"Van den Bussche","year":"1993"},{"key":"2020022409593837900_B44","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1006\/jcss.1997.1450","article-title":"A semideterministic approach to object creation and nondeterminism in database queries.","volume":"54","author":"van den Bussche","year":"1997","journal-title":"J. Comput. Syst. Sci."},{"key":"2020022409593837900_B45","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1145\/256303.256311","article-title":"On the completeness of object-creating database transformation languages.","volume":"44","author":"Van Den Bussche,","year":"1997","journal-title":"Journal of the ACM"},{"key":"2020022409593837900_B46","doi-asserted-by":"crossref","first-page":"462","DOI":"10.1109\/69.929903","article-title":"A survey of languages for specifying dynamics: A knowledge engineering perspective.","volume":"13","author":"van Eck,","year":"2001","journal-title":"IEEE Transactions on Knowledge and Data Engineering"},{"key":"2020022409593837900_B47","author":"Wang.","year":"2010","journal-title":"Logical Foundations of Database Transformations for Complex-Value Databases. Logos"}],"container-title":["Logic Journal of the IGPL"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/jigpal\/article-pdf\/25\/5\/700\/19916954\/jzx021.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/academic.oup.com\/jigpal\/article-pdf\/25\/5\/700\/19916954\/jzx021.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,24]],"date-time":"2024-06-24T15:58:25Z","timestamp":1719244705000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/jigpal\/article\/25\/5\/700\/3930938"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,7,6]]},"references-count":47,"journal-issue":{"issue":"5","published-online":{"date-parts":[[2017,7,6]]},"published-print":{"date-parts":[[2017,10,1]]}},"URL":"https:\/\/doi.org\/10.1093\/jigpal\/jzx021","relation":{},"ISSN":["1367-0751","1368-9894"],"issn-type":[{"value":"1367-0751","type":"print"},{"value":"1368-9894","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2017,10]]},"published":{"date-parts":[[2017,7,6]]}}}