{"entities":{"Q5900690":{"pageid":8006918,"ns":120,"title":"Item:Q5900690","lastrevid":50958506,"modified":"2026-01-15T22:40:42Z","type":"item","id":"Q5900690","labels":{"en":{"language":"en","value":"Theorem proving using lazy proof explication."}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5695378"}},"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":"Q5900690$1FD02A28-E1DB-41EB-A94F-3F413062ACAF","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"73bd069b212797cd1b716ecedbde3c2b856d1f40","datavalue":{"value":{"text":"Computer Aided Verification","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5900690$D4B491AD-1FF5-49FC-B68F-D8F1BF299F51","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ac1d6c888a15cd861d23bc613272dfc3e86a1aeb","datavalue":{"value":"1278.68259","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5900690$C5DCAC96-8EB9-4F11-842D-0443C958D9FA","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"38126dc183098febb961ba3435b28eb28edd09c1","datavalue":{"value":{"entity-type":"item","numeric-id":557791,"id":"Q557791"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5900690$FD18DC7C-61F9-438B-B17D-7298A5E6FC5E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4e6f417f09c985107129e25aec6563cc542c4012","datavalue":{"value":{"entity-type":"item","numeric-id":457248,"id":"Q457248"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5900690$C23E118B-43A5-43E7-9797-16809BCFF76B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4ad467815e869a9a01b5c6d6ab4b4dcfe8fa7e66","datavalue":{"value":{"entity-type":"item","numeric-id":2751854,"id":"Q2751854"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5900690$C3B16410-953C-4D95-8AA9-25B36551078F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c19976f280af2a9432c2c51239959366e237e59c","datavalue":{"value":{"entity-type":"item","numeric-id":598817,"id":"Q598817"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5900690$957CE282-8C70-4656-8011-E11FCAA3FA58","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":"Q5900690$F2E75844-407F-455C-BD39-C0B0715CDF6D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2c61bb6d282cc95675f5b726985d020f8b0e6f23","datavalue":{"value":{"time":"+2010-04-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5900690$CA40BFC8-DFE0-4DE2-8C03-8A2E04116D39","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5900690$609225D5-0392-42A0-827C-1B3AFC5468E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5900690$8979263F-F4CD-4826-A5C8-FF4B307F0C46","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f83d173b45a7f8946331bb579f15023192ef1b63","datavalue":{"value":"5695378","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5900690$0DA6E4AD-3E7F-4379-B834-FD2CFD8AF490","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"5834864074172f90c0db592b61fbce75f9303a03","datavalue":{"value":{"entity-type":"item","numeric-id":16627,"id":"Q16627"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5900690$43FBE7D3-1B45-472C-811C-823BC28E5E23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2822825cdea331aa7c0ec2c340c1eb36d62db00b","datavalue":{"value":{"entity-type":"item","numeric-id":17123,"id":"Q17123"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5900690$B302597E-F140-4A7D-B37B-34FAAC217BAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"478f9061f14e098e3fdf3fe3667d3a7084c42e61","datavalue":{"value":{"entity-type":"item","numeric-id":18982,"id":"Q18982"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5900690$6DB3B4A7-CAAA-4736-833C-0531421E95EC","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":"Q5900690$38D1E83E-65C1-4B0A-9538-F12DED83CEE7","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"050caeb9facfc2b37142c301b40d1dfd9dbf1be9","datavalue":{"value":"https://doi.org/10.1007/b11831","type":"string"},"datatype":"url"},"type":"statement","id":"Q5900690$F0845800-4BC6-442D-91BF-7CDD4AAB2240","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ca9b9df0d9ff4e5d8e3d66da51426dae32b7ea5b","datavalue":{"value":"W1571340194","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5900690$BE5785A1-B844-490F-8752-A1F815883898","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"0bc3be280ea47ce2c61f3b7e2b376b1d1ce60a5c","datavalue":{"value":"10.1007/B11831","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5900690$3FBD976D-206B-41FB-93B8-AF7A22A2A223","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2d4be7d7978e80bb59263872b297862b5cb916f8","datavalue":{"value":{"entity-type":"item","numeric-id":4809077,"id":"Q4809077"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"532509e9ef3a193ba6fd976a06a7fbaaae24bad2","datavalue":{"value":{"amount":"+0.7868903279304504","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":"Q5900690$946F74C7-66D8-4358-918B-F375C5A931CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ee9666d9095ca892169a9512aee8dbcd8fbe4f61","datavalue":{"value":{"entity-type":"item","numeric-id":5312942,"id":"Q5312942"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"71c85b19e11d8d9ca030dc84fc79bc51fce4ecc8","datavalue":{"value":{"amount":"+0.7550008893013","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":"Q5900690$BA7BD4A7-6BCB-49D2-9BD7-C5784BAB43AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8ca11e31f171093630925d50733f9af1acd317b4","datavalue":{"value":{"entity-type":"item","numeric-id":2870323,"id":"Q2870323"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e582dcea51b8b5a0519cc6927d6c33a6ca7dc878","datavalue":{"value":{"amount":"+0.7513775825500488","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":"Q5900690$05F58C24-63A1-458E-B542-4AD2DBC3149B","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":"9f53b76990e35e96658f2576f84d315a0552b986","datavalue":{"value":{"amount":"+0.7445918321609497","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":"Q5900690$362891FF-16F3-4E78-959D-88339EC4A63E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5fe2500297f15417006abf8b451f8fc6bb1190f4","datavalue":{"value":{"entity-type":"item","numeric-id":1309245,"id":"Q1309245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"be9fc812a17b0b7ec9ffa7edd72e77e5bfbe8b66","datavalue":{"value":{"amount":"+0.743164598941803","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":"Q5900690$9D8DEEA8-7588-4FF1-91B3-431F512C3AFE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5900690","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5900690"}}}}}