{"entities":{"Q5166496":{"pageid":7196068,"ns":120,"title":"Item:Q5166496","lastrevid":56869923,"modified":"2026-03-24T09:25:39Z","type":"item","id":"Q5166496","labels":{"en":{"language":"en","value":"Panoptes: an exploration tool for formal proofs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6309202"}},"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":"Q5166496$8CEC01D8-2413-4F56-9C81-2B0CEC77C964","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8940c3bead60e60bff883cd03df8ba3aa90ea4e1","datavalue":{"value":{"text":"Panoptes","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5166496$0DF2C33B-1D56-456A-8181-073DF58AB00E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9d26d00ca0e65b15bbf837084ce7cb82e030ebff","datavalue":{"value":"1291.68339","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5166496$43A225F3-E74C-4196-BD0E-6F7D375AD201","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"596956d13d65318c3063740527340bc624646ab6","datavalue":{"value":{"entity-type":"item","numeric-id":174773,"id":"Q174773"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5166496$82F5F1EB-F0CB-4515-925C-B1607746A014","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"319d2c137a3ad1d88f7985c9a6ae36735f64db2b","datavalue":{"value":{"entity-type":"item","numeric-id":5166495,"id":"Q5166495"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5166496$B29AE61E-BB26-4435-A0C9-855FCAA95F09","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3478ec308a15597e43cb648673c843463f4d3028","datavalue":{"value":{"entity-type":"item","numeric-id":163528,"id":"Q163528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5166496$040A91B4-F235-4693-B8D6-3D81BC0DE17C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"251e0e848447c04df22617da60cec84f2100f397","datavalue":{"value":{"time":"+2014-06-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5166496$E63FEA5B-9AEA-4341-92DE-A1A739F1CD91","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5166496$17C087C3-21D2-4365-96EE-8200F9D5A61D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"37850679e633669368ccd3b2b6b8c0efcc2ed7da","datavalue":{"value":"6309202","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5166496$BEBF833B-3F3C-485A-AA64-2271D3551DAA","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"57011f4359c34ab7c9585d8629a23d759f50e140","datavalue":{"value":"IMPS","type":"string"},"datatype":"string"},"type":"statement","id":"Q5166496$859799B6-686B-4946-84F1-66CE556ECCAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5fefb0a256282830a8f0578e7a1e60e221743807","datavalue":{"value":"deduction graph","type":"string"},"datatype":"string"},"type":"statement","id":"Q5166496$200D42AA-62ED-4789-9110-A6E39D30EEB3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0213b48e373f0f895e54a16323e67f641558338c","datavalue":{"value":"proof tree","type":"string"},"datatype":"string"},"type":"statement","id":"Q5166496$52B0AF98-1FC7-419B-912B-2D6AE153A482","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8bf549142b710f01581b24fd28cbb67614316cd4","datavalue":{"value":"theorem prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q5166496$3B688B92-3691-4558-81FC-14A1BDDC1793","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4622cbeb71c776b80d62fd4a6cf06621776120f3","datavalue":{"value":"graph visualization","type":"string"},"datatype":"string"},"type":"statement","id":"Q5166496$A1EE9DCA-D4B0-4A76-B70B-CB7F5A4421A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bd8e841e4cc6e9002be5ed45d8dcddb3e497bd39","datavalue":{"value":"OCaml","type":"string"},"datatype":"string"},"type":"statement","id":"Q5166496$94630085-FBAE-4FCB-8D5F-4C7A907F2AB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e9577bd7fadf977c171e1627d7e88f6b1a421079","datavalue":{"value":"OpenGL","type":"string"},"datatype":"string"},"type":"statement","id":"Q5166496$4B3044A9-4DB5-47E1-87BF-67CBD7D5251C","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d3ed9701b24c07e8ddeb19932e1fa77191c06e95","datavalue":{"value":{"entity-type":"item","numeric-id":16327,"id":"Q16327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5166496$297E33D2-15E3-4DD2-B9DB-329DEEA9CAD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"dc5c7cbf0d7f199d01b4d7bea26f5d171327f0b2","datavalue":{"value":{"entity-type":"item","numeric-id":33179,"id":"Q33179"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5166496$A94AE084-75BE-490C-8B1B-9CD8CCD47B28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3a91a09cea06b92a374a381bd8f3c8c9a2e6ea69","datavalue":{"value":{"entity-type":"item","numeric-id":5974577,"id":"Q5974577"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5166496$A06B3547-3C00-44D7-841C-92E184FCD611","rank":"normal"},{"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":"Q5166496$5122FE22-4189-49F1-9FFF-F6A1739A84CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fd4e6e16753ae90acb872bc722ea8ec4d73935f9","datavalue":{"value":{"entity-type":"item","numeric-id":18816,"id":"Q18816"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5166496$53009794-FC32-4825-B19B-A3757C990591","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b799da0cc0efb29a46dd283874e64386ca0e87dd","datavalue":{"value":{"entity-type":"item","numeric-id":21136,"id":"Q21136"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5166496$ECAEE1C7-BD24-419B-B1E3-F2F03F2FC2C4","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":"Q5166496$AAFE4A06-8840-430E-BC1E-1AFE6FB3BE48","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b4314020a2946508d0912fd08bf584d4ab9694e6","datavalue":{"value":"https://doi.org/10.1016/j.entcs.2008.12.096","type":"string"},"datatype":"url"},"type":"statement","id":"Q5166496$AD63EA6F-88C0-47FD-AB39-845308DEDCD4","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d96cecfcd2df2e43139f935829a913d0510a7526","datavalue":{"value":"W1483110599","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5166496$7B5C072F-CD49-44D9-A3A4-FF90564DF7FC","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"fa946e46dd7fe5ebbecad5b92f77605dd2ee5cd0","datavalue":{"value":{"entity-type":"item","numeric-id":1319391,"id":"Q1319391"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5166496$9D8C2343-654F-4A97-9D79-70D66950B1F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"79085101887fef7638c901f59dd636a71ab7ae64","datavalue":{"value":{"entity-type":"item","numeric-id":4647527,"id":"Q4647527"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5166496$4D29B187-6F47-4C9C-8101-1FDE9303E2A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2618e53bed1b3c3886f64bb636cb8ec1116d4797","datavalue":{"value":{"entity-type":"item","numeric-id":5166496,"id":"Q5166496"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5166496$C49EF2D9-76DA-4D2E-97EF-6E943741F3DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"60e78f3a5cbdcade8fda91d2f65f010e0adbc083","datavalue":{"value":{"entity-type":"item","numeric-id":3613401,"id":"Q3613401"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5166496$B1D348B4-C23F-42E1-9A84-2D17E7CEB805","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2c5b09e879fc9e6d166a18cb26ec583e2bf401aa","datavalue":{"value":{"entity-type":"item","numeric-id":1272614,"id":"Q1272614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5166496$56AE3E95-0B94-439A-99E6-E08475690FA3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"25d88e8214fc05d7111bfb1c0e54ac7e886bdc6f","datavalue":{"value":{"entity-type":"item","numeric-id":2867942,"id":"Q2867942"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5166496$22B21394-F73F-4C01-8F83-57BAE07EEF90","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"45620a1ccda69348db7290da3ac1c5edb6c8c9f6","datavalue":{"value":"10.1016/J.ENTCS.2008.12.096","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5166496$E0AF5DAD-5359-44DB-B95C-C0E2FE6FCCC4","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"757e822784b4bdc641199b06bea0bf174e7498e6","datavalue":{"value":{"entity-type":"item","numeric-id":832103,"id":"Q832103"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"309a16ed550f5e5268139c63249a9c74fce6b2e0","datavalue":{"value":{"amount":"+0.8020243048667908","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":"Q5166496$AEE86004-1BB9-47B9-BEE6-3BBE901B325C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d66339c795d505f780406e18e20e0f95f8bd017d","datavalue":{"value":{"entity-type":"item","numeric-id":2729065,"id":"Q2729065"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4c972a3e02f38511f34320bb85a67f6daf385e35","datavalue":{"value":{"amount":"+0.7508459091186523","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":"Q5166496$83468226-DD0D-4207-9746-A0A6A55A2940","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"af47caf822b03a03a704ed7ee8caa15dc6e408e7","datavalue":{"value":{"entity-type":"item","numeric-id":2462635,"id":"Q2462635"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"524598a4c8a5f4226ad848bac251676c99d83ed8","datavalue":{"value":{"amount":"+0.7500606775283813","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":"Q5166496$57B50AF5-F879-4E5D-8308-AE7A48307B3A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"35ad20c823504330711c7e03204434544d918e40","datavalue":{"value":{"entity-type":"item","numeric-id":2462636,"id":"Q2462636"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9dccad1f8d7672e08ebc9f06af84f76eceeee500","datavalue":{"value":{"amount":"+0.7498484253883362","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":"Q5166496$913FA0C7-C148-41F8-B841-DD4DEE1D00D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7eaadebc466006f9ba58130f8a493cb2148622f8","datavalue":{"value":{"entity-type":"item","numeric-id":2829254,"id":"Q2829254"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"abd3dd3607f501cc7e326777e6cd4f29066f800b","datavalue":{"value":{"amount":"+0.746256947517395","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":"Q5166496$C0319741-CEC0-4619-A4A3-745288119A5A","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"c39a117a349789e54237c0a3254f5a10c0a6517e","datavalue":{"value":{"entity-type":"item","numeric-id":6830565,"id":"Q6830565"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5166496$253F612D-49A9-4207-9B6A-D3D099472894","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5166496","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5166496"}}}}}