{"entities":{"Q2979871":{"pageid":2990596,"ns":120,"title":"Item:Q2979871","lastrevid":52792007,"modified":"2026-01-23T12:39:43Z","type":"item","id":"Q2979871","labels":{"en":{"language":"en","value":"Deductive formal verification of search programs in arrays of arbitrary size for abstract register machines"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6708348"}},"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":"Q2979871$FA71098D-B7EA-4AFA-844A-293B35DB3B39","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"247e6fae1a7972fd0316403c51fa386612f15c6a","datavalue":{"value":"1374.68276","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2979871$9D82E059-9CAC-4C0D-9038-4848874FE787","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"780337e612606e6b0cfc1a9e4d31030a02569608","datavalue":{"value":{"entity-type":"item","numeric-id":2729919,"id":"Q2729919"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2979871$AFBA6E85-E73E-4813-A3C9-401D94C95F25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f12ab6a50dca285e32f059f3cef41583e61bc6ed","datavalue":{"value":{"entity-type":"item","numeric-id":174086,"id":"Q174086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2979871$26EFEBF5-9EF8-4F47-8B1A-E4CEFF0AA2C2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5136aa5d1d5384ee622607c2cb579d682b7a682f","datavalue":{"value":{"time":"+2017-04-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2979871$096F646F-477F-4E98-9AFF-4DD1FA73E9F6","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"09a1917c844a927b43c2117218a51a04d846362e","datavalue":{"value":"http://bulletin.iis.nsk.su/files/article/chklaev_nepomniaschy.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q2979871$1F1E31BF-08CA-4B0D-9174-409D186EAEED","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2979871$C5EFA0D1-694B-45A7-A517-A93BE7F45C0A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a7dde57cbaf704d564d8f981ca98d6340e3d4aaf","datavalue":{"value":"68Q05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2979871$04975054-62B3-4192-8328-A58F75FDF524","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2979871$2F77B972-432E-4A2B-B9D5-490D7DF21843","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"27e8d97cb1d0c6d0dda73cca90cf17ce224bcb97","datavalue":{"value":"6708348","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2979871$4712BC3A-C78E-4A5D-98C9-9BA9784B8AE2","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"04c3aab5a061d35b4c668f3feb13bfd604c5534a","datavalue":{"value":"abstract register machine","type":"string"},"datatype":"string"},"type":"statement","id":"Q2979871$294E9A9A-0D53-4949-B79A-326478663F16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"35c2de8df8bea7d6ad3c7280dbbbde5b95b595d6","datavalue":{"value":"random-access machine","type":"string"},"datatype":"string"},"type":"statement","id":"Q2979871$ED5C2008-1C21-463E-8D07-EA4C14A62822","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a08f83a606742cb47022960ab42e26fe51054d19","datavalue":{"value":"search program","type":"string"},"datatype":"string"},"type":"statement","id":"Q2979871$68D1AF74-EBA8-46B3-8E14-8B6C509B7F1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"87994eb840961e5165378eb7f918102952689b42","datavalue":{"value":"formal specification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2979871$CC260A00-D216-4002-8AFB-82BDACE6FFF5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2979871$89A60CFC-C146-49BE-B339-7B942B88E16C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"14b5e090dbc9bcb80548540aca8b83d5cf21b1b3","datavalue":{"value":"verification system PVS","type":"string"},"datatype":"string"},"type":"statement","id":"Q2979871$77129845-7086-4A90-B8E6-71499A7886C9","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2979871$528BD3A4-E480-4F50-B085-726AB7264C48","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":"Q2979871$D17FFBF2-E5EF-4777-B45D-7249D55890A9","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8bd3e90d535e5ccef0f68cbceae528c380a32067","datavalue":{"value":{"entity-type":"item","numeric-id":2979849,"id":"Q2979849"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8af3307b657613ae23559c10ec9042447cee8070","datavalue":{"value":{"amount":"+0.8636382818222046","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":"Q2979871$51F665DA-7175-48D5-8EEF-2E1DBF948A82","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2a76b3577a7618bb02f9806580f51d2b7da93b94","datavalue":{"value":{"entity-type":"item","numeric-id":5900551,"id":"Q5900551"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e7143652aace9b03f3e3d8e6ad5ed1130dcda725","datavalue":{"value":{"amount":"+0.7106429934501648","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":"Q2979871$EC14F30C-3CDE-419E-AB45-4B5069C36C03","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"747262510cb6b2d1e886a4e3f4a91d7ce069382a","datavalue":{"value":{"entity-type":"item","numeric-id":4818811,"id":"Q4818811"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"95cd7d4fe4d5e45196152afbdf5e3a911c13cfbe","datavalue":{"value":{"amount":"+0.6924148201942444","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":"Q2979871$5EC41810-E2A9-4046-B03A-6342AEE6D8DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"59bfbdc7e86cccf445f54e1e3091c5033971a071","datavalue":{"value":{"entity-type":"item","numeric-id":2323994,"id":"Q2323994"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2a3397860e38d013976de12e23310bc73af7ae35","datavalue":{"value":{"amount":"+0.6839051246643066","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":"Q2979871$A599DD61-11D6-41D1-86D3-940EA472CC1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"819aed6fb55858a3ba166b981e35c6d2e4ad1174","datavalue":{"value":{"entity-type":"item","numeric-id":2946676,"id":"Q2946676"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b36832ebb993a044185f16dff0765e5d5c079891","datavalue":{"value":{"amount":"+0.6829807758331299","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":"Q2979871$9E6C485E-C585-4FDE-AB7C-4EC6702DEE14","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2979871","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2979871"}}}}}