{"entities":{"Q3460073":{"pageid":5239473,"ns":120,"title":"Item:Q3460073","lastrevid":52431461,"modified":"2026-01-22T15:28:44Z","type":"item","id":"Q3460073","labels":{"en":{"language":"en","value":"Reasoning about loops using Vampire in KeY"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6528798"}},"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":"Q3460073$46B587B5-C4A9-406F-B0E6-8CFDE93617DB","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6739f02877762e403cc0f2f9d6ca9a431d5de966","datavalue":{"value":{"text":"Reasoning About Loops Using Vampire in KeY","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3460073$E9F8FF00-8D33-4746-8897-C3CE77F7C0DA","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"51717fb764f597a05ce4e28e25f9ecb9bc5c7be3","datavalue":{"value":"1471.68299","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3460073$57AEE08C-003A-4A65-8DD0-FC55B4C79E82","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"89a8d1024f58a429fb6d4806e6b405c7b5970868","datavalue":{"value":"10.1007/978-3-662-48899-7_30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3460073$731D3029-CF98-4091-89D6-9ABB0057E0D3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"38294c3226d3792efd0f0a6334adfdf20cdb195e","datavalue":{"value":{"entity-type":"item","numeric-id":1951608,"id":"Q1951608"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3460073$510BEDBE-BF3F-448A-B972-6618CD1440BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f17059e6c6c8a57972334867cc4d511b5d1368f5","datavalue":{"value":{"entity-type":"item","numeric-id":507357,"id":"Q507357"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3460073$F171C25D-8FAD-474D-8BD9-2F5F1F817C37","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"271a0e8db5ca773d7b7fe045738dca9e2e181b42","datavalue":{"value":{"entity-type":"item","numeric-id":1799097,"id":"Q1799097"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3460073$90A0D298-E0D3-4A5B-8A05-06D13C9575DC","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"23864e2be568bb8a6a4b0526f5a5216348320070","datavalue":{"value":{"entity-type":"item","numeric-id":2870110,"id":"Q2870110"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3460073$81B2ECD1-C052-40CD-A18E-CD70C845C0E7","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f91432dc3d3ba35c1a5312422600047e5b632480","datavalue":{"value":{"time":"+2016-01-12T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3460073$FB1ED5CA-643D-4B75-B651-51C1051DCDF3","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"0ecf7423fb0b745a64619cf276027d5f39a0414e","datavalue":{"value":"https://research.chalmers.se/en/publication/230103","type":"string"},"datatype":"url"},"type":"statement","id":"Q3460073$00AB50F2-7373-4809-B2E0-434F4FC11C71","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3460073$45B96F17-C0ED-4ADD-BDB6-14BDA67DC64C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3460073$F81EA4DA-E2F1-4EC7-8BA4-71C067F83784","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3460073$E7D11A5F-7769-4405-A43E-DE57102B17BC","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a8d1c9dfcac37ec9868e95f8c147ebb38b5885f4","datavalue":{"value":"6528798","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3460073$7CBEF466-CADA-4750-A43C-72F0069E9B72","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"33734e36764580044df2d1101af853dac96392fb","datavalue":{"value":{"entity-type":"item","numeric-id":21759,"id":"Q21759"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3460073$5415F91C-F2C1-4E35-8DAD-D92F179E862B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"12b8fef36068e5bdaa4e8c4c10a706c6f98b9349","datavalue":{"value":{"entity-type":"item","numeric-id":21946,"id":"Q21946"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3460073$AFD65FCD-248F-4BA8-AA32-C00CFF7F0322","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"4e406b8269af4709abcc406a491ca24cc7343d00","datavalue":{"value":{"entity-type":"item","numeric-id":26190,"id":"Q26190"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3460073$C1299BC6-D861-44DA-A17D-D902F7B03CDE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b6da1f42e3d4d28e24ecb68672c28ee0982a60c2","datavalue":{"value":{"entity-type":"item","numeric-id":12950,"id":"Q12950"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3460073$1F0702CF-5E5F-4B05-9280-2C2CE71463C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b443b776731e3bc75eb79b752e7ef8c4cee2d97a","datavalue":{"value":{"entity-type":"item","numeric-id":15455,"id":"Q15455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3460073$FB9FC462-38DF-427D-BE92-2EB908B5F40F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ea1fa890b2f09c8cd0bccb17957cf46696afec2a","datavalue":{"value":{"entity-type":"item","numeric-id":19731,"id":"Q19731"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3460073$23996E4C-F21D-499E-BCFF-E09E4AD8A891","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bc807d9506db4bab94926c38fdb1add92f3e81aa","datavalue":{"value":{"entity-type":"item","numeric-id":25559,"id":"Q25559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3460073$7AFD4915-FFEC-4591-B575-FADEFEF355CF","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":"Q3460073$AF6D94B3-DA73-42D0-B5AB-357FC315997A","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"1610096efb70d40429d59134c88efb72661ea3b4","datavalue":{"value":"W2230265119","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3460073$8C9D9341-70FA-4737-B244-55F086B0C494","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"78e34b0c20288b3099b2e33d6d5d3751e01de186","datavalue":{"value":{"entity-type":"item","numeric-id":5747760,"id":"Q5747760"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a919a810be63f60b9145b4f046547c35359691f9","datavalue":{"value":{"amount":"+0.7713898420333862","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3460073$FD2041DF-CE92-409F-87CA-F4519CCB6170","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"87fe0da3efb68e9a28fd7c5b4931d8d9ec90853c","datavalue":{"value":{"entity-type":"item","numeric-id":882517,"id":"Q882517"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9e19e16f2c2eb38a60a744e7e0bd2fe7ba871190","datavalue":{"value":{"amount":"+0.7565450668334961","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3460073$9CF56BFF-8618-4DC7-B849-00B30A85FB3F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"76b63caf5f28b762bf948547dcc600d322ce5750","datavalue":{"value":{"entity-type":"item","numeric-id":2180218,"id":"Q2180218"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8685b11e13571fb64ac8abbc9a28648e4dce4d34","datavalue":{"value":{"amount":"+0.7510885000228882","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3460073$7248A0E9-CEDC-4084-9F03-B6415D3AEA23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5cb23bd8c9cdca6792eabcff20647876a470cc75","datavalue":{"value":{"entity-type":"item","numeric-id":5096093,"id":"Q5096093"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8755c4bf330b6acd7b1c6640236af26f9631bbb8","datavalue":{"value":{"amount":"+0.7443662881851196","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3460073$7935E1D7-566D-40F1-9F47-7A1CE2F5B7EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"08347eef503ef7ac96f08b390b8462d50d19a875","datavalue":{"value":{"entity-type":"item","numeric-id":5387902,"id":"Q5387902"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8d731412b151224c5f9bf0a5ec1f10600564702f","datavalue":{"value":{"amount":"+0.7336447834968567","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3460073$AB23B98E-B1AC-41FF-B495-0228E30E657E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3460073","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3460073"}}}}}