{"entities":{"Q5034385":{"pageid":7063962,"ns":120,"title":"Item:Q5034385","lastrevid":98387861,"modified":"2026-06-05T17:23:36Z","type":"item","id":"Q5034385","labels":{"en":{"language":"en","value":"Mathematics and Software Verification"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7481172"}},"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":"Q5034385$8DA6D0D9-992D-48F0-B4A2-A945A6FC4BF0","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"22a59e3cb129feaf342f2467dcdb0341e0f58ab8","datavalue":{"value":"1497.68110","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5034385$45CB4731-3F04-48A7-A659-7B78B0B47232","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"83e9de7499b5a0f6d14506339adc50b7e4e1adfe","datavalue":{"value":{"time":"+2022-02-25T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5034385$82F60FE3-E58A-421B-B97A-7AB515B7AA91","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"fd95a8d23bdffdfa0a772ed7c4346e1798b9016e","datavalue":{"value":"https://www.cambridge.org/core/books/mathematics-for-future-computing-and-communications/mathematics-and-software-verification/40F48E325441E8BDB0B4D0C174493C81","type":"string"},"datatype":"url"},"type":"statement","id":"Q5034385$63FD370C-36E0-495C-911A-5C6349213307","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5034385$8EBC2431-7DEC-465B-8868-E3D3C166ECBF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5034385$317CF864-FAC5-4E3D-A06D-A6B5479DD183","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5034385$7F950180-9F9B-4256-8FE1-5BA374E21B6D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5034385$834AB67C-6CB7-491F-B8FF-F3AB3BEE2A39","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e89612c1e4149c8e7e1b04a4a656f43feec54578","datavalue":{"value":"7481172","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5034385$8304A820-5468-4285-A4AD-F99F2AAF4F75","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"78b2cb2aa8953507be78145ef07fb1e05160aa99","datavalue":{"value":"lambda-calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q5034385$0C4BF38A-5740-4A97-BF5A-208AA9F07064","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"eaba8710741c3625f74acb34aa4edd5eb82e000b","datavalue":{"value":"type systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q5034385$62C42A38-7AA9-4674-BAB0-74F6AFEB9889","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8649681bd6e022af57b527d538b7a92c7e6b6e88","datavalue":{"value":"Hoare logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5034385$37EAA36C-F0C4-4BA9-AA76-407CE7C11E2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"453e0c333d139491675f587668506703329e380f","datavalue":{"value":"propositional","type":"string"},"datatype":"string"},"type":"statement","id":"Q5034385$97E26D26-88B8-4D90-A5EF-35112E0B3F4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4bbb0c1d4a0dde26226934f7234d049627289106","datavalue":{"value":"logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5034385$7D38DB69-E5D6-48A0-99AB-DF12CACB8976","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a4a6f11756e1720f07cda5a080ef0476786d909b","datavalue":{"value":"temporal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5034385$917A751E-C667-4A63-9FD8-54A7DFF60496","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f89b34d84a29901e6cfe557573b31fa1373d9525","datavalue":{"value":"Curry-Howard correspondence","type":"string"},"datatype":"string"},"type":"statement","id":"Q5034385$26D3C88E-0179-4598-8EF7-99B57F572C83","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8bf549142b710f01581b24fd28cbb67614316cd4","datavalue":{"value":"theorem prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q5034385$ACBB9BE6-69AA-418F-94B1-E539596EAAD7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bda40ec213904c1453e8a281472f9239bacbf0a6","datavalue":{"value":"model checker","type":"string"},"datatype":"string"},"type":"statement","id":"Q5034385$957B70FA-2174-4614-995D-FAB4CEA17912","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c0f668560f85d7afd1fece97b175bc3414226fbb","datavalue":{"value":"program analysis","type":"string"},"datatype":"string"},"type":"statement","id":"Q5034385$9E851808-31E3-4FCF-8772-F5FDFF390443","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":"Q5034385$A39E2918-F956-47A4-AB1E-315E4B479372","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f1ea3579438a3282b8d760521b2d0f5a4c8d2f67","datavalue":{"value":"10.1017/9781009070218.004","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5034385$A31E74AE-0B5F-4420-8111-518B5DBECAFE","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"71c53046bd7c8feae0e5510e492c3038e7297ea2","datavalue":{"value":"W4200585533","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5034385$A77B56B8-CFCD-4C71-A2C1-E5E611E8FA48","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d198505a043011f7927cf7643da75d3250a09047","datavalue":{"value":{"text":"Mathematics and Software Verification","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5034385$68FA352E-C303-41AE-B988-4BBA2C6D811D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a8470007205dbfe1cee57b9adc29ba46c1af543e","datavalue":{"value":{"entity-type":"item","numeric-id":4718231,"id":"Q4718231"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a9d92864d12c9d893be1b9f3d5054b3355c21ead","datavalue":{"value":{"amount":"+0.912243","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5034385$DEE6819D-7C20-4B95-8C98-5190C016E638","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bc14187770e67062cdb53c67a7ab88200831dae0","datavalue":{"value":{"entity-type":"item","numeric-id":4929925,"id":"Q4929925"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f3fe36b49ee61ec10be0453231da8ad3f6df52cc","datavalue":{"value":{"amount":"+0.8915857","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5034385$0B3210A1-BF24-4668-8996-9A187D22D79D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"187ddb9dbc8f16f78a958b019089298a129462a4","datavalue":{"value":{"entity-type":"item","numeric-id":4003444,"id":"Q4003444"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8bdca811ba70a65a9967a84356bc1f20305fafbf","datavalue":{"value":{"amount":"+0.88592315","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5034385$5152BF8C-0BC3-4CC9-98C8-73F883D05FDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1d4f6a6129f9f29667323ba246bbda5a98053c4b","datavalue":{"value":{"entity-type":"item","numeric-id":4284599,"id":"Q4284599"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4768faa35f97ec292615e094e88c728e27818a5d","datavalue":{"value":{"amount":"+0.8858259","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5034385$86942F35-4129-4689-ADBD-280611DB4C54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"18b45fc735c0a84871240051e9d100a34e025117","datavalue":{"value":{"entity-type":"item","numeric-id":4364532,"id":"Q4364532"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5478a5620492e13d89babbc282c0f67ca34a20dd","datavalue":{"value":{"amount":"+0.8821385","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5034385$2B8EF127-0835-4352-8A84-126DE090B811","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1ed458b9d688347bb438672da469a0a34103d14f","datavalue":{"value":{"entity-type":"item","numeric-id":3637262,"id":"Q3637262"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f401252ceb26982d9c9fea3bf99b801b80abe268","datavalue":{"value":{"amount":"+0.8813926","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5034385$D7C59791-6C85-42B3-B6F1-0CC0D42E013C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3c0254df9f4f76cad0ec1855a19e97bfce6ef1bb","datavalue":{"value":{"entity-type":"item","numeric-id":2988059,"id":"Q2988059"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"718ac44bda57305f462a5b5a3bb5004fc705a7bc","datavalue":{"value":{"amount":"+0.87266254","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5034385$D966DE7E-7555-48CF-9156-9E7612ADBEAC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"39b4648096244d97855d2751bd98de8192b299ae","datavalue":{"value":{"entity-type":"item","numeric-id":1181864,"id":"Q1181864"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"95111d0ee6b7f686abcc5c3879adcb0b4595f53f","datavalue":{"value":{"amount":"+0.8685269","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5034385$F6BAB20C-B459-4013-B6E8-A25E2ABA1611","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Mathematics and Software Verification","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Mathematics_and_Software_Verification"}}}}}