{"entities":{"Q5717444":{"pageid":7746998,"ns":120,"title":"Item:Q5717444","lastrevid":38740082,"modified":"2024-12-11T09:09:37Z","type":"item","id":"Q5717444","labels":{"en":{"language":"en","value":"Mechanizing Mathematical Reasoning"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 2244726"}},"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":"Q5717444$365C0E20-906D-42BA-9FA8-32A1BC8F7D56","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"72fe85e01709f12944d8ecd77a8d9733a0d516d8","datavalue":{"value":{"text":"Mechanizing Mathematical Reasoning","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5717444$3A16768B-962D-4199-96AF-829163EAE330","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"75753adca763f749b0c831c5cf197dcfc668c341","datavalue":{"value":"1098.68632","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5717444$3C63B35A-5B29-458D-9868-FB07DFBFAE7F","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5717444$52E63232-2B0D-418E-BA68-00304CCDC9C8","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0e93cf8dacd1ede76e69913529f9bf4e8192e151","datavalue":{"value":{"time":"+2006-01-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5717444$0A576E5E-1B49-4B11-9C5B-CDA1C2F447D2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"344f62a15ccd40e690364bd758985e8313f47f4a","datavalue":{"value":"68R10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5717444$791BC7BF-EC26-47C1-A0EE-D772DA400065","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"810d660658648f9bc3138c1cd0aba8029bb9050c","datavalue":{"value":"90B06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5717444$A90AAEBE-E709-41F5-8FA2-2C10CA42CB82","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d2d4f4e28fa9ca38421c473fcb6ba728a44de59a","datavalue":{"value":"90C35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5717444$8821288F-545A-443B-B6D6-49AD197C0BBC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fdd9498216d1fd2eff80e5a7d18782b649eb7b2f","datavalue":{"value":"68Q25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5717444$8FDB750E-7DB0-4261-9C3F-617671BC8376","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5717444$DDDF116E-D76F-4C92-9D4E-300AD28078EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d5c83f057600e5614b7fec59c8e4ac61cb41ba8d","datavalue":{"value":"91A80","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5717444$35B3C9F1-C501-4C10-B802-510BDE2B8F26","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3ff53188c47b81fafbd30f9b078e0382ae733219","datavalue":{"value":"2244726","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5717444$72F65C82-4AE9-4B2F-984C-7089BCE1518E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cff4611211e7993ef5cb2fffeb0e45036a9eba0d","datavalue":{"value":"sabotaged Graph Reachability","type":"string"},"datatype":"string"},"type":"statement","id":"Q5717444$C9DA9EE1-5D2A-4FA1-8078-1B805725535D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e513e0e4a2f9fe9c2e9add88e515ac966218b3d6","datavalue":{"value":"Traveling Salesman","type":"string"},"datatype":"string"},"type":"statement","id":"Q5717444$7E5945A8-BE2F-4C76-BBAD-7295B51566D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"900449d9c111228b32b61aefc4917c5119284013","datavalue":{"value":"complexity bounds","type":"string"},"datatype":"string"},"type":"statement","id":"Q5717444$1FC50D8B-B454-4FC3-94BF-490D82A9AA6C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb9f8004d477a3922fe8bde53d670f8b57c48852","datavalue":{"value":"model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q5717444$50D4F321-A82F-4CD8-8128-F0A5DB40A055","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f1dda010537b7b36bd45151721146f720815706e","datavalue":{"value":"modal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5717444$8363F2F7-F4DD-4CBD-99DA-0DAE0B45FDDB","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a16bed3fcf9befde6b615ead23f4b855455a9900","datavalue":{"value":{"entity-type":"item","numeric-id":1246519,"id":"Q1246519"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5717444$8C786273-7B3A-46EB-A98D-1287C1EFC3CB","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":"Q5717444$11069EC8-3EBD-4515-9298-B9F9908407D7","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"703773b8d2bd6b8fbc89ad622e8566bce28b2e06","datavalue":{"value":"https://doi.org/10.1007/b106663","type":"string"},"datatype":"url"},"type":"statement","id":"Q5717444$DFC7DBDC-CA67-4650-B3AC-CDA3FE562173","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"15846dcb4b029236c46835509fa6b1f264866a57","datavalue":{"value":"W2484955858","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5717444$C3F693D5-6905-4404-9EA3-4AC92A275651","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"222aa4c71b9d7ceffdd56e5dd6ca1fc858b04bb7","datavalue":{"value":"10.1007/B106663","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5717444$8329ABA2-DF14-434C-85EA-CD573E29E40B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5717444","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5717444"}}}}}