{"entities":{"Q2198134":{"pageid":2208877,"ns":120,"title":"Item:Q2198134","lastrevid":57778644,"modified":"2026-04-02T12:07:06Z","type":"item","id":"Q2198134","labels":{"en":{"language":"en","value":"Formal verification of robotic cell injection systems up to 4-DOF using \\textsf{HOL Light}"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7245546"}},"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":"Q2198134$9BC8BAA8-F83A-47E2-B103-EF43007139C3","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4ad32f5fc7e73f517830af7efbf0406e1091ac2f","datavalue":{"value":{"text":"Formal verification of robotic cell injection systems up to 4-DOF using \\textsf{HOL Light}","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2198134$428FAC8A-9428-413C-91C4-45C2AE3F3CDC","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4688a227a8441d28517d8010feef9deb23525ceb","datavalue":{"value":"1458.68220","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2198134$7FA4B26D-4094-42AC-852B-2E39A141C035","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"891b3bc2f96589c9dedada7f9b5bb76f55e7c5a3","datavalue":{"value":{"entity-type":"item","numeric-id":1640639,"id":"Q1640639"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2198134$E8D34CCD-B53E-4C96-9B26-11D11255FCC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"393ef07e7673f4510d0e5689d2d44001b3ecc236","datavalue":{"value":{"entity-type":"item","numeric-id":246140,"id":"Q246140"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2198134$F265C861-FCB6-45E9-9596-8544216599C0","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d9925518446645d219093152a820aba790417b61","datavalue":{"value":{"entity-type":"item","numeric-id":164203,"id":"Q164203"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2198134$6DAC0CAD-C4E0-4728-B30D-81D8F265B99F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2af50a8f38b9014baebb3050a8a71f7f232c1207","datavalue":{"value":{"time":"+2020-09-09T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2198134$FB4BF2E4-52CC-4A5C-ADE1-F92FE25FB60A","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"32b91c97fecb4e19bb6505b742f7457f93a16902","datavalue":{"value":"https://arxiv.org/abs/1805.02858","type":"string"},"datatype":"url"},"type":"statement","id":"Q2198134$DC9D4615-83FE-42A0-9898-5CEF87D28A53","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"46ffee837b0dbcd63fffc2834ebe2705f88e57be","datavalue":{"value":"68T40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2198134$50B69802-67EF-4A50-AF50-E9A88FF9156F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2198134$E3C25396-5768-496B-AC8F-2D1A17D188CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2198134$A4219C7C-C57A-422A-9DE2-BAE0207BD289","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"22384f514d07e2f675325750f710d3ba3f32e96a","datavalue":{"value":"7245546","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2198134$E8CBBE3C-3A69-4FA9-B0D7-C5BBBB83EA2E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fec1d901a406a7887c6a5de0c7f92844727850db","datavalue":{"value":"robotic cell injection systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q2198134$E502F192-8922-4335-B8B6-AA1F80DF4655","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2eb4d1af95699ef062cce80ecbcf1e1484586450","datavalue":{"value":"formal verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2198134$8796DA4C-5E46-4C62-9596-70B765060362","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2198134$DD525F4B-852A-4869-99D4-99957D02D93D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2198134$D5DD742C-9A77-4DA3-B497-FA23A821C415","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"104686f3a3b63f31fa6c79f5f0116fe39fff0a7f","datavalue":{"value":"HOL Light","type":"string"},"datatype":"string"},"type":"statement","id":"Q2198134$7A4D5719-73D8-46FB-8813-18C6FB298F37","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"99df3d19c323261cc6f51ef59d8e58bf43957bec","datavalue":{"value":{"entity-type":"item","numeric-id":54579,"id":"Q54579"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2198134$31947DB7-B2F2-4E19-AC8D-1C12D3397707","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d89eed7087f93c1cdf4120c868b02779d34eaa8b","datavalue":{"value":{"entity-type":"item","numeric-id":13309,"id":"Q13309"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2198134$F6A61F32-2DA9-4A44-AAB8-13EA9256AACF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2b02b46847f3d7e3a5825b9484a88607b98dbd14","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2198134$2E6881F8-DCEB-4AD4-AB07-BD8CC66280DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2198134$4AA49ADB-12EA-48F4-89A2-FAD7E19BBCCD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a709ac7c97c67049e241e0b036253f1d955c589a","datavalue":{"value":{"entity-type":"item","numeric-id":13313,"id":"Q13313"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2198134$09E1063F-8C5C-4016-ADB1-6B8FBD27D12D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ee80fa482e8c030191fc3263e069d0dc0cdf7815","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2198134$C493580F-015E-438D-95D5-285541DDF062","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"485f54a0549a89232924cb0abb443c2fad36af9f","datavalue":{"value":{"entity-type":"item","numeric-id":13300,"id":"Q13300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2198134$56E4C906-AFF7-4E9C-AF94-EF617C0BEE66","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"707d41837f49f36c2612e42ad4cba320a8c29001","datavalue":{"value":{"entity-type":"item","numeric-id":20896,"id":"Q20896"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2198134$66937C7C-A97E-4FC8-8622-72B4BAAED902","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8bf42d0fd66acf369e3d5d44d7ebef6adc7ae452","datavalue":{"value":{"entity-type":"item","numeric-id":56651,"id":"Q56651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2198134$2D36B30D-01D8-4487-9310-BB4DF5BABD23","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":"Q2198134$1493D373-5529-46C7-86F5-73A9E7B45EC2","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"f3a0a436a0beb44a85830e64e8494bc693891e39","datavalue":{"value":"W3036333943","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2198134$E80190AC-58BD-4002-AB1E-5714C0BCC846","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ce71a5e212a8c5cd65d66580e9075eb5aa319ca","datavalue":{"value":{"entity-type":"item","numeric-id":2956706,"id":"Q2956706"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2198134$CF936BC3-EF23-43D0-AAF0-30E073720370","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8092a4684ef7778dba1ddad2618a794c87412cd6","datavalue":{"value":{"entity-type":"item","numeric-id":5227061,"id":"Q5227061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2198134$7F4AB033-B1AA-44EF-973B-026DEFF2AC95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e7237ffb12f9e25db6f08fc9a97900ed45e5a332","datavalue":{"value":{"entity-type":"item","numeric-id":2813263,"id":"Q2813263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2198134$D28FE3A2-76C3-4E8D-A785-D5552E5411F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"03cb8e50e6c3bd60a9a9a59407cf30e8e788baa4","datavalue":{"value":{"entity-type":"item","numeric-id":3618853,"id":"Q3618853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2198134$2612ABD4-FEE2-46B3-9F5C-3DF8A85312AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b0ef84619234e2e46e8c4513d6d1ef3cba6f5b65","datavalue":{"value":{"entity-type":"item","numeric-id":1945903,"id":"Q1945903"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2198134$3A3CBDA0-CF64-4B27-B0A3-1B8607C1A1B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"085f2f402bb0aaa918a693e06aa64da16c2193f2","datavalue":{"value":{"entity-type":"item","numeric-id":5687569,"id":"Q5687569"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2198134$A177DD56-2564-4636-8F7F-7C811729658F","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"d7f8c5202eddf9b264a9322d254907a9e7a74abe","datavalue":{"value":"Q130846630","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2198134$183EA2E2-C961-44AB-972A-DE49FAED4572","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b1aa867295baba569d9b5846fb241b57b99fc7b8","datavalue":{"value":"10.1007/S00165-020-00514-3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2198134$1B97601C-47F2-417C-8E83-0CA0B624683E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6a4a5e811b912f210d0e5220ef81ba26c37c0253","datavalue":{"value":{"entity-type":"item","numeric-id":4560620,"id":"Q4560620"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f96866450c3e459772466f9a513d0270c0e107ab","datavalue":{"value":{"amount":"+0.6981661915779114","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":"Q2198134$05663EB9-F1D1-4C04-8B5F-3E6769320CF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4867ce6e792bece096e21f88b609d530ff82bd27","datavalue":{"value":{"entity-type":"item","numeric-id":4546958,"id":"Q4546958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e92ed70e6b8ef51debca0d254e80ab92a4e1e1ef","datavalue":{"value":{"amount":"+0.6415291428565979","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":"Q2198134$ACCE9722-6CB5-436D-BCB6-D50396D4BC9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"539bc861b4d3009317613a6568132d2e0c6e496b","datavalue":{"value":{"entity-type":"item","numeric-id":475384,"id":"Q475384"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6901fdb4ff771f677282a417a7fa5dd50dd72ca2","datavalue":{"value":{"amount":"+0.6214269995689392","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":"Q2198134$6E159F6F-8B3D-4D1A-92C7-59DFC7500BD6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5bc71288bc152c8b66c4e360ece91d01118d8b11","datavalue":{"value":{"entity-type":"item","numeric-id":5045474,"id":"Q5045474"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aee42fce6e27a5898d62af49e9b61ebe89e951f9","datavalue":{"value":{"amount":"+0.6189329624176025","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":"Q2198134$DB9635D7-30F4-4B50-B8CB-9158177DE5B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1d04c42e58e23ec1d6352624e342ca502217cb95","datavalue":{"value":{"entity-type":"item","numeric-id":2361358,"id":"Q2361358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9ab572fcc7469ee406151e2ec36e61ddf941c708","datavalue":{"value":{"amount":"+0.6113120317459106","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":"Q2198134$F0573150-219B-4465-8E82-771E8F209121","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2198134","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2198134"}}}}}