{"entities":{"Q1791175":{"pageid":1801917,"ns":120,"title":"Item:Q1791175","lastrevid":72966525,"modified":"2026-04-14T09:04:36Z","type":"item","id":"Q1791175","labels":{"en":{"language":"en","value":"Understanding parameters of deductive verification: an empirical investigation of KeY"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6946989"}},"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":"Q1791175$5F543C33-03FA-40F5-819E-B4B7682AF947","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4dffcd5171cf2dc0554c053a07b4c54691ef4ae4","datavalue":{"value":{"text":"Understanding parameters of deductive verification: an empirical investigation of KeY","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1791175$94FEE6B7-DCB8-400D-A94F-527379B797E5","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"56c5c9a9a5c98f2f56df1150cffd1064d8382283","datavalue":{"value":"10.1007/978-3-319-94821-8_20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1791175$F86E72C0-7478-4A4C-A388-93A3898FC418","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"41193c596bf2de424ac488931905f246bbc586b8","datavalue":{"value":{"entity-type":"item","numeric-id":1791173,"id":"Q1791173"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791175$3EE4030E-6500-40D2-9141-29B1780751D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"199d29c818adf5bb5c4ec4c2444a8433d9523b01","datavalue":{"value":{"entity-type":"item","numeric-id":898604,"id":"Q898604"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791175$AEB6314A-8DC3-4ADA-9E9C-33076E55FB12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8f0fec23d80a5dbd2be19aeaac202fb947617bc9","datavalue":{"value":{"entity-type":"item","numeric-id":1791174,"id":"Q1791174"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791175$2265F023-27F9-46E4-AEC4-105715467EC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1a8de372799402bb9369830764b9ee203260e67e","datavalue":{"value":{"entity-type":"item","numeric-id":736802,"id":"Q736802"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791175$90076E83-FDDB-4364-B841-4889EFC54F59","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ff3c7136492fcf13c84b92efb7ac37b3eed57322","datavalue":{"value":{"time":"+2018-10-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1791175$1183DE87-CD60-459B-9B90-93AF4DCC51F6","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1791175$8864A8B1-1A68-432F-963D-920952445574","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1791175$E48E3F7A-72CF-4FC7-B58E-E34055D19ECA","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1ca7a6db9057e4024e55eb9f5c7305dcc6f6a7ac","datavalue":{"value":"6946989","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1791175$5B20C5CF-4E2D-45E3-9E4E-02E68C489428","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"aaa74f946f4a7cf49359214ccbeddb232ccd2dee","datavalue":{"value":"deductive verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1791175$537EAD12-A78F-4865-A0A3-56DAAFAF30FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2cbb25dd1a234db43cc9aa51b496d6421ffc2d9b","datavalue":{"value":"design by contract","type":"string"},"datatype":"string"},"type":"statement","id":"Q1791175$11831D55-BC83-4450-9237-AF35D5A2AC17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f02f4db7bd17ba3fbae1be6bcee13dc9e5aa86bc","datavalue":{"value":"formal methods","type":"string"},"datatype":"string"},"type":"statement","id":"Q1791175$CD81A3DD-A2CA-4C92-B840-AD7A2A9B018B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1791175$C7F2E410-9CBF-4BCD-868F-85BCB547BE2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"705a0c0d09de33f73edbfd6e8882cde2e052192f","datavalue":{"value":"KeY","type":"string"},"datatype":"string"},"type":"statement","id":"Q1791175$80959757-6D2D-4C4A-8130-4CBF7C13160F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c36a37a31166e7bf8d8dbc7f214e58b6f7cd6e2c","datavalue":{"value":"control parameters","type":"string"},"datatype":"string"},"type":"statement","id":"Q1791175$25189A40-B169-4063-B9BA-11F9BC450B15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1ca1042868ff4f694776e4b2c62ec66638c4ef91","datavalue":{"value":"automated reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q1791175$D60D61A9-8E72-4E17-9AED-CAE1F1A7EF73","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bb4ac1b3e6590933f07db2ef44e8e77f8844e4b4","datavalue":{"value":{"entity-type":"item","numeric-id":19271,"id":"Q19271"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791175$F0D426B7-4B61-44A9-9478-6B0924BAF77C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d560ad72fd288969b6a46f8ac77d54f6d297bf97","datavalue":{"value":{"entity-type":"item","numeric-id":16796,"id":"Q16796"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791175$5DF69E03-EB2C-43CE-9AF9-0F3397FD88DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fe5077d712c4f7a91829b6a22ef0e0039cd600ea","datavalue":{"value":{"entity-type":"item","numeric-id":15691,"id":"Q15691"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791175$36EAFF0E-E166-4733-8472-2D40157BADD3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"602b32d79a3dd12c7713e80fb0597b8ab4375f08","datavalue":{"value":{"entity-type":"item","numeric-id":16614,"id":"Q16614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791175$799B3732-BFB5-42DD-8D90-5371FCC4D62C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"076ade2f424feb4292ee73db98fc22d62f6154a2","datavalue":{"value":{"entity-type":"item","numeric-id":16769,"id":"Q16769"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791175$C3579FBD-BCC4-469A-A05B-CABE816F3BD0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"875fd2341d7eaef60a26a549ea0c9adfdf328e2e","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791175$85B7F532-1BDF-4FE2-B087-DF7BB7F2A368","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"cc47147a404ecf949cf86c4e92d2dcc5a8bfafcc","datavalue":{"value":{"entity-type":"item","numeric-id":19680,"id":"Q19680"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791175$B35D7E1E-4D7C-4363-8551-8E3C00F4EF39","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":"Q1791175$C5FB2490-B242-4108-AF56-71881EE33484","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"beb205139d0971fca32ffa61e5b55aaac31a7181","datavalue":{"value":{"entity-type":"item","numeric-id":16768,"id":"Q16768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791175$98BEE6D8-2BF3-4821-A20B-C11BC1FF1684","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"174f08d95eb791d469e1c45d7c14093069896ee1","datavalue":{"value":{"entity-type":"item","numeric-id":16797,"id":"Q16797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791175$6994DF13-E59D-419D-9096-15F621C98197","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"387c490c1ae397aba8f3b504d6b9f3825c760b89","datavalue":{"value":{"entity-type":"item","numeric-id":40366,"id":"Q40366"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791175$83A5B839-1525-450D-89D1-F18B6B445560","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":"Q1791175$B974CC44-B662-4D5F-A395-F2654EF75559","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e3430e3690f116ec125ce693bfa1cb36ac8ca8db","datavalue":{"value":"https://doi.org/10.1007/978-3-319-94821-8_20","type":"string"},"datatype":"url"},"type":"statement","id":"Q1791175$A60FD953-DB05-48EF-B8E1-C7F871209BF9","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"38ec8e39456dae04b1e50c3ed826b4aea57ccdd3","datavalue":{"value":"W2810611369","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1791175$EC132279-E972-47D3-B215-CE87EB413E24","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1c5f98b8871ed19af1195521070eec1de6c7a54c","datavalue":{"value":{"entity-type":"item","numeric-id":2075776,"id":"Q2075776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"db13c0b86496bd631ad1dac01f989953ed4dc646","datavalue":{"value":{"amount":"+0.7424479126930237","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":"Q1791175$2C3F2A01-FC69-4356-A94D-414A618A7DE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"27834f8881d79d504650b55693f4830b894523f6","datavalue":{"value":{"entity-type":"item","numeric-id":4530805,"id":"Q4530805"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b9620653c46fda052f28c94565aee8220685bd65","datavalue":{"value":{"amount":"+0.6940436959266663","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":"Q1791175$D259A6C6-F0D1-4E62-B26B-A6516E02F621","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"018780f278d91b1e97c8f1940276e2350ff28205","datavalue":{"value":{"entity-type":"item","numeric-id":6039756,"id":"Q6039756"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4522d3fadb27c684e5bbc2bc225d110a9bf904a2","datavalue":{"value":{"amount":"+0.6783473491668701","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":"Q1791175$EEFF97BC-DB5E-4C20-AF6D-AE7074A9DC0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9ec08b3c02523e826073b8df81c45fb239d6bd16","datavalue":{"value":{"entity-type":"item","numeric-id":4617972,"id":"Q4617972"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c95ce987060b483da3e28aa1898d9e9e497174ec","datavalue":{"value":{"amount":"+0.6782028079032898","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":"Q1791175$26E12A33-8FBA-413F-8425-7519AB0C3DA7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a14fc18ee4cf8f91dedea6c0f0ff3ff81b9e0fcc","datavalue":{"value":{"entity-type":"item","numeric-id":3525138,"id":"Q3525138"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1805f0b5d745e982b5062b1db8b2d40d106f3b27","datavalue":{"value":{"amount":"+0.6694135665893555","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":"Q1791175$46989C30-7478-4A23-A49A-57E1B2E3342D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Understanding parameters of deductive verification: an empirical investigation of KeY","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Understanding_parameters_of_deductive_verification:_an_empirical_investigation_of_KeY"}}}}}