{"entities":{"Q6185826":{"pageid":13320714,"ns":120,"title":"Item:Q6185826","lastrevid":57213798,"modified":"2026-03-27T12:07:44Z","type":"item","id":"Q6185826","labels":{"en":{"language":"en","value":"Integrating ADTs in KeY and their application to history-based reasoning about collection"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7785151"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6185826$6B04DB00-769D-4C68-ADB3-7B87871F1336","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"3ebc983c02ae4fc04753e2d1b875cdcb34587f23","datavalue":{"value":{"text":"Integrating ADTs in KeY and their application to history-based reasoning about collection","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6185826$683062A7-2312-44BE-9918-6A24AADA97BA","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8a8163f9cdc0e6fc922c2081ffd4c650707ccfc1","datavalue":{"value":{"entity-type":"item","numeric-id":6185824,"id":"Q6185824"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6185826$AA288938-FA64-451D-96E0-8CBF29ABBCB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"215a6f15b6577f5bb7dab2e8f95a2ff457c27f20","datavalue":{"value":{"entity-type":"item","numeric-id":6185825,"id":"Q6185825"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6185826$BEEB5A18-22A1-414C-96A1-3195809E7BAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c6539cfadc75d6504ef9c471b16074d64840fa76","datavalue":{"value":{"entity-type":"item","numeric-id":433335,"id":"Q433335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6185826$19840303-7B31-4C11-97B1-90755507AB65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4e006463586296b6604df0526236cdd07ea4c259","datavalue":{"value":{"entity-type":"item","numeric-id":439943,"id":"Q439943"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6185826$261C27E6-CFD1-4218-9583-530E8850AD24","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"70551fcc6e89042fc26ae9242a005533b44a2d7a","datavalue":{"value":{"entity-type":"item","numeric-id":169908,"id":"Q169908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6185826$31B84DAB-6D24-47E4-8CCE-4FC7A7C10DF8","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4e50f80f2416051e0e7d7d1cfabce1de8c3ea5bd","datavalue":{"value":{"time":"+2024-01-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6185826$0073CAA6-9A99-43CD-80B0-0C0E5E927CD1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"62a49b155c9af634e6c3562b1547da1f7c08791a","datavalue":{"value":"68-XX","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6185826$842449A1-6C27-4E22-AE9F-C4E96DA25FE2","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f80e68296449ea0a50499256db4546a112c3fa7f","datavalue":{"value":"7785151","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6185826$98DC64FC-1297-49C4-B370-7466420B1BA5","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2eb4d1af95699ef062cce80ecbcf1e1484586450","datavalue":{"value":"formal verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q6185826$1A41365C-AB04-4CD1-8CC9-9ABB2E3CAED8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3e1daee68cedeeadccdf496f924561e3065e4444","datavalue":{"value":"abstract data types","type":"string"},"datatype":"string"},"type":"statement","id":"Q6185826$4C25497C-525A-4140-AB89-94957CA90B86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a2b746efc66121bc1fb497da4ab39b83b5cd2f4c","datavalue":{"value":"program correctness","type":"string"},"datatype":"string"},"type":"statement","id":"Q6185826$CBB472E3-D568-4C47-8673-3F957C255762","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"15d3e4620267f515631734468329e39358d098f9","datavalue":{"value":"Java collection framework","type":"string"},"datatype":"string"},"type":"statement","id":"Q6185826$71C0D363-AA33-467A-AB2B-E61D3D5FC4E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"705a0c0d09de33f73edbfd6e8882cde2e052192f","datavalue":{"value":"KeY","type":"string"},"datatype":"string"},"type":"statement","id":"Q6185826$26FD4054-4400-49B3-BEEF-1F042B506D39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6cdc50f9ca57759a689d99741fec6e06b3926c2f","datavalue":{"value":"JML","type":"string"},"datatype":"string"},"type":"statement","id":"Q6185826$703493BB-0F6C-418D-93F9-26FB461D4E0B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"42f0513e500ea6cb630e73925875c7d53ca8d8e1","datavalue":{"value":"Isabelle/HOL","type":"string"},"datatype":"string"},"type":"statement","id":"Q6185826$2B633F1B-5657-4A55-A981-DCEEBF4C2391","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6185826$CBE9AA9F-9969-4AE1-A51C-7AAC727C0262","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7951004c83d78c1e328de2ee1a358e3b4ad24d19","datavalue":{"value":"https://doi.org/10.1007/s10703-023-00426-x","type":"string"},"datatype":"url"},"type":"statement","id":"Q6185826$87C3EB2A-6C1A-4DA6-8634-15C4E0F536BB","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"fc17bfeff7a650c29c86456156b13085870b54f4","datavalue":{"value":"W4381588017","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6185826$0BABFE80-146A-4008-806E-4DF2529AD39F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"0d19d8be06009204324df8ff597524e57805cadb","datavalue":{"value":{"entity-type":"item","numeric-id":1630025,"id":"Q1630025"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6185826$5CA22651-73F1-42BF-B556-6B3C277F705D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d0813cd8b3343a84e582034987af948dbbdb7363","datavalue":{"value":{"entity-type":"item","numeric-id":2165501,"id":"Q2165501"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6185826$AE269594-FBEF-46D7-9ADD-43CF9AFA749D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b74bb22a60e02eca9f5554979a5792a64d443ec1","datavalue":{"value":{"entity-type":"item","numeric-id":2351413,"id":"Q2351413"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6185826$4C2F6035-1579-4EF5-9993-3E56A45C8526","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d8f6d658032331dfb0270d5e1966446426f3c01f","datavalue":{"value":{"entity-type":"item","numeric-id":5326280,"id":"Q5326280"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6185826$E0EEF3DF-03B9-45C0-928B-E4A3A67C3A42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e01b51a15cfb4a137078371d8e4ef36fd1bf9baa","datavalue":{"value":{"entity-type":"item","numeric-id":4808693,"id":"Q4808693"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6185826$42EBFEF5-4FA0-45FA-B610-24093237AE79","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"00c403687d8202dbd67fe55941237745276ba153","datavalue":{"value":{"entity-type":"item","numeric-id":5953451,"id":"Q5953451"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6185826$88D5565A-1DC0-42E2-9DC5-D13B82B76575","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6b0143bb17c3271918d22cb266df388a036cbf5a","datavalue":{"value":{"entity-type":"item","numeric-id":5316580,"id":"Q5316580"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6185826$F6846E10-692C-4CD9-8939-773BA2C82570","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1807204606c08bc0647f8c538053670a3e876b3b","datavalue":{"value":{"entity-type":"item","numeric-id":3066108,"id":"Q3066108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6185826$24CA7879-54AC-4B66-A08E-DD59F3456E86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4fb957da5b0257c250122f71073f39ef71d5f9df","datavalue":{"value":{"entity-type":"item","numeric-id":5458406,"id":"Q5458406"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6185826$2D141DCA-39B1-4F23-AB3C-5D8F3C7DBC47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1ae35c6fd3b2ff27c008d60d7414656306fb431b","datavalue":{"value":{"entity-type":"item","numeric-id":5075300,"id":"Q5075300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6185826$8634FB02-8D76-421C-8880-C3B8F900D3E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6185826$9CED48BF-F16E-4CBD-9FF8-CCEC6741B028","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a1fec13708686f567ce8f652a4b4b1f5722daf5","datavalue":{"value":{"entity-type":"item","numeric-id":610397,"id":"Q610397"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6185826$3FF9FD46-7C02-47EA-BE54-502D47E6FA97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c2fa401b3f58fb4c2bc9ea2f71ee0d728db11587","datavalue":{"value":{"entity-type":"item","numeric-id":2986838,"id":"Q2986838"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6185826$289BD6C6-43E7-4CA9-B421-E8D8DBFEF9CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cb636a19f07738495cd7c2789db1b47cb8caa811","datavalue":{"value":{"entity-type":"item","numeric-id":4329634,"id":"Q4329634"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6185826$E9673F53-7015-4165-B9E5-BE5379F16EE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a2b4e51a1efe12022c4b79dd533236fa1a2525c4","datavalue":{"value":{"entity-type":"item","numeric-id":6488468,"id":"Q6488468"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6185826$ED450365-75D9-4EBD-944B-29529FF1F6C8","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4b4be52db0ec1ae33ef044e4e5ae8c4963db5e05","datavalue":{"value":"10.1007/S10703-023-00426-X","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6185826$FB53602C-8526-4355-8A15-0824A22B5154","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f5e40233eac78b6670ab30780408c237e3ea732a","datavalue":{"value":{"entity-type":"item","numeric-id":6488468,"id":"Q6488468"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a3c15f945ac1add5ffbb51e35cca2c187822f40b","datavalue":{"value":{"amount":"+0.94239664","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q6185826$CFC64651-071F-4315-9253-A83600E6E4B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b71f501dd494b832d5573783dcd25c1fa0bf2c09","datavalue":{"value":{"entity-type":"item","numeric-id":928661,"id":"Q928661"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fe68624ac9bcf439b5b3c2f0c5003081bcfbefda","datavalue":{"value":{"amount":"+0.78369844","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q6185826$8DC86D60-2662-4BF8-A9AD-83CF94394683","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dd64d5abb90dca86adaa0212049ec37dbd44fcd9","datavalue":{"value":{"entity-type":"item","numeric-id":3613439,"id":"Q3613439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fe68624ac9bcf439b5b3c2f0c5003081bcfbefda","datavalue":{"value":{"amount":"+0.78369844","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q6185826$EBA51CD0-2F32-4FCE-A4D3-8425878B6F03","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9f774791477f03afece3118a1a42eab20fcc9e7b","datavalue":{"value":{"entity-type":"item","numeric-id":4933282,"id":"Q4933282"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b603d8cb257299f760cac30a957440d1f624aa59","datavalue":{"value":{"amount":"+0.7817012","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q6185826$319101CA-0E9D-4822-88FF-CEA8052D426D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5217e06d4b33c6fa4cb698d1d2a86043c0548c3e","datavalue":{"value":{"entity-type":"item","numeric-id":5715664,"id":"Q5715664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"189bdb3e61aba9dbb1c55d397d7152bad3b45218","datavalue":{"value":{"amount":"+0.779726","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q6185826$8E92FC5D-50C7-41B7-9841-9AACEDAA4EBC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2143b0969f27f168fa6c313dcb63780c99f51a38","datavalue":{"value":{"entity-type":"item","numeric-id":1799066,"id":"Q1799066"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2db32ccab73a7945346bab88f585efbd9c00e3d6","datavalue":{"value":{"amount":"+0.7742026","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q6185826$F247BEF9-D26C-40C4-BE28-89C60502E043","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"202220c6fbcc86eaf73cd13e67301ef04335c259","datavalue":{"value":{"entity-type":"item","numeric-id":4593956,"id":"Q4593956"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"685d6fe5ae5717c5bcd06532bbca2e48fd2f142d","datavalue":{"value":{"amount":"+0.7737406","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q6185826$AA96C98D-4B28-48D3-8C81-2C00194ED40B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dfeedc05a0ec0c7d0f8ade66c64e5b7a9fc19fc0","datavalue":{"value":{"entity-type":"item","numeric-id":4251098,"id":"Q4251098"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"959f0f9a25df8d26b74907e2be89db1d63f755f1","datavalue":{"value":{"amount":"+0.77334404","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q6185826$7385B3D9-DE2F-4BE3-80A4-A4BE43E4C134","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6185826$85F2304A-66D4-4579-9004-B90C61E21960","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6185826","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6185826"}}}}}