{"entities":{"Q5505513":{"pageid":7535073,"ns":120,"title":"Item:Q5505513","lastrevid":50550290,"modified":"2026-01-14T09:03:59Z","type":"item","id":"Q5505513","labels":{"en":{"language":"en","value":"Combining Isabelle and QEPCAD-B in the Prover\u2019s Palette"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5498237"}},"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":"Q5505513$F582477A-E378-47F6-AFE7-4E9CC81D4C3E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"87edddb907b2d4a21ba50dd723564691ab4d1e9c","datavalue":{"value":{"text":"Combining Isabelle and QEPCAD-B in the Prover\u2019s Palette","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5505513$E0AD0669-D549-45E3-B55A-F1CF41CCC4EC","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"cf2bd10232d6aaacd1224e33141f16699466bb49","datavalue":{"value":"1166.68351","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5505513$EF34AE81-5244-40D3-8BC1-2F6B9AC55CAA","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"957147cd1fb2f6a33aa1bce4d8dea4ae73907ad0","datavalue":{"value":"10.1007/978-3-540-85110-3_27","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5505513$B40A725E-C562-441E-8D7C-E93D3B882A11","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a20ba0f830157b69065a87d58c4f41556bd7f709","datavalue":{"value":{"entity-type":"item","numeric-id":3559772,"id":"Q3559772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505513$C87E71A1-5849-45AD-8EDA-4FFAB628080F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8d78e8b1fd2bada0896418639974db329feb4fe3","datavalue":{"value":{"entity-type":"item","numeric-id":2102945,"id":"Q2102945"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505513$70F956C8-B0AB-45FC-815C-A0797FFB0659","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":"Q5505513$6FE60A3F-95C7-47EB-82B6-0315F60DF3BC","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"51e6c39ac6ec91b8381a06fe1e16cf5aca0f2bdc","datavalue":{"value":{"time":"+2009-01-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5505513$EE7AD4AF-DAC3-4EF9-9293-B13C20CC57D7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5505513$B3BBBFE5-1B30-4B16-9F17-99762F02A92F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"22839c51fa81bb014e3c8e2ab8a9fc05ce8f567e","datavalue":{"value":"5498237","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5505513$D8549B08-9BD2-467B-BCB3-3CE49EFCBC6B","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505513$493EE1AC-B847-4961-94EF-A23563B3BBD4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3c22b4e6c24037f313b1837c22cc6ae0308a77c7","datavalue":{"value":{"entity-type":"item","numeric-id":13503,"id":"Q13503"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505513$8BEEA1C5-9985-4133-B878-F9F90500FEC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"25ab810b26d873ddbfbbf9d419fe20355f2f315a","datavalue":{"value":{"entity-type":"item","numeric-id":13570,"id":"Q13570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505513$65BF37EB-6B90-4CC4-9E2A-F72E7612AA82","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c62f005e0d35aadf822b20988439b932534d85d7","datavalue":{"value":{"entity-type":"item","numeric-id":13537,"id":"Q13537"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505513$58414068-1CA1-45C1-957C-DFEAFEA4D21D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"261ae6dfeffd96c9ea238e124055221c78337064","datavalue":{"value":{"entity-type":"item","numeric-id":13705,"id":"Q13705"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505513$946306B6-3213-4129-8992-FFFCFB2DEBD9","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":"Q5505513$6BF02ED2-AE5D-4437-AE6A-9D63838C8733","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"cdcc0bfabd14bdd646876906a05685210dfba2f9","datavalue":{"value":"https://doi.org/10.1007/978-3-540-85110-3_27","type":"string"},"datatype":"url"},"type":"statement","id":"Q5505513$5141775D-CEA9-4214-93B1-54782B922FF2","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d7e651ed3a3665904feb21e3fce33e7977d16dd9","datavalue":{"value":"W1507490915","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5505513$AB598BCE-B4A8-4BFA-94A0-D1CC22F226DB","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b7be2d05c20413feb6443e1b1af122bfdc77cfe","datavalue":{"value":{"entity-type":"item","numeric-id":3498456,"id":"Q3498456"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505513$D66613FB-4130-405C-BBB2-7DE07171E207","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e8910a816017d823e1c2ea267ab4a7baedcd6f69","datavalue":{"value":{"entity-type":"item","numeric-id":5428268,"id":"Q5428268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505513$CAEEB3EA-F633-4F06-8445-F1BBE7DEA2DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"19121fe5036f2676946186c6f9a088bb5b461d0f","datavalue":{"value":{"entity-type":"item","numeric-id":4227289,"id":"Q4227289"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505513$1FBEDBFC-0783-47A2-A181-18804813BC2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"017dca64578e6979a09aeeb8b382b1388bace1b7","datavalue":{"value":{"entity-type":"item","numeric-id":4810199,"id":"Q4810199"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505513$58D8C695-CFC0-405D-B8C8-AF1878DA8BA9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df9fb4bc160a2caa739ce4a3c250258344d6a7c4","datavalue":{"value":{"entity-type":"item","numeric-id":2729073,"id":"Q2729073"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505513$F95907B5-431F-4971-B1C1-F24065AE513D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2837eb28569a008677bba2643bbc6df5d206bee8","datavalue":{"value":{"entity-type":"item","numeric-id":4247790,"id":"Q4247790"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505513$DAD9D53D-1089-468F-8579-D39F14EA57A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d43a848f856e7add83e6907744bb466bc863e38a","datavalue":{"value":{"entity-type":"item","numeric-id":5394621,"id":"Q5394621"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505513$5EFC5DAB-A8AD-4A5E-9ECF-1BAF633A4454","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8e5d997d3c3c1c4cbe0d251137694980cd98cf08","datavalue":{"value":{"entity-type":"item","numeric-id":1272607,"id":"Q1272607"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505513$3A2EC459-60D7-4B93-98B9-136BED4F028A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"08eaa6c03390b94af9efd4280f970d5d0809ce58","datavalue":{"value":{"entity-type":"item","numeric-id":1186711,"id":"Q1186711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505513$03DFDC38-3633-4C15-92BA-EE189D1DFDBC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cc5bac2a1c3bf09f6471a60799fa53f4bbb721a1","datavalue":{"value":{"entity-type":"item","numeric-id":5428262,"id":"Q5428262"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505513$6373D9B8-5540-4127-A567-E4C51C43EFE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0bd0fc8e1eccde465b8ad59a4b0fe16a5a8a39a0","datavalue":{"value":{"entity-type":"item","numeric-id":1272609,"id":"Q1272609"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505513$447F8E84-0062-4DF4-B92E-AC763F8A85A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7ff600c639285bb06593ca61942b0f485ac06878","datavalue":{"value":{"entity-type":"item","numeric-id":1202183,"id":"Q1202183"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505513$96B0E30F-F931-49DA-979C-56A6E54D8C27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"79bfc697d8da1639edfa9171984fbef54e299a56","datavalue":{"value":{"entity-type":"item","numeric-id":5493316,"id":"Q5493316"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505513$7EBED89A-5C50-44B1-9B85-ED40AA4BE9CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c00ecccc176b971f8f655f17f279ab75b6423f0b","datavalue":{"value":{"entity-type":"item","numeric-id":2432769,"id":"Q2432769"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505513$C7D4CA66-5629-4B2B-902A-7E1A6F4043CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a10bbeb6c6903ace983b2dbf286a2ef4e5b248ab","datavalue":{"value":{"entity-type":"item","numeric-id":1331625,"id":"Q1331625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505513$4ABB79C9-D426-415F-A211-A464877E2372","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c8be9375a315209f41df1b38374a5e7e956d28bf","datavalue":{"value":{"entity-type":"item","numeric-id":5807665,"id":"Q5807665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505513$C37F6D42-DAAB-447B-A7ED-060AD31ADDBC","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fbc9d0942e84fb7a62e503e275b2c81263df97e5","datavalue":{"value":{"entity-type":"item","numeric-id":5170239,"id":"Q5170239"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"85f0f8ec286962e1e9caa621c39201fa7e230d9a","datavalue":{"value":{"amount":"+0.9032220840454102","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":"Q5505513$CCCE99D0-0F69-4F53-867D-BC5FD6EFC5AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"404825eb196e28e9cdb897322b5b207a1e9328bb","datavalue":{"value":{"entity-type":"item","numeric-id":4790649,"id":"Q4790649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c7592dbdfe7a57cf424843b2b6692c7348ad5657","datavalue":{"value":{"amount":"+0.7458913922309875","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":"Q5505513$2E604BB9-99D9-430B-97C8-FAAA95BECFD3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0f16aadc6cf54417a3910e3f401c2c1c02bdb63a","datavalue":{"value":{"entity-type":"item","numeric-id":4934138,"id":"Q4934138"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5637cb0dfd80911c9740f176649cb0afe31093fc","datavalue":{"value":{"amount":"+0.7217898368835449","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":"Q5505513$9E96A12D-DAC2-44DF-8713-9CA9533E017A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"633f5109f061dfddda51f045da9e8b0fa4ee5413","datavalue":{"value":{"entity-type":"item","numeric-id":5899057,"id":"Q5899057"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5637cb0dfd80911c9740f176649cb0afe31093fc","datavalue":{"value":{"amount":"+0.7217898368835449","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":"Q5505513$B49671CD-E1F4-4BD4-8A10-1CD4911C62E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d6958c32e58988a08693ac87970e050d9d1ca1fc","datavalue":{"value":{"entity-type":"item","numeric-id":1272607,"id":"Q1272607"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"df0cb6f025bde0f4eabac3131fff9db7454ab241","datavalue":{"value":{"amount":"+0.7207697629928589","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":"Q5505513$C76A1EBB-7BA1-47A3-8294-D99E91F34467","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5505513","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5505513"}}}}}