{"entities":{"Q2441776":{"pageid":2452519,"ns":120,"title":"Item:Q2441776","lastrevid":74108433,"modified":"2026-04-14T18:23:48Z","type":"item","id":"Q2441776","labels":{"en":{"language":"en","value":"SMT proof checking using a logical framework"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6275291"}},"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":"Q2441776$290AE9BD-25EA-485F-9D89-6983A2270FCE","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"130465cedf52f3906700f0b7d35b0dd5ce19025b","datavalue":{"value":{"text":"SMT proof checking using a logical framework","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2441776$C27C6911-5D82-4FE6-9D97-D0F4EC220C48","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"e4155253633088fc0b10c5494c8dcb9515d237b4","datavalue":{"value":"1284.68521","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2441776$2EA4CCEA-A24F-472B-BDB2-971719826F56","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7daa8e19dd762c08a3fe86309cfbf3893a62423c","datavalue":{"value":{"entity-type":"item","numeric-id":286782,"id":"Q286782"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$866B03BE-3C0D-4315-A66D-C1C363E83AEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"af1f9ccd2a93b218960642acac4fd4c971fbba18","datavalue":{"value":{"entity-type":"item","numeric-id":2441774,"id":"Q2441774"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$7CDEF9D4-555A-4F7C-B42C-6F5C2B3F747F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"84952d23570c02a49b2cbd6b6731071617699380","datavalue":{"value":{"entity-type":"item","numeric-id":518398,"id":"Q518398"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$EB6EA4A0-0A3A-452B-8153-231C803E5A91","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"2cd201d4e9072c0558fc093a2a86e6ed9aceb4c9","datavalue":{"value":{"entity-type":"item","numeric-id":2441775,"id":"Q2441775"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$6DEA335B-B7D6-4E1A-9137-33DDD251A13D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"947e5398223830d4c80e75386dbd3c8e6dd67f1d","datavalue":{"value":{"entity-type":"item","numeric-id":429585,"id":"Q429585"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$7C9CB21F-062E-49DB-987D-4B4E3266F74C","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"70551fcc6e89042fc26ae9242a005533b44a2d7a","datavalue":{"value":{"entity-type":"item","numeric-id":169908,"id":"Q169908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$95750A28-B152-43B5-A66A-5C959956CA63","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b8e12da0e8bd681f94b625e1ea013bf02fcfebe5","datavalue":{"value":{"time":"+2014-03-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":"Q2441776$17555C93-E052-4913-937A-A9FD0445C36B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2441776$309986C7-62C7-4866-9196-448AC675EDCC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2441776$02283C36-121F-4D2B-AD5A-A4E3D937CE38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2441776$0146EBFA-F80F-4B2F-A6D1-AA9763BEC92B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"40d293f5d2161e80872b42afb12a3fc45e5d1401","datavalue":{"value":"68Q55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2441776$17670330-713C-4044-BD7C-9382BCE1053E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6cdf47ec6db89d4387d615f185d055ccae6f1a23","datavalue":{"value":"6275291","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2441776$6BF4FD60-75E7-4C31-804F-3C9AEC1BC9E0","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1254a7c01d2970b87da2854c1fde40c268a1f55d","datavalue":{"value":"satisfiability modulo theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q2441776$7212B3A4-8338-4EC2-9A66-1B77815DADDF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4a614927b0caf638748bb51c0de92c1b49104311","datavalue":{"value":"proof checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q2441776$159F2F9C-99F4-41C7-A9B1-89B386E8EFFA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ba03543f6eb8246f3663782c06e96c302c8beacb","datavalue":{"value":"Edinburgh logical framework","type":"string"},"datatype":"string"},"type":"statement","id":"Q2441776$38CBC8A7-3EAE-4DA6-8F1B-E252DA2913F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ed7dcb8860fe9a4dad338a041af2f059e5463519","datavalue":{"value":"LFSC","type":"string"},"datatype":"string"},"type":"statement","id":"Q2441776$B7199F92-B1C0-4245-BB70-5A8449590BE6","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6d1b503d7c8f19634e207574177819c306621855","datavalue":{"value":{"entity-type":"item","numeric-id":17038,"id":"Q17038"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$95425FEF-86D5-48E9-8FDF-3E2BE54448DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"5df14ee9c6f65085bdee53a419634b2235aa5c43","datavalue":{"value":{"entity-type":"item","numeric-id":19326,"id":"Q19326"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$E711438D-C7A4-4AEC-AAF2-0B6694E4E2A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f29f161a221c0bedeec97e9d4ad10664227f4777","datavalue":{"value":{"entity-type":"item","numeric-id":16290,"id":"Q16290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$6FA217A8-9CDD-4C1D-8835-157555E97516","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8312fa7309b2bb86919d80d9dd327b01ccd3eb19","datavalue":{"value":{"entity-type":"item","numeric-id":19268,"id":"Q19268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$DC714448-7264-493F-8CF5-06BF30399BD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$462FFC65-F1E3-4CA5-91F8-BAF93F9BED84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"602b32d79a3dd12c7713e80fb0597b8ab4375f08","datavalue":{"value":{"entity-type":"item","numeric-id":16614,"id":"Q16614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$303FB989-0EA1-40A8-A6F1-E595CF9E7A9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"875fd2341d7eaef60a26a549ea0c9adfdf328e2e","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$E3162EF0-CA19-4830-8E26-E9E4D1D77E52","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ea1fa890b2f09c8cd0bccb17957cf46696afec2a","datavalue":{"value":{"entity-type":"item","numeric-id":19731,"id":"Q19731"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$A165DDD8-0B44-40AD-B6A4-FC76E191B056","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3ac1e8c13c0130a75f4cf78841def0133e1a8ff4","datavalue":{"value":{"entity-type":"item","numeric-id":20425,"id":"Q20425"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$BDFA08E8-0019-427A-A77E-B7043C2C1EE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19db008058ce3a679389c190541b4b00e350555f","datavalue":{"value":{"entity-type":"item","numeric-id":27113,"id":"Q27113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$A3D523C5-A59B-42F7-8522-73AD2C2A68DB","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":"Q2441776$4AA27206-9E54-4777-B1ED-1DF70A28DF15","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ad7a8ca590655fcbd33965cb692125a4ce15d701","datavalue":{"value":"https://doi.org/10.1007/s10703-012-0163-3","type":"string"},"datatype":"url"},"type":"statement","id":"Q2441776$9BBF5DD0-4426-4CE1-B1BF-4E79ACCAE7AF","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ad72320b0f63c0ba8f59ead1503a6efc83c438d6","datavalue":{"value":"W2054859958","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2441776$EBD90417-4A8E-44A6-BAE2-2B762290B412","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"8d6521b2af4cfbacb55e12311cb9a04d48ea2141","datavalue":{"value":{"entity-type":"item","numeric-id":5899041,"id":"Q5899041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$585854CA-15BD-465A-B2DD-140B70CF742B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bb15445443b7a8677c7ef043ed8530f20d54b0c3","datavalue":{"value":{"entity-type":"item","numeric-id":3100209,"id":"Q3100209"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$9F2663D2-1CEE-4791-ACE7-613F2FEA62B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"516f1874c8ee0b4ec27c5e2e2791ec6f448a7313","datavalue":{"value":{"entity-type":"item","numeric-id":5493194,"id":"Q5493194"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$5D5052BB-B462-41E4-B0C0-85BBCE3B7A2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f3ea02b15a15931f4cd364dd4a0ce61e10ac225","datavalue":{"value":{"entity-type":"item","numeric-id":703860,"id":"Q703860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$64AB662E-EFC4-4686-8CA3-D635A06DC111","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"494aa31720bff090f87eabeb86ce7380ba058cbf","datavalue":{"value":{"entity-type":"item","numeric-id":5747649,"id":"Q5747649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$7B808078-01D5-4A77-AD20-AF483B8FE822","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9cdaa2ec8eceac1d3a0c164dd76be4ed6c68bc4d","datavalue":{"value":{"entity-type":"item","numeric-id":5946344,"id":"Q5946344"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$B72514C6-5303-424E-8185-82329A3DAC20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d2b783d0052b7f250a9573410e9be2b4624ef11e","datavalue":{"value":{"entity-type":"item","numeric-id":5899057,"id":"Q5899057"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$260002DF-794F-43E4-B8CD-90158E149AFF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c5d6321a3b15489d3ed6e73cf55ba5d79230f775","datavalue":{"value":{"entity-type":"item","numeric-id":4809071,"id":"Q4809071"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$4F5A8B05-619B-42D7-992F-C15A46A42FA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bb60c55290ccc2425872093c601ec557fb400edd","datavalue":{"value":{"entity-type":"item","numeric-id":5191102,"id":"Q5191102"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$F959EE1C-A2A5-44CB-9A8A-4976D32FED06","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"021e6e2184fd3d7f831680d56b426b95217eac7a","datavalue":{"value":{"entity-type":"item","numeric-id":4033837,"id":"Q4033837"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$97715DAA-8E08-4265-B0CC-630FC4714A54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ce3bb918603ae315ee0224631b7326b49acf86c5","datavalue":{"value":{"entity-type":"item","numeric-id":5899073,"id":"Q5899073"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$80F67894-6057-444A-BE94-6A41D5540893","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6063e4a144bafe1447ae8b10555347d26c418f1d","datavalue":{"value":{"entity-type":"item","numeric-id":3189797,"id":"Q3189797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$516D5649-EFF7-4ADB-8702-6BE848BBF13E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f2f77790f3de0e7a5198a8f1c64a8023dd2bee09","datavalue":{"value":{"entity-type":"item","numeric-id":5348912,"id":"Q5348912"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$FB64C865-92E3-4E39-8B2F-E361A7ACA734","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"839fe9e80ad88458f41a8a24be5284fc203e2e80","datavalue":{"value":{"entity-type":"item","numeric-id":606999,"id":"Q606999"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$29CC575E-502B-4F44-9242-AB5B45EF7107","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"348369ca3fccbe91226809a75cbf31afd7f3186d","datavalue":{"value":{"entity-type":"item","numeric-id":5900666,"id":"Q5900666"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$8F420330-F1E5-4BF5-9D18-30AFAC295291","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c22bde11e78369a6138771e56f2c61a2713ba27a","datavalue":{"value":{"entity-type":"item","numeric-id":5458346,"id":"Q5458346"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$D9F7710A-A9FE-4252-AF83-F246E6399AF2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d0ecda2530a74fd3b958fc170aad75894016b80e","datavalue":{"value":{"entity-type":"item","numeric-id":3541720,"id":"Q3541720"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$007F1FFE-E772-4BA6-9451-C44956818EFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4aa8869764d95275ff1256e74294386e198dd5f3","datavalue":{"value":{"entity-type":"item","numeric-id":4936138,"id":"Q4936138"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$8687B966-7B33-4BC2-929E-B97B8333A54F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7fe8cac8585e29aabc7a821fa20c965a2d68e7b8","datavalue":{"value":{"entity-type":"item","numeric-id":5178881,"id":"Q5178881"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$1EDA652E-53FB-4B79-858F-4FB207A75438","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"79db93a0bb311f56c816d6ffc92dd7b60e23250d","datavalue":{"value":{"entity-type":"item","numeric-id":3455223,"id":"Q3455223"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$FB6EA497-0A8C-4FD1-9B8B-20E95EEAF937","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$CF370C71-193E-4A8C-A375-943F829D55D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"309a715ecfe3fe3e4ec0e698ae13dce021cfc93e","datavalue":{"value":{"entity-type":"item","numeric-id":2724150,"id":"Q2724150"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$9BAC6183-F5CC-49F4-A96D-179EC20EC2ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7b1ef4c8566673a8a5c94d00ea3fc5ee04078d8e","datavalue":{"value":{"entity-type":"item","numeric-id":3506045,"id":"Q3506045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$96AA438F-432D-4B7B-B1CB-561947E4584D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"30da8148c90aaf17fe8a996c8559dd1f27b45ebd","datavalue":{"value":{"entity-type":"item","numeric-id":4809074,"id":"Q4809074"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$5AB8C64C-D0AB-4E1F-8792-43A484251669","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fa19d45127427927ec930c6ce8f8170b9db93184","datavalue":{"value":{"entity-type":"item","numeric-id":5712317,"id":"Q5712317"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$155551BE-4DDB-4424-96F3-3CADBFA65666","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"271326b3f6ba4699b8b9534f6c64338c8ddd3a50","datavalue":{"value":{"entity-type":"item","numeric-id":1006729,"id":"Q1006729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$CA9F4424-E6F4-4C4A-9F9B-23E010E9F92E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bbf7a93d9fd055f21d4bf9911f205499faf8d773","datavalue":{"value":{"entity-type":"item","numeric-id":4809068,"id":"Q4809068"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2441776$47DCAAB0-C907-4C60-94F5-D4CAA6651777","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4713dfeb3d4d2ee0b821b30e24b46dfa5420fe7f","datavalue":{"value":"10.1007/S10703-012-0163-3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2441776$6F434167-4E6C-478C-8419-46A152C8235A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b25840e9689e28a5767a31e8370e4b859c5091dc","datavalue":{"value":{"entity-type":"item","numeric-id":5458346,"id":"Q5458346"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e87c2b24fba1ae700305731b7358a85142d9b41f","datavalue":{"value":{"amount":"+0.8209550380706787","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":"Q2441776$277A15CA-5F9C-41B3-B495-D3C785235953","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d13a1aa7335cec291b0dfd74d25004b6bcf26c1d","datavalue":{"value":{"entity-type":"item","numeric-id":3460065,"id":"Q3460065"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"227cf5d145db489bb738a28b874a69b14638f8d5","datavalue":{"value":{"amount":"+0.773145854473114","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":"Q2441776$FA6432B5-21EA-4AD2-9E2D-8AE0F0F0D5B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"12a132e4daa2e15bd5dc269ad3507f16b279f28c","datavalue":{"value":{"entity-type":"item","numeric-id":1687744,"id":"Q1687744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d9726fbdae074899ba72b725b4489744d555e40c","datavalue":{"value":{"amount":"+0.7555729746818542","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":"Q2441776$D529174C-F985-4E82-A991-E7C79ECAFD0E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f1f943c54080b27de44312af7634875e7f707904","datavalue":{"value":{"entity-type":"item","numeric-id":5716582,"id":"Q5716582"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"217aa039fe1cf17e334a0745f81d9e1502f6416f","datavalue":{"value":{"amount":"+0.7554461359977722","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":"Q2441776$C141BA22-F231-4A11-9EFF-C40E8F26E524","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8738b00b1ca33051359a5e295052e5443121b0d9","datavalue":{"value":{"entity-type":"item","numeric-id":2164216,"id":"Q2164216"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"143b06fcd04f315bf3b107a9fa79aa9d7682be54","datavalue":{"value":{"amount":"+0.7509414553642273","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":"Q2441776$ABBF220D-C1AB-4697-9285-8C5A6C000489","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"SMT proof checking using a logical framework","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/SMT_proof_checking_using_a_logical_framework"}}}}}