{"entities":{"Q6108812":{"pageid":13243119,"ns":120,"title":"Item:Q6108812","lastrevid":47868640,"modified":"2026-01-02T22:39:31Z","type":"item","id":"Q6108812","labels":{"en":{"language":"en","value":"Formalizing Some \u201cSmall\u201d Finite Models of Projective Geometry in Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7704983"}},"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":"Q6108812$CE7F3053-2177-4433-ADDD-2E505CD9CCC4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c9686b0697314f845f0d68a62b33f0b701e91785","datavalue":{"value":{"text":"Formalizing Some \u201cSmall\u201d Finite Models of Projective Geometry in Coq","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6108812$66AD3132-7426-4BED-993C-243021A556B6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"49ca72c1dbd69dde11b19d20584c8ab138f7efd1","datavalue":{"value":"1515.68349","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6108812$F8356631-9816-4DA0-8987-67FD52CEA53F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"9086eff315adbe5ec2bd338c39dd730d113832a5","datavalue":{"value":"10.1007/978-3-319-99957-9_4","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6108812$65909736-B73B-4C95-8F04-8EFB22265A09","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"296b44c0c7487db7cf7567934fe97965dd3e319a","datavalue":{"value":{"entity-type":"item","numeric-id":620244,"id":"Q620244"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6108812$D24EC796-1CDD-4667-A23E-59271EA433CB","rank":"normal"},{"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":"Q6108812$B516958D-7075-4CC0-AC33-A7C3B529E006","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":"Q6108812$80F116BD-E801-4D1C-AD1D-3A9E68805129","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d890af79c9ca3ac61d434a598eaae0d88b56c6ae","datavalue":{"value":{"entity-type":"item","numeric-id":5302894,"id":"Q5302894"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6108812$FBC7C92C-5397-4935-A1C6-3A6D2DB0B667","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"71476e68174ce61b1b2a41ccdbdaefb9b107de95","datavalue":{"value":{"time":"+2023-06-30T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6108812$0BBAA168-8EE4-44C8-B1CA-1AFACEDF059F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6108812$AD02D7D6-B4DE-4982-A470-D3C1E01E42FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d3fd9b3464d5377e9ea4754230e8e8757563cdcb","datavalue":{"value":"51E15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6108812$95FF2453-7FD3-4AC2-9D95-D02B7E3956AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"97436ffec0c1cb82ffc805c68f1388491dec22eb","datavalue":{"value":"51E20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6108812$50D1977E-4732-4DED-90B9-9B97597F3BE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6108812$13E0E773-741E-4798-97AC-789686EB7C84","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3e40ab1f7c71591255e7775c8a026252e2d2857c","datavalue":{"value":"7704983","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6108812$5A4F1910-FAD0-41B9-851C-775D15FF73A2","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q6108812$141DB5B1-A623-47D8-B243-A36C0AC341D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d62798ced101241ac0d5e46110e32d69e73a0c1a","datavalue":{"value":"proof automation","type":"string"},"datatype":"string"},"type":"statement","id":"Q6108812$99D7C195-D3C2-40E7-9A5B-E0F0636170BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1f269977a25fe087b7007d36378986cca32ece60","datavalue":{"value":"combinatorial explosion","type":"string"},"datatype":"string"},"type":"statement","id":"Q6108812$24CDECF8-F14A-4297-859D-922D91152500","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d48249d047d710b8bc54f2eade143c98e00faa5c","datavalue":{"value":"finite inductive types","type":"string"},"datatype":"string"},"type":"statement","id":"Q6108812$2F6B99DB-62DE-4255-BB23-C951C326CB59","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"619cec4664a98d8c81850d161b273c3520446471","datavalue":{"value":"projective geometry","type":"string"},"datatype":"string"},"type":"statement","id":"Q6108812$D012F1E9-B11F-4A71-A200-F0997AB7FD48","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2f3fec54e2b916afefffc7e2ee5ccefb811a12f5","datavalue":{"value":"finite geometry","type":"string"},"datatype":"string"},"type":"statement","id":"Q6108812$47BE605C-12E4-4C2F-8D8D-A0F77393DD77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ec6eb39c4252a727450e8bc8ec923ed1b608edc1","datavalue":{"value":"Desargues' property","type":"string"},"datatype":"string"},"type":"statement","id":"Q6108812$D0E126D0-B0C6-48AA-984F-0FA3B9B03ABE","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":"Q6108812$D73650D1-E378-43A3-B8A2-508A25DD7E38","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b8fbc483c4ef131fa9b4ca036896b7171e2863cf","datavalue":{"value":"https://doi.org/10.1007/978-3-319-99957-9_4","type":"string"},"datatype":"url"},"type":"statement","id":"Q6108812$A6CEFE67-9643-45F9-AE9E-CEE51CF81BC9","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ad5ce580126521c83fd0fca17204c8974278607e","datavalue":{"value":"W2888726077","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6108812$CEA2CD49-4A1C-4881-845A-C45FF34972CA","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"abd21664f7486d9fb3ffe2d0d2bed84c1a486b3e","datavalue":{"value":{"entity-type":"item","numeric-id":4354373,"id":"Q4354373"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6108812$871198F5-A467-4F79-8059-FA7516FF5148","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":"Q6108812$C4EA3CD5-7218-457C-8CD3-F44B38167408","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"56561891c6904c5a2dfd08a9117937b91fb7bf32","datavalue":{"value":{"entity-type":"item","numeric-id":4763522,"id":"Q4763522"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6108812$BAA64F5A-2B91-4A79-AA09-41FB6777BD31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2cb7dc4e540bfc1c1f9b3070e4d2e003f7057e7a","datavalue":{"value":{"entity-type":"item","numeric-id":4434670,"id":"Q4434670"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6108812$17CCF86A-26F0-448E-A1BA-79A46DE6D39F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ebb5074ee36ed9bb9d929040b0c1d4214893958e","datavalue":{"value":{"entity-type":"item","numeric-id":5836618,"id":"Q5836618"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6108812$E7BEBB8E-D990-4458-8CF7-944234AC6DCE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5296a1d08321e3fc28ff882325d64dbe74172a0a","datavalue":{"value":{"entity-type":"item","numeric-id":3003232,"id":"Q3003232"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6108812$C464CC2A-C743-4FBA-972E-79BA61E81D5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bc813c3420ba0b42fe4bea1f4208b1eb74e62860","datavalue":{"value":{"entity-type":"item","numeric-id":448975,"id":"Q448975"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6108812$F53A50A4-67D4-4A77-9372-FDDE967E9FFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0fc41f2b2a8aa0d1d1987dc920f043ef4c6d51ab","datavalue":{"value":{"entity-type":"item","numeric-id":3422215,"id":"Q3422215"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6108812$1F9918AA-251B-42AE-92E4-AAC9E75B2C5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d683fb2836ef8e0f33b304608f2624c55a5cf0b0","datavalue":{"value":{"entity-type":"item","numeric-id":5484515,"id":"Q5484515"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6108812$C592A748-6A09-46DF-B579-0B383B11A049","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"16c58bccac3eb8e167d77acc1c92ca853e7a5fcc","datavalue":{"value":{"entity-type":"item","numeric-id":2655326,"id":"Q2655326"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6108812$6139DED0-289D-4246-9F3E-860140902226","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d54bed5461dfeb3ada4aeb652d634bd759c55c96","datavalue":{"value":{"entity-type":"item","numeric-id":3003232,"id":"Q3003232"},"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":"Q6108812$7E126690-734B-4DCB-A89F-5791CE1AF368","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":"dae89ea28ad173800b9376ee3bc50776c3bb3d62","datavalue":{"value":{"amount":"+0.8546350598335266","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":"Q6108812$372904BE-D00C-4D4B-BE04-D867830CE004","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1ed32a4f5d8b518e0ac9f5003543d94b115432ff","datavalue":{"value":{"entity-type":"item","numeric-id":1924746,"id":"Q1924746"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"27527ef01a55438d18ef9793fe9f6290e3aaa071","datavalue":{"value":{"amount":"+0.8471398949623108","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":"Q6108812$BA4D2004-43B8-4CEB-906D-E7EAFB35A12F","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":"78831e615e035fde5b990f517f518b4ef2d7909a","datavalue":{"value":{"amount":"+0.8286571502685547","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":"Q6108812$27CD4DAA-077C-452E-AD37-6DB017386ADA","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":"6f183862a5e96f1bb1089a2bbf183535a531824b","datavalue":{"value":{"amount":"+0.7837026119232178","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":"Q6108812$65B09FCA-44FE-4B57-BDEB-6DBF286557E4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6108812","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6108812"}}}}}