{"entities":{"Q5389068":{"pageid":7418642,"ns":120,"title":"Item:Q5389068","lastrevid":51453587,"modified":"2026-01-18T07:44:40Z","type":"item","id":"Q5389068","labels":{"en":{"language":"en","value":"Automated certified proofs with CiME3"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6027825"}},"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":"Q5389068$66D07F74-D37F-40BE-9F8B-0F227E343CDB","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d5974618e739a137cb471ca15a187bcf319d61eb","datavalue":{"value":"1236.68219","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5389068$6CB6472B-7304-4CF2-8E07-406DB008FA0D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"55727f9f4a7efb137e6c3bf39c513ca15ab9ea55","datavalue":{"value":{"entity-type":"item","numeric-id":851140,"id":"Q851140"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5389068$6EAEC53C-D962-4021-8B3F-A009E324E4DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"cfcdce602f947ea2b49893140570219e6c30f521","datavalue":{"value":{"entity-type":"item","numeric-id":483060,"id":"Q483060"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5389068$072E9FB5-D342-450E-9EDF-E48170C0ABD6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a56edde208bf248962b68bd4f23acb521eb5af39","datavalue":{"value":{"entity-type":"item","numeric-id":2467564,"id":"Q2467564"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5389068$C1450C10-ACFE-48FB-BE82-B1740F0A8D76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"59f62068e8a2da23dd7ff743c1bb63e81e79c3e4","datavalue":{"value":{"entity-type":"item","numeric-id":2769424,"id":"Q2769424"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5389068$4823EA77-558D-4B0D-A42D-60F4BA0117BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a99601cd1ef3148b698a6343b127ea54820fa08e","datavalue":{"value":{"entity-type":"item","numeric-id":483062,"id":"Q483062"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5389068$15A312DB-D6DB-49E5-AF46-D4D7D1DD1FB0","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"85ed9f287d2ea9a2dac92419860840c9949df976","datavalue":{"value":{"time":"+2012-04-24T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5389068$F7EF8336-9554-4B9E-A6AB-EE8C8F18641F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"507a823713da5998a010ed489f7d1a6b25169dac","datavalue":{"value":"http://subs.emis.de/LIPIcs/frontdoor_a155.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q5389068$9DE4F4B1-F1D6-4277-AACD-CAE31141B667","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5389068$89458822-BBA9-4326-B4DC-AF417B75D863","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c636094cc8b933189eabd7c009d327f829bc6ac4","datavalue":{"value":"68Q42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5389068$D20F811F-FCE1-48F0-AA44-0FA0AB3A5386","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"b672fc932a40934db58f6d1aa8f79d2f46fa8d1c","datavalue":{"value":"6027825","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5389068$74FEF4DB-7C4B-48D7-971F-164CD8D589D0","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"476e70cc5d552d5cdc76575cc73d40a8bfb4b86e","datavalue":{"value":"rewriting","type":"string"},"datatype":"string"},"type":"statement","id":"Q5389068$3D735E68-FA66-4D18-B3B0-9C596D61FFF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"326c300cf62efa849a7bdb94dd90663d744d9f5d","datavalue":{"value":"formal proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q5389068$B638AD7D-E522-4FD9-9C58-0CB0A474E10C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d62798ced101241ac0d5e46110e32d69e73a0c1a","datavalue":{"value":"proof automation","type":"string"},"datatype":"string"},"type":"statement","id":"Q5389068$CEF98C4B-7A25-4B09-87E5-F3B91BF8E47C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c6a78675f0dcb3af511ac1d4dfa61901e828bcb8","datavalue":{"value":"proof assistant","type":"string"},"datatype":"string"},"type":"statement","id":"Q5389068$E6B06859-8516-43E3-9141-C3282A205CED","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"184b17ed6ef8f72f90ef44ecb976296d445c28b6","datavalue":{"value":{"entity-type":"item","numeric-id":21947,"id":"Q21947"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5389068$5A9B83B5-12EC-406E-8D10-342FC7698C0C","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":"Q5389068$3D59848E-8605-44E0-8E8D-078338E753E1","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":"Q5389068$C7DA2AFF-79F2-479C-831C-179BA6A0C541","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e76f97cc173869d6439a41864ebccd64daccc280","datavalue":{"value":"10.4230/LIPICS.RTA.2011.21","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5389068$32B601BE-A9F6-44FF-BC67-F20F71510220","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1d5624ace0144ae139f076458cfea517e275bd15","datavalue":{"value":{"entity-type":"item","numeric-id":3525007,"id":"Q3525007"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"383adadebe1959a478c801779edd04c6db0d7837","datavalue":{"value":{"amount":"+0.8454686999320984","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":"Q5389068$128953EE-FDAC-49A6-A4BA-F5BFC64314BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7686a1559586f19dc54d1a839b5cd4c8e0eefb47","datavalue":{"value":{"entity-type":"item","numeric-id":3183545,"id":"Q3183545"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0b25933fca2f00a59e83f7ecdbed4803157bcc69","datavalue":{"value":{"amount":"+0.7856953144073486","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":"Q5389068$219838A6-E9BF-46FF-95AE-B4B972FD0D04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"41f0638a8c38776d201be9f988b1fd4a259df9fb","datavalue":{"value":{"entity-type":"item","numeric-id":5448658,"id":"Q5448658"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5768773474d5e75fc5218ac2a3cfb8d049495e6c","datavalue":{"value":{"amount":"+0.7468227744102478","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":"Q5389068$4089053B-D0A6-4983-8502-007A12B56B54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4413ccc9ff1d95352c9a2afe1ef977852e8f6412","datavalue":{"value":{"entity-type":"item","numeric-id":5277869,"id":"Q5277869"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fb2409cba0089c01109bac40ad58fc1ba181e568","datavalue":{"value":{"amount":"+0.7428390979766846","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":"Q5389068$07C5BBDA-B92E-4317-9977-168CE0CD18BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9796d7520d7b11fc49e48598e4e7c8921bdf8142","datavalue":{"value":{"entity-type":"item","numeric-id":2841249,"id":"Q2841249"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a9b514fce207c7a2af5c882e6cfef1221adfd92e","datavalue":{"value":{"amount":"+0.7388430237770081","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":"Q5389068$DFE4684D-41DE-4834-9B6A-D8C31E70DE9F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5389068","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5389068"}}}}}