{"entities":{"Q448980":{"pageid":450747,"ns":120,"title":"Item:Q448980","lastrevid":51550763,"modified":"2026-01-18T18:07:29Z","type":"item","id":"Q448980","labels":{"en":{"language":"en","value":"Designing and proving correct a convex hull algorithm with hypermaps in Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6080929"}},"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":"Q448980$8A99C83A-6E4C-4C66-96FC-492F1DE1EA5C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5cc5b5892a1fb7391757b2280b5b209a5da52824","datavalue":{"value":{"text":"Designing and proving correct a convex hull algorithm with hypermaps in Coq","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q448980$80D2C550-665F-42CB-A0E3-49E7892367F7","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f1e793e5c00e6c3f3c5e47fdcb1ba08d7f591698","datavalue":{"value":"1247.65021","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q448980$FB77670E-A434-46FF-A5FA-5B1521A7AB89","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8b355a9128566668fe86b87b08ecc54a6751f15c","datavalue":{"value":{"entity-type":"item","numeric-id":448979,"id":"Q448979"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448980$26832962-697C-4CF9-A412-0E059FB5CA24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7b9642534f304d9a98032df7352635c1aa31c0f2","datavalue":{"value":{"entity-type":"item","numeric-id":396465,"id":"Q396465"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448980$8382CD62-0892-47EE-97EE-70706F702201","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":"Q448980$4D7C49EF-7D14-475F-A80F-52BACA0E857D","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"285beb29e5e30a7ba8792191178d7f52682884ef","datavalue":{"value":{"entity-type":"item","numeric-id":175378,"id":"Q175378"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448980$B39CD5B0-10A3-4421-A3FE-83EFF99CF994","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5eb7c028e513adb70517d5dc7c8a025b4004820b","datavalue":{"value":{"time":"+2012-09-11T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q448980$505FCCC6-0CB1-4396-97A9-5979D4BBD32D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"2ce72165d993b0b8ed97728d731d2db2473b9554","datavalue":{"value":"65D18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q448980$508D70CA-0265-4B93-8791-1D9FE69DE8B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4844ecc2838b02f08a426d6ddfea94d07252b432","datavalue":{"value":"65Y15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q448980$54E7495D-1471-4BEA-8DC1-9BCE1837AED0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"fd589486cb58321b202bbd0368d3bbeb74093294","datavalue":{"value":"6080929","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q448980$D7BE6CFD-20B8-438B-8E29-58F873DEA916","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"697626a6c5ea4a7921eba4e0f3fdba17e2e290d9","datavalue":{"value":"convex hull","type":"string"},"datatype":"string"},"type":"statement","id":"Q448980$9B2B959D-7EC8-4571-8D32-8942F67EEE88","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8dc5992e44b20c9bb28dceede04bd8419143b6d5","datavalue":{"value":"hypermaps","type":"string"},"datatype":"string"},"type":"statement","id":"Q448980$89C63C77-6A0C-4C9F-A308-494E2BC39D43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2c7ac263324871a44dcbba67d80bbe91e299cc16","datavalue":{"value":"formal specifications","type":"string"},"datatype":"string"},"type":"statement","id":"Q448980$A8F9E639-98ED-4AA3-9896-4B94306BF05A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"83a4003069926cc612c694964e3cbdf707c8f2c7","datavalue":{"value":"computer-aided proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q448980$A04C8CD9-19F3-4D1B-BE54-697F56AF47C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ae6e62c84697a17d98f1da6fedd7e40013028a1b","datavalue":{"value":"Coq system","type":"string"},"datatype":"string"},"type":"statement","id":"Q448980$C682BD00-6762-4782-BEAA-DE8EE06B2E9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"551d108313cfab3a77b395a647aede7021169ebd","datavalue":{"value":"computational geometry","type":"string"},"datatype":"string"},"type":"statement","id":"Q448980$FE3D65AF-3F0C-4D96-8D8B-D7BE53722925","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"73bf07fb0985efe0166024eb806e5cf2244671a5","datavalue":{"value":{"entity-type":"item","numeric-id":18489,"id":"Q18489"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448980$DF9B7ABE-4FC4-48F5-95A9-DDBCBEB3496D","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":"Q448980$04AEC065-5F8E-492C-A5C6-0FB0B638894D","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":"Q448980$28349561-5AEA-429F-AAC3-F27449171932","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"44e1d38ad604ab0174774eb4779bf26094c1fdb8","datavalue":{"value":"https://doi.org/10.1016/j.comgeo.2010.06.006","type":"string"},"datatype":"url"},"type":"statement","id":"Q448980$8C701642-A3AF-47D8-9514-92B9A610628D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"8b0a4934ef61dfeb5089e04615f24195674eecd4","datavalue":{"value":"W2166210250","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q448980$2CF54C80-B1FD-4144-BDAB-E2AAD61E67BB","rank":"normal"}],"P223":[{"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":"Q448980$09C0757E-1848-4482-9F4C-051E0E55A05B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2bc8d159e33e0b9cec2c132fd576f1962fb82116","datavalue":{"value":{"entity-type":"item","numeric-id":1868507,"id":"Q1868507"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448980$065CE2CD-FA9F-41E7-9957-7B54F77FE99F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"25fa1198b80017739f0fdb556bd9257106df7653","datavalue":{"value":{"entity-type":"item","numeric-id":4217293,"id":"Q4217293"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448980$CDD2B2A1-03B4-42C6-AB5E-96F52F760BD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cf540dac72bcd5ec964f271bd4451af06502cd55","datavalue":{"value":{"entity-type":"item","numeric-id":4071773,"id":"Q4071773"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448980$2B3BE233-D173-407B-A29D-13408D15E9D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3bffe48c7c76b90bf68970921698e19786e1600b","datavalue":{"value":{"entity-type":"item","numeric-id":2747613,"id":"Q2747613"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448980$DBDF9182-FA33-4208-B1EF-8B5DC0AD5BCA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4241f8308d167565bbead4d0eec3525ac106e02b","datavalue":{"value":{"entity-type":"item","numeric-id":5452284,"id":"Q5452284"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448980$4A65CE0E-36EE-4E24-8BA4-D0533CEC2037","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62b779ecca4f2c81aa34d372723ce74f8abed7b3","datavalue":{"value":{"entity-type":"item","numeric-id":2643883,"id":"Q2643883"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448980$2B17FAD3-B214-42FC-99CA-6D0B6F3A46CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3554b70a34d910ef7cc4793e9bfe42975ffbbc28","datavalue":{"value":{"entity-type":"item","numeric-id":4910724,"id":"Q4910724"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448980$CE0E3F10-212E-4394-83F6-44C608E9F00F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ee21c0df1cd1ed20706890eebef9c09dbf7c7e70","datavalue":{"value":{"entity-type":"item","numeric-id":944364,"id":"Q944364"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448980$F7B6AEFE-50AC-4EF6-AB45-C6417AB5058F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6930b5d30b40008083479f898f52bf6f3f2e4aed","datavalue":{"value":{"entity-type":"item","numeric-id":839032,"id":"Q839032"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448980$DBE4B0B4-1004-46AB-8A25-0835761461D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"25b026e498c7466f890693e678f90760ff4b1c4e","datavalue":{"value":{"entity-type":"item","numeric-id":3772828,"id":"Q3772828"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448980$D49E9626-527B-462C-A72C-CDF3C3263D7B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7d9190693f3924b86be7203c014f0b8b161bc6f8","datavalue":{"value":{"entity-type":"item","numeric-id":5302559,"id":"Q5302559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448980$76C0064B-0E6B-4BEB-B4B4-9E4C794CB332","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d43f11a5e6fc21caa581e9ac1e35682b1839d73e","datavalue":{"value":{"entity-type":"item","numeric-id":3075246,"id":"Q3075246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448980$BD55EE0C-B87F-4D1F-B212-DC4B5C6CE19D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"53a8687c0d1c36ee83f5185757ea9d3953bc19bb","datavalue":{"value":{"entity-type":"item","numeric-id":5615284,"id":"Q5615284"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448980$D2B8C581-DF85-412C-AFE0-6C7B23F9E80C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da5c4c6269cfab8e5917ddd21b6126adfe8f1934","datavalue":{"value":{"entity-type":"item","numeric-id":5458427,"id":"Q5458427"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448980$154EF1CC-AA00-4787-AAD8-C737BD5249BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5eeea6b81b649443d654385a558cdcdd4000e4c7","datavalue":{"value":{"entity-type":"item","numeric-id":2479475,"id":"Q2479475"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448980$A4C2C674-8184-4CDC-9D72-EACA28629DBB","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":"Q448980$AA4FFE2A-7370-42FE-893B-62687CE5CFC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6a7692118b11252b3f0cec4dada3c7d7555230b7","datavalue":{"value":{"entity-type":"item","numeric-id":1174819,"id":"Q1174819"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448980$1883B881-F28E-4371-B024-DABB9C40682B","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":"Q448980$A6650282-CB3D-4771-BB7B-C8D7C27406B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2e1e35e1d6126eec41b1ea07713b5304f3ba86b9","datavalue":{"value":{"entity-type":"item","numeric-id":4790670,"id":"Q4790670"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448980$6FDED090-1B49-418C-89A2-C9E4E9506630","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5827b33f6040e2365ba104b2c460c40532349bb","datavalue":{"value":{"entity-type":"item","numeric-id":3311639,"id":"Q3311639"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448980$5317988B-74A0-4AEC-8B1C-562901324C90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7b075ec1308248860fcfdc195b05217fd7b238e7","datavalue":{"value":{"entity-type":"item","numeric-id":3855206,"id":"Q3855206"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448980$63440825-064D-4E17-A8EF-DEFEB38E1C9B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"37d79a43da1617380e648e4ae89b78a9fe0ede16","datavalue":{"value":"10.1016/J.COMGEO.2010.06.006","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q448980$8B7F50A7-5253-4F61-BAD5-F6582FDBA980","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a7a2ab1b64aefaad63434d35e63853f0e8c9ef14","datavalue":{"value":{"entity-type":"item","numeric-id":2849508,"id":"Q2849508"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f609175950a5ec6f1b1bf97ca1b03e9ffb37da81","datavalue":{"value":{"amount":"+0.8874422907829285","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":"Q448980$76ECCA7A-F9A4-44A7-AE76-4476818089A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3b784c61d389e3095e4916001fa44acb7c8e1993","datavalue":{"value":{"entity-type":"item","numeric-id":4790670,"id":"Q4790670"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4e46aeff3b57b8cd44e550c1ec6932eefcefa2ae","datavalue":{"value":{"amount":"+0.8457993268966675","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":"Q448980$02954055-A5CF-4F72-9421-093471BC8631","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"878e59eca479c140a2d6f9aa5873256c95814086","datavalue":{"value":{"entity-type":"item","numeric-id":1623113,"id":"Q1623113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0c60daef3eb8702e86a5992b110224c84b585099","datavalue":{"value":{"amount":"+0.7523130178451538","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":"Q448980$D94745D2-1935-4C1E-9826-A856961157BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8d47f90a6218449ec00e40f295fc64cd92cfe1c7","datavalue":{"value":{"entity-type":"item","numeric-id":2643883,"id":"Q2643883"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f517e2c7352451fc1577296275e35925a09aea4b","datavalue":{"value":{"amount":"+0.7512603998184204","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":"Q448980$98B2878C-B14C-4A67-9809-CF89CC1CE409","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0f45eb44c051a43ed17bf428283ac729a5b368a9","datavalue":{"value":{"entity-type":"item","numeric-id":4910724,"id":"Q4910724"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ea0eefe06f466ae89c2486020a35884f079b3b8e","datavalue":{"value":{"amount":"+0.7484387755393982","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":"Q448980$4D3E7C28-2909-4870-81FF-30B680E19818","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:448980","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:448980"}}}}}