{"entities":{"Q5000334":{"pageid":7029911,"ns":120,"title":"Item:Q5000334","lastrevid":54043433,"modified":"2026-01-26T03:48:33Z","type":"item","id":"Q5000334","labels":{"en":{"language":"en","value":"12th international conference on interactive theorem proving, ITP 2021, Rome, Italy, virtual conference, June 29 -- July 1, 2021"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7370959"}},"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":"Q5000334$06C734B2-C76A-4AF6-B37F-BF010575C03D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"7e872ec6be24fbd61603baa1da3c382b66d45735","datavalue":{"value":"1465.68016","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5000334$5EFA40C9-05EF-40C7-B913-B1AF7E895CCF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b168cbdb70f056f1ff9fc87d7bff79f83c6e09a3","datavalue":{"value":{"time":"+2021-07-12T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5000334$0C0EB6B2-7E1C-4299-AC87-625C2F1C98B3","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"1a69847d8cd1567017e1f77c4e7ab7b3b57c5f57","datavalue":{"value":"https://drops.dagstuhl.de/opus/volltexte/2021/13894/pdf/lipics-vol193-itp2021-complete.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q5000334$22EC81B7-0401-459C-BBBE-A2BEA1CB27F6","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"ed293b811733fa9438a72e1b6ba5680a0d2aac9e","datavalue":{"value":"68-06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5000334$525E824A-647A-403F-B225-C990E257695D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5000334$EAD2A92A-CE57-42A3-8C13-039D773B8511","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6f2c17db95e93f9a5a19ff6c68b3a1df8b0c021e","datavalue":{"value":"00B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5000334$65BB2EE3-1532-4F2F-9415-C5E5576144DA","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"49361187993485dc33ba4c9b94745683c2503252","datavalue":{"value":"7370959","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5000334$DAAC9CD6-C321-4770-B684-EAFF0AB7AD6D","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":"Q5000334$3C33E05D-E6A8-4F8A-ADEA-124F41E4ED0A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"956f1e784a601b99489b8568bf70a16e07aa6846","datavalue":{"value":"10.4230/LIPICS.ITP.2021.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5000334$D6B331F9-F577-479B-AABB-556FB5CF7567","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5dcdd717f1786c3858a3c0b3e9a930ec7da13cf0","datavalue":{"value":{"entity-type":"item","numeric-id":4994500,"id":"Q4994500"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f8d2dffb33c838b2fa12fb222f5999405f2f556c","datavalue":{"value":{"amount":"+0.7370908260345459","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":"Q5000334$D45CF006-75F1-4CC6-BD73-4682FD985F03","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"14f81f78dc252cf9fbec5abdeab0e8bf758ffed9","datavalue":{"value":{"entity-type":"item","numeric-id":2049504,"id":"Q2049504"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4e300edb2396fb677acf1b4f8364d836c33d9b8c","datavalue":{"value":{"amount":"+0.7342585325241089","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":"Q5000334$E24BED93-3B10-4FC7-ACAB-E28B51BCB156","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5c2557ccafea795ca9d1b67b8e8b12cc70f4f8f8","datavalue":{"value":{"entity-type":"item","numeric-id":2049503,"id":"Q2049503"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5b61e7c9cd24ff4308aa3c8a8e934104f9ae451f","datavalue":{"value":{"amount":"+0.7338933348655701","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":"Q5000334$DFB9172F-A105-4C07-9839-DB25EA8536E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"94dceb33d32a6ce1739308a1eea07ebd9cdecb06","datavalue":{"value":{"entity-type":"item","numeric-id":822930,"id":"Q822930"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7f9c7782de36f19c7ee16d6b09466323b4ce7f3d","datavalue":{"value":{"amount":"+0.7196320295333862","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":"Q5000334$6E21D1D4-5493-4DD9-AF1F-4E6E4EBF7FC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a59dadb88cb8be93c3aec77d3d07d8a294274d49","datavalue":{"value":{"entity-type":"item","numeric-id":2310769,"id":"Q2310769"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"627589a62a164fcbe07bd8a09b70522f15fcef59","datavalue":{"value":{"amount":"+0.7109320163726807","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":"Q5000334$5844B5CD-0E7F-4CE3-A8A8-918030C98816","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5000334","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5000334"}}}}}