{"entities":{"Q3003232":{"pageid":3013956,"ns":120,"title":"Item:Q3003232","lastrevid":51253997,"modified":"2026-01-17T11:29:29Z","type":"item","id":"Q3003232","labels":{"en":{"language":"en","value":"Formalizing projective plane geometry in Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5899972"}},"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":"Q3003232$169DC968-E0B3-438E-97AB-D76D8D25D93E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"42195446b93b59d7f9287cb19f0bb46f046e8f45","datavalue":{"value":{"text":"Formalizing Projective Plane Geometry in Coq","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3003232$BB454BC8-7EEE-48B3-9650-E7E886D370B8","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"818641987b04d0bc4293a20395d3585e5a58200d","datavalue":{"value":"1302.68246","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3003232$A6BBF27D-F326-44B7-A4BC-F1186F91C39D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d136d6d0dde741b795d8cdb5a23dc7b75f8b3237","datavalue":{"value":"10.1007/978-3-642-21046-4_7","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3003232$3927709C-67AA-4879-AD65-F51391821825","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"77d146ed87b25a3f218b4b3975707f6be569c62c","datavalue":{"value":{"entity-type":"item","numeric-id":448974,"id":"Q448974"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3003232$B55A120E-244A-404B-8EC6-7BA3C288F770","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7154e8ca53ace223b8c5be019b7f4f775aab0292","datavalue":{"value":{"entity-type":"item","numeric-id":294376,"id":"Q294376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3003232$913D67C6-4C3C-4048-83FC-0C3A4D5EFE5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c4f67aad00a911cdfd4a5f73b3962a1f5be1f7e5","datavalue":{"value":{"entity-type":"item","numeric-id":294371,"id":"Q294371"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3003232$51AB74D3-BB0C-4593-9D8A-8FB787EB5AD9","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"348c28e159850115a4bf602bf9df1d1e5c1cbebe","datavalue":{"value":{"entity-type":"item","numeric-id":2849503,"id":"Q2849503"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3003232$37DEE644-1081-4B71-AE72-DAE42D92FAFD","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d0d41ce3332fcf97fd23ad798d4a05a02b8284bd","datavalue":{"value":{"time":"+2011-05-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3003232$99F321A5-1E78-45C2-8AA1-AD78DC5B434E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3003232$4D514728-3955-4013-8581-068BA3887C27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4e0e8c7d6615f164a0f34e5ca0ec887e89f48671","datavalue":{"value":"51N15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3003232$CA5FC716-C134-4E1B-99CF-CCD10F1F772F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9700d9c9373e96f28fcbbfbc6e4396eb8c646cec","datavalue":{"value":"5899972","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3003232$4C1294EC-5217-4B6E-9F86-22C74173EC8A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d5ef51b89dbf72f7181f6b41896d9233a3e6b1ce","datavalue":{"value":"formalization","type":"string"},"datatype":"string"},"type":"statement","id":"Q3003232$E3A51D63-79C5-440A-A7C0-77CD7DA767ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"619cec4664a98d8c81850d161b273c3520446471","datavalue":{"value":"projective geometry","type":"string"},"datatype":"string"},"type":"statement","id":"Q3003232$0EC452CB-09CC-45A4-B3A0-97812CF11E49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d1ecf978a28e5d1baefdbd10dbc4f102a6158a13","datavalue":{"value":"duality","type":"string"},"datatype":"string"},"type":"statement","id":"Q3003232$A6F9C19D-D9CF-415C-93FD-1E7FF8ABC5E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q3003232$76866ED9-A95F-44D0-BDFF-0E853D7669C1","rank":"normal"}],"P1463":[{"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":"Q3003232$AA9D2483-6B67-43E8-9872-43AAA8E91C9D","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":"Q3003232$3E4760DF-CF5B-4101-AA2D-BF72E8173C99","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c9718a6a6488c83cd10bf28f84ffe07eaecbe882","datavalue":{"value":"https://doi.org/10.1007/978-3-642-21046-4_7","type":"string"},"datatype":"url"},"type":"statement","id":"Q3003232$D502DC16-9868-4343-B984-771ECFC959F4","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"fdfb5792d1b426847828fbb4fb9b00b3964088ea","datavalue":{"value":"W1572941424","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3003232$A6D1AAD6-6777-4776-BC60-736EEDB1A8B1","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"adbf9b5719c13218db616f95f2a4a5f325af358f","datavalue":{"value":{"entity-type":"item","numeric-id":6108812,"id":"Q6108812"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"18dfc76074cf30ca26875c08de846478392dc296","datavalue":{"value":{"amount":"+0.8910681009292603","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":"Q3003232$2FA0F339-7F01-4161-A409-9EFDD23E6BA9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d3648fbe773481fa8147015af9b6ede0a3db1ed7","datavalue":{"value":{"entity-type":"item","numeric-id":448975,"id":"Q448975"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"59944297738486900667ba9aa92efa5aef29dd77","datavalue":{"value":{"amount":"+0.890132486820221","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":"Q3003232$F1A2FF5B-0051-47B2-B99E-0FA28A0C919B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b1bf28bfe52028ed618bbaa8952574102140b299","datavalue":{"value":{"entity-type":"item","numeric-id":2631964,"id":"Q2631964"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"acbe3b0a75dedd927e19e056553f8659a32d1cab","datavalue":{"value":{"amount":"+0.886109471321106","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":"Q3003232$D3A82FEA-7DEC-44DA-AE8E-F3A8B0DB0541","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6ac2b964c4fb8308af8ebc827cd48f5ed10e00c8","datavalue":{"value":{"entity-type":"item","numeric-id":2333313,"id":"Q2333313"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2db62978ac9a1b968d77569485aa5bb345bf8985","datavalue":{"value":{"amount":"+0.8483896255493164","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":"Q3003232$E5197E02-464A-4E33-936A-EE16EC787949","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e17806c70270f139697ad9b10ec0e5c8afe8d1d1","datavalue":{"value":{"entity-type":"item","numeric-id":1640646,"id":"Q1640646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"585d4d46e2bd31ab4d338ecefa0f11bb968e1991","datavalue":{"value":{"amount":"+0.8318252563476562","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":"Q3003232$3C2D08A3-D8E0-4B00-801D-E285BA371E55","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3003232","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3003232"}}}}}