{"entities":{"Q6488526":{"pageid":14067295,"ns":120,"title":"Item:Q6488526","lastrevid":47845624,"modified":"2026-01-02T20:57:15Z","type":"item","id":"Q6488526","labels":{"en":{"language":"en","value":"Tactical theorem proving in program verification"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7680802"}},"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":"Q6488526$75741E86-E2FB-4B8D-98A6-7FA110B6CADC","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8db42e05b251606b1a771aeb2e39d03d9996d9e9","datavalue":{"value":{"text":"Tactical theorem proving in program verification","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6488526$A6D373AC-8B6E-4A2E-A8F6-2AF18518C9BD","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"28a72edabcf70c6aae35d2fcb402b7a7b9170713","datavalue":{"value":"1509.68165","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6488526$E7E185AB-C7F2-4062-8E85-4D72911BEAA6","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"cbf712d733969dba54524698f6da245bf8977eed","datavalue":{"value":"10.1007/3-540-52885-7_83","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6488526$63E5F316-B521-4376-B13F-74328EDA2D8E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ddd8c7cdfab1c438dce05a29a6739ec9dbbcb8dc","datavalue":{"value":{"entity-type":"item","numeric-id":4559229,"id":"Q4559229"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488526$4ABD4EFB-FB91-4D91-97CC-30E105CA68E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8dfedb9e8f39a520fe833d6538db6dc39854cff4","datavalue":{"value":{"entity-type":"item","numeric-id":539222,"id":"Q539222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488526$EDB6F762-8EE9-4A98-94E7-806C8AD3A0BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"15e486d32bb4e02e637c42fa3bc0f8812e77532d","datavalue":{"value":{"entity-type":"item","numeric-id":1856149,"id":"Q1856149"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488526$6437586C-68D0-421E-9D71-7DFE9C82B452","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"30bf4c979a904132ac28909e79b707831f730270","datavalue":{"value":{"time":"+2023-04-28T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6488526$ACA31816-B83B-49A1-ADC1-4720D7AB5359","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6488526$B6D20549-BCEC-4025-B270-CC53E4CAD06B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6488526$CE23BE68-C49B-4795-9DB1-430E67BCF5E4","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4017244ded1e02c5fa1c7a4f76b2eecc91344cc9","datavalue":{"value":"7680802","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6488526$8C65F784-9BB1-4251-8898-A6EAECE86C6E","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":"Q6488526$773E7C83-9F9C-484F-B66B-E1B327D06E32","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"a92f26e58a943b02e78674f3a8491b69ad7ff1fb","datavalue":{"value":{"entity-type":"item","numeric-id":789887,"id":"Q789887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488526$1C414C9E-112B-4D6B-AC78-98212FA1B642","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8124e2aa86067094dab23bb14b8dadf2e19d522b","datavalue":{"value":{"entity-type":"item","numeric-id":3894958,"id":"Q3894958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488526$E0F7C2BF-E66E-4A96-8919-98B94301EF42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d346d8485da0bc889f787fa277d331b616d4df2","datavalue":{"value":{"entity-type":"item","numeric-id":4054648,"id":"Q4054648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488526$8368E971-836C-4738-B85A-2D035BB40E5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f4e10d75be49aac16b2a9fe9dea41a737d04b003","datavalue":{"value":{"entity-type":"item","numeric-id":4692773,"id":"Q4692773"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488526$4B5FF182-4576-42BD-B0EA-70A4A3384D53","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d5e2b13fd5a27d330f592699f5bb5ff339813ded","datavalue":{"value":{"entity-type":"item","numeric-id":3789101,"id":"Q3789101"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488526$A8A87B2E-B628-4AA0-BEA4-7389C641B404","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6cc8abb92210655a5bd4143cbbadd6eadb52d635","datavalue":{"value":{"entity-type":"item","numeric-id":1801222,"id":"Q1801222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488526$27AC82C7-BE78-462F-BDB6-119DF64481F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1cfde9258ea2a6a7a2ef370ef24dca25d45d9fcc","datavalue":{"value":{"entity-type":"item","numeric-id":1158956,"id":"Q1158956"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488526$BF453F91-188B-40E3-8B53-9DD1118574F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e47b8c90d45ee285590b1a168a8503851fe5b134","datavalue":{"value":{"entity-type":"item","numeric-id":3925859,"id":"Q3925859"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488526$54240027-5C82-4AF5-80D6-E39247FB5123","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5710cd0fb8b5907d40eeada6e14d4018e26669a5","datavalue":{"value":{"entity-type":"item","numeric-id":1255942,"id":"Q1255942"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488526$BDC7F62F-B4E4-4E8D-B3E9-3B976DBB772A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d933b03354d7c828ce52bdfc7df38cf961b128e","datavalue":{"value":{"entity-type":"item","numeric-id":3766816,"id":"Q3766816"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488526$C434160C-69DB-4312-9E78-A3F61638529D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ba9ff30ef38a52ddb3b28dfeaf2110fe75244c1b","datavalue":{"value":{"entity-type":"item","numeric-id":3826528,"id":"Q3826528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488526$F35CF7F4-E961-4DE4-BF69-C24FEB23108E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9087b8af215e6c289de2d21b6b2bd6cf9bd5820d","datavalue":{"value":{"entity-type":"item","numeric-id":3336725,"id":"Q3336725"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488526$4EF7CEBA-5AF3-403E-8BA9-74DC4DC1C13D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"777f1902a1127b94884ae1ddc89768860f054a6e","datavalue":{"value":{"entity-type":"item","numeric-id":3789060,"id":"Q3789060"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6488526$E93433B1-E13F-4AC1-BC28-2B933AA2AC9A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"65783770f753a60e730e2f256403c2da900bb4d3","datavalue":{"value":{"entity-type":"item","numeric-id":3766816,"id":"Q3766816"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3899aec6b083a13cc23047558a7028748eab35c8","datavalue":{"value":{"amount":"+0.8085874915122986","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":"Q6488526$4EBE9DEB-8C2E-43E3-B7F0-8C2D475AA728","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c15b367ae67621962a2dd23d164a19c1765a25bb","datavalue":{"value":{"entity-type":"item","numeric-id":4023471,"id":"Q4023471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"02c4dd244619dc3085d2e6bca03a1ac8e249134d","datavalue":{"value":{"amount":"+0.801760733127594","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":"Q6488526$8614245A-AB76-4911-AB55-ADB98F949EC7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"66cfe833b200e2892ad65263b6548fcb16588766","datavalue":{"value":{"entity-type":"item","numeric-id":4858951,"id":"Q4858951"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"36b3ce4a16d238bb5a22062f8afe2016d95623aa","datavalue":{"value":{"amount":"+0.7852089405059814","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":"Q6488526$D40BC019-0203-4010-B8C7-40F1B0610EF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"25b7aa2bce2a81296f4432af903ffab266b5f8fd","datavalue":{"value":{"entity-type":"item","numeric-id":3805959,"id":"Q3805959"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7ec6ac37b15bf09062a9a8b6b572435aebfbc0db","datavalue":{"value":{"amount":"+0.7838963270187378","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":"Q6488526$314FF9A7-8898-476F-829E-FBA6417F9E1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a84e644170331a6a9485b207c047e686cd4d5525","datavalue":{"value":{"entity-type":"item","numeric-id":3826528,"id":"Q3826528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4c9b69885776bc5696afcc3db14c139cc87dc4c0","datavalue":{"value":{"amount":"+0.7793048620223999","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":"Q6488526$09E3DCBD-FC0E-4CEA-AD41-47A5F5BBE70E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6488526","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6488526"}}}}}