{"entities":{"Q5222980":{"pageid":7252550,"ns":120,"title":"Item:Q5222980","lastrevid":53469746,"modified":"2026-01-25T00:29:11Z","type":"item","id":"Q5222980","labels":{"en":{"language":"en","value":"A verified theorem prover backend supported by a monotonic library"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7076888"}},"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":"Q5222980$20B16CDE-F76A-4F85-A0C7-D88F77178EC9","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e862f8f8987af69c2e76d5ce1970998da4999ebf","datavalue":{"value":{"text":"A Verified Theorem Prover Backend Supported by a Monotonic Library","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5222980$621F41EB-5B44-471B-9C54-53730F5180F1","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a36e9ace35e0fa988bfaf14e7d31a7953ab74fcf","datavalue":{"value":"1409.68262","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5222980$BD2F1D33-C1A3-4CEF-979E-3FB0B5943354","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"94e04c8c2512ac0b5c5096b1f636df023ddd07c2","datavalue":{"value":{"entity-type":"item","numeric-id":507362,"id":"Q507362"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5222980$FCAC1C6B-AEBD-4F34-A1D6-B2CB21C45D30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"fca002f5263bf37cd78527dfba7fca450ce3c4eb","datavalue":{"value":{"entity-type":"item","numeric-id":1694468,"id":"Q1694468"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5222980$8B1D2FD2-AEC6-4A2C-950F-209D368B0031","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bf4e80c62f3af6544d946ed36bab3a03f4f43897","datavalue":{"value":{"entity-type":"item","numeric-id":392279,"id":"Q392279"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5222980$8C41BE91-BE56-4AF6-AAFD-B9C0B0D6DB16","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"eae4601ff702bcaa610b94b3434abd8165930c5d","datavalue":{"value":{"entity-type":"item","numeric-id":4645721,"id":"Q4645721"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5222980$80C9DBAA-3A99-4DD2-A7F0-A005051C58EB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"311afef0a4b95245df7f6c2908ad6e9d40f3f2be","datavalue":{"value":{"time":"+2019-07-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5222980$24837BFE-800B-400A-8F9B-9A80E646096A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5222980$41825AE1-0E5A-40AC-85C9-9C4E147792A4","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"77f4be8506287fdecbc28c73da3050e9f1ed33c2","datavalue":{"value":"7076888","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5222980$E3875EEA-E602-4FC4-A015-678F2137DA96","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q5222980$0610A999-35A4-4D33-A63C-4AE7377EAE52","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"227516aa7fbea9b9a02265574c64839991a58972","datavalue":{"value":"digital library","type":"string"},"datatype":"string"},"type":"statement","id":"Q5222980$C5065727-EBBC-4E4A-92EB-6B684F28C995","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6f8c1a6a94dc6f409a1001bf601947c25349ecbd","datavalue":{"value":"Kripke semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q5222980$6E4D847D-AB4A-4F30-960D-08814C87BF9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"afe493c1ace3fa52144c0315aaea9019dde435a3","datavalue":{"value":"monotonicity","type":"string"},"datatype":"string"},"type":"statement","id":"Q5222980$A14D7AC4-E636-4ECC-B2A5-7D8C3615A3DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"efaf681fa46ac3de36993134e18f2efa737a2c0f","datavalue":{"value":"Nuprl","type":"string"},"datatype":"string"},"type":"statement","id":"Q5222980$A07D4111-D615-40D5-9E10-52ED6699BCF5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e29a0a1a089c1739ef594b8aa170de0991ebf7f7","datavalue":{"value":"proof checker","type":"string"},"datatype":"string"},"type":"statement","id":"Q5222980$5FE751C3-EC3F-454D-9738-C8FA1EC39F58","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5614ce1201b522da92016cbfc0aa775f87d97e03","datavalue":{"value":"verified theorem prover backend","type":"string"},"datatype":"string"},"type":"statement","id":"Q5222980$48E600AF-2346-4AE0-9B4F-8C6C3D59652E","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"cfcce3c91bc8c99152c1c82bea5047be55960c64","datavalue":{"value":{"entity-type":"item","numeric-id":41357,"id":"Q41357"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5222980$FE5726F8-570B-4945-A041-791209C24FFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"533959f24a509b955614f607e46b8aa4cec190ef","datavalue":{"value":{"entity-type":"item","numeric-id":20799,"id":"Q20799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5222980$D92D79A4-1642-491F-A245-3DDECFA64C29","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":"Q5222980$DEA24584-9751-4EE6-BA9F-1DEEB00E02BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b6da1f42e3d4d28e24ecb68672c28ee0982a60c2","datavalue":{"value":{"entity-type":"item","numeric-id":12950,"id":"Q12950"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5222980$77300E1A-37F9-4D4C-A3A3-65E044747A3A","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":"Q5222980$359B935F-4A71-444C-8A71-135CB3F6BD15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a0292a334cfc9946d990e370c442c475973c3701","datavalue":{"value":{"entity-type":"item","numeric-id":16053,"id":"Q16053"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5222980$DEE82B25-495A-48F6-B211-4CA44E004C6C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"49f6fb65fa6d2a219475c4a5b936c8907f84d3cb","datavalue":{"value":{"entity-type":"item","numeric-id":16063,"id":"Q16063"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5222980$C58D6831-EAF1-463F-8654-8CA20EB7081A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"27b6ae20da44d6f09b655d9481cc0df08a8ffcdf","datavalue":{"value":{"entity-type":"item","numeric-id":18826,"id":"Q18826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5222980$A92C36DD-215C-420F-9A17-F3505B4EA089","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2e079f4640d565f0ca1930fd327c2c7e8d634508","datavalue":{"value":{"entity-type":"item","numeric-id":21954,"id":"Q21954"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5222980$F8ACAF60-824D-4ABE-9E1D-3A7DFADFD121","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1a8b6b13bef47cb19f4e2508b5917af235a65eb0","datavalue":{"value":{"entity-type":"item","numeric-id":21668,"id":"Q21668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5222980$9B344091-3643-44D2-88DE-433026EA9608","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e603d7c91a5659a0e67ae5a0b1fc4700fb0830e5","datavalue":{"value":{"entity-type":"item","numeric-id":31834,"id":"Q31834"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5222980$99FCD997-66C5-4436-A7EB-0646A5F3F1AC","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":"Q5222980$53B53DCC-62C9-4E55-BF6B-D1D3BA4B5CAD","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a92df80e54f9386bdf6aba75a67fa60648bd7b8a","datavalue":{"value":"https://doi.org/10.29007/f58n","type":"string"},"datatype":"url"},"type":"statement","id":"Q5222980$D3C4DCDC-5E8A-4781-B4AF-9927709483FC","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"248ab0324b68ba0a6b736a11f947de4dcfac1fa5","datavalue":{"value":"W2906661256","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5222980$C8033889-CA33-4CF5-BBB1-EC02E4DE7052","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"79d5e42f83366c8da0bb2dcd277179a15dd16d5f","datavalue":{"value":"10.29007/F58N","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5222980$CF513F28-8B0D-4337-BBDE-2294CB679DD5","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"eb9707e33700967679010ac1d47d134b3b741111","datavalue":{"value":{"entity-type":"item","numeric-id":2879241,"id":"Q2879241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b3a42f208a13f253278aa0ab99a93cf4a38f3d98","datavalue":{"value":{"amount":"+0.7745513319969177","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":"Q5222980$A11A1D11-0D69-40E5-BD53-49FAE7716CF3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6069596235a77af4a0ce188dbd6c4aa338ad0602","datavalue":{"value":{"entity-type":"item","numeric-id":3789525,"id":"Q3789525"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"15be5d945be03befc122301a3b62281b0dc45ff2","datavalue":{"value":{"amount":"+0.7578049898147583","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":"Q5222980$1563CC43-25F1-4183-82EB-C244D728DEE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"16b4ad2e93424e9b6828135c36f028dc0dcc0af4","datavalue":{"value":{"entity-type":"item","numeric-id":2219381,"id":"Q2219381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9266a484feaeed6d0979a87a7620fbfe8859b2e3","datavalue":{"value":{"amount":"+0.7270841598510742","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":"Q5222980$E931F934-FAF3-43D1-8456-1C8CBCDA7B99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5c708fef69a8eece560799e6bf7db9d9dbee7964","datavalue":{"value":{"entity-type":"item","numeric-id":3088011,"id":"Q3088011"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"27f99dbdc46371a1494ac4a51deb52a52f04b6cc","datavalue":{"value":{"amount":"+0.7129895091056824","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":"Q5222980$CC24D468-2A97-4F67-9AC2-E901C47F4888","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2a637a3ec8530fd323624ddc6f2ba82d813d4aa6","datavalue":{"value":{"entity-type":"item","numeric-id":3546045,"id":"Q3546045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cd2e90fce24dfb65437f4d29f22870c09e5f1c46","datavalue":{"value":{"amount":"+0.7107020020484924","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":"Q5222980$65DE5D44-3424-4D77-8D5A-6AFEED5FFF19","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5222980","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5222980"}}}}}