{"entities":{"Q2219076":{"pageid":2229819,"ns":120,"title":"Item:Q2219076","lastrevid":82661099,"modified":"2026-05-06T21:26:30Z","type":"item","id":"Q2219076","labels":{"en":{"language":"en","value":"Dual and axiomatic systems for constructive S4, a formally verified equivalence"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7297792"}},"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":"Q2219076$DEFFC79B-1617-4600-9C9F-BBBC97E78989","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"34968c6fcc73f138de95cf64d3c3acaf543d1797","datavalue":{"value":{"text":"Dual and axiomatic systems for constructive S4, a formally verified equivalence","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2219076$7A570C08-86DE-4573-BE21-A817192FA101","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6aaf74ff6539cb9bce26965659d193c2b5a25820","datavalue":{"value":"1495.03032","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2219076$7EAA02DA-96B2-4CE6-B249-B0AD9419A5ED","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"77349d7f7398c47e6d2065cd0d80588fae809ad3","datavalue":{"value":{"entity-type":"item","numeric-id":2133448,"id":"Q2133448"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219076$582325D7-0FF0-4BB3-BF3A-33D78AF8654E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"617513ed20293f92b2f67987461eb17d18d83c6e","datavalue":{"value":{"entity-type":"item","numeric-id":2133447,"id":"Q2133447"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219076$1C844289-944D-4111-A45D-C9CA7D07DEDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"803bea2a250aa044a568a4d507a15b39a3e843a0","datavalue":{"value":{"entity-type":"item","numeric-id":2133449,"id":"Q2133449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219076$206D003A-481C-426E-B416-E87279FEEB9E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"a1a70f16fd8e81a4c35439aeec3d3645cd1e55e6","datavalue":{"value":{"time":"+2021-01-19T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2219076$9ADB35CF-7E26-4BBA-821D-257B5DE8A13E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2219076$181E090E-60AE-4CBE-B1A7-FDFB5721D0E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2219076$DB8AECC5-7947-496E-B9F8-3B0C49506182","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2219076$98E0D111-4391-4610-AB81-97CCC6600712","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"552e3c1436324db5a01603a5396a61e9a6ecb823","datavalue":{"value":"7297792","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2219076$3D2D151C-A5A2-47A8-9043-095A14E975C2","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ae682d5c22f8702c694a649057f29b8c3c289b60","datavalue":{"value":"modal logic S4","type":"string"},"datatype":"string"},"type":"statement","id":"Q2219076$CFDBC4B9-30F5-45D8-82C9-38FF4D8BEC61","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c4a62be59df86ac5656fbe65ad3e6c1589611bfc","datavalue":{"value":"constructive logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2219076$6EE56FED-7ED6-4C40-8264-079F60227E31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a7245057d33d9a959e820bafe53b372c083536e6","datavalue":{"value":"natural deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q2219076$1A89E899-E737-47E5-AA96-D38C9AD3BAA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4cb59c9f34d3c81e61b3a2c9d8c9182884aa2134","datavalue":{"value":"dual calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q2219076$164117C8-23D7-4BDE-A3CD-1EC27AEE18ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2eb4d1af95699ef062cce80ecbcf1e1484586450","datavalue":{"value":"formal verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2219076$8D00C07A-33B6-403B-B002-93DB559D0487","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q2219076$DE426A4A-57F3-4DC3-B720-0B5E945FBEC0","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"134eb05b9c51716f31ce6e2afce915498d90f6db","datavalue":{"value":"Q113317342","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2219076$44A52EAB-E15E-4CDD-BBB8-AF638F9B5317","rank":"normal"}],"P1463":[{"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":"Q2219076$79F8C6D7-6121-41CC-8B03-6BC2F4047671","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6111489034643139b6436054b44d6250e7c1756c","datavalue":{"value":{"entity-type":"item","numeric-id":41339,"id":"Q41339"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219076$5B42EF04-579C-4A29-9ACC-D2BE36AAA925","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":"Q2219076$9A0BE6CC-88B4-4260-A27C-4EBF7E5D0DC1","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"cd1ed8e3275daaa10a47dc934fa593fb4ffd413b","datavalue":{"value":"https://doi.org/10.1016/j.entcs.2020.02.005","type":"string"},"datatype":"url"},"type":"statement","id":"Q2219076$40C5AC14-0F13-4BA8-9A10-9B73177A571A","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d80b69a0e3dac26ccf5d5999a484069f15a449de","datavalue":{"value":"W3013261218","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2219076$3FE0012E-EE06-42FC-B2A6-B5EEF01FAE4F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1d8e7ec345413e104735faa57122d0400eae37de","datavalue":{"value":{"entity-type":"item","numeric-id":4785506,"id":"Q4785506"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219076$3F0903A2-2ACB-43DF-9C49-29B60A186332","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d8448c0105e91748355fbfe83c6a8ebfb33e3531","datavalue":{"value":{"entity-type":"item","numeric-id":1577344,"id":"Q1577344"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219076$0F333DBF-D11B-4AC7-840A-59CD8E4A9012","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"450927e1d852a7d15cf0194c2cb39e02a3cf5c9f","datavalue":{"value":{"entity-type":"item","numeric-id":4007157,"id":"Q4007157"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219076$298FE791-0964-43BC-A2E9-DFF784C9F720","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ba08a437a70cf639d99741bc364e8aa3e5f667ca","datavalue":{"value":{"entity-type":"item","numeric-id":3605521,"id":"Q3605521"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219076$8220F9A7-06FD-4AA1-B9D3-B18A778D30DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2e71729ea20b25ac29e78246550bb4c8ab42ed4d","datavalue":{"value":{"entity-type":"item","numeric-id":1652988,"id":"Q1652988"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219076$95870C1B-29EB-4AE7-BA49-751EA0E4A3D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"05618bc94dd537d3034b233a45ab1cb0906c9164","datavalue":{"value":{"entity-type":"item","numeric-id":3196622,"id":"Q3196622"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219076$66D431EA-FA38-4CB9-9B67-75166BB56109","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f8bb526784b7bc0517d99805eff98b4a5f58f8ee","datavalue":{"value":{"entity-type":"item","numeric-id":1368378,"id":"Q1368378"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219076$550382A9-73B4-46F4-B196-35AA6B1A7398","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aaa788232f974bc5396481c46998b860ec3e6d1b","datavalue":{"value":{"entity-type":"item","numeric-id":1056744,"id":"Q1056744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219076$7C3D0439-944D-45B7-A693-E84E9F6D90DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"86f70427d1bec1892856b306a28600257c0fb1f9","datavalue":{"value":{"entity-type":"item","numeric-id":3408862,"id":"Q3408862"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219076$49E6AC80-F2C5-4161-A2B3-512DB04AB7CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f34b77e9616af68856c2fef9e864836767c008fc","datavalue":{"value":{"entity-type":"item","numeric-id":3414345,"id":"Q3414345"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219076$61306B2A-0DF9-47EE-850D-DE075C7A26DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"191e9aa8283541e6a8e1a9c064cd250820506f48","datavalue":{"value":{"entity-type":"item","numeric-id":4219051,"id":"Q4219051"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219076$3DD9FBC6-8385-48E8-8CCE-4EE9CA4CD990","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d8facf0d51be0f110356c413bcb4d3b0db305a8","datavalue":{"value":{"entity-type":"item","numeric-id":5231279,"id":"Q5231279"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219076$E06A003A-DEF5-4D3F-8F24-78E14D2D1FBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"adf8ba65b22cb108cd3fff432281939108477768","datavalue":{"value":{"entity-type":"item","numeric-id":383061,"id":"Q383061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219076$9EFFFBB6-F6C8-49FF-A431-2104E65BEF30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"672be30d9c0fd1bb08a1fc6131d1506ec245277a","datavalue":{"value":{"entity-type":"item","numeric-id":4830107,"id":"Q4830107"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219076$CD1744A3-44D0-4CFE-87B9-9D78BDD17C3E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a568888be8b5be4fdbfd5a43fc3024e643387af5","datavalue":{"value":{"entity-type":"item","numeric-id":659458,"id":"Q659458"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219076$7A902436-D9BC-49DD-880B-B49013664208","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cc9ef798e3ca8ce1bee688f2fa85b74a55e80258","datavalue":{"value":{"entity-type":"item","numeric-id":5144635,"id":"Q5144635"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219076$2928D89F-31A6-4337-B7B1-A5F3D0A3B963","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5bb72cd6bda37262199f054c3e49ed1f627a6fb7","datavalue":{"value":{"entity-type":"item","numeric-id":1392142,"id":"Q1392142"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219076$E04501DF-F3CC-4482-B6F9-734A312E1A1C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1968a7a950e39434a878f5976f0c19d61093a1a6","datavalue":{"value":{"entity-type":"item","numeric-id":5111325,"id":"Q5111325"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219076$CB8794F9-C808-4961-9017-D246F731E965","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5769eff0a2ede6650e8ecb17abc74e30a6cc9dd4","datavalue":{"value":{"entity-type":"item","numeric-id":4360856,"id":"Q4360856"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219076$8541D515-8F9F-4D97-A505-759BF9F8A9C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47b0ec3118c55b6f3ab232f29debefc8c9d383a9","datavalue":{"value":{"entity-type":"item","numeric-id":3688389,"id":"Q3688389"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219076$2382B9B8-04CA-4CE5-B993-8A44988377E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"604686a5863b0bbdb6c64aa93b923e5212a9cf8f","datavalue":{"value":{"entity-type":"item","numeric-id":2746757,"id":"Q2746757"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219076$0082E593-D77B-4D07-87A3-A90D62C4952A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2cf8d33b8b327786a9a2b104ad143919c97e9e62","datavalue":{"value":{"entity-type":"item","numeric-id":5408687,"id":"Q5408687"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219076$86EFBA36-2D00-4241-B41C-15C9B0159BF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d5396675c233e52b8c02a15330c24f234a93204a","datavalue":{"value":{"entity-type":"item","numeric-id":987853,"id":"Q987853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219076$01EBE769-67EF-4050-9F90-68F9A7906182","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a4441a33df5428b009347f1022f1440c1aaee513","datavalue":{"value":{"entity-type":"item","numeric-id":881453,"id":"Q881453"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219076$254A5015-EB41-49E2-9261-7D27B34151D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bd91764eff76cc10b57d0382d5477793a8cf7f61","datavalue":{"value":{"entity-type":"item","numeric-id":4686519,"id":"Q4686519"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219076$1D46BAD9-BF06-4DB9-864D-B5C596133028","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"93f5092601c81792f7b9738f21ce688a77409d15","datavalue":{"value":{"entity-type":"item","numeric-id":4530621,"id":"Q4530621"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219076$F092EDFB-C080-493E-9764-5C535A59840B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e06536935b7efcaa88b0e1b16b72fed895f259d0","datavalue":{"value":"10.1016/J.ENTCS.2020.02.005","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2219076$B31C7012-DB8D-4B88-9528-1E83DC17DAFD","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"18c4ffe40372dc0a9b0b95d7bdcb764f371d41ad","datavalue":{"value":{"entity-type":"item","numeric-id":5231279,"id":"Q5231279"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"56188f5c3641d7e69d78a7a454d26be83c6fca98","datavalue":{"value":{"amount":"+0.9040607810020448","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":"Q2219076$665A0484-4F45-45FD-9311-2B322E53824E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f898127b0c13eea1e50d7c1753fd84736fe82118","datavalue":{"value":{"entity-type":"item","numeric-id":3196338,"id":"Q3196338"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b7c16a5dde7246c5aa842aa5e9f2e652e4974728","datavalue":{"value":{"amount":"+0.7624890208244324","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":"Q2219076$99F16B1A-70C5-44F0-9C45-347045C168F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4aa3e52fba1a9078ffd97183f542871dd8723343","datavalue":{"value":{"entity-type":"item","numeric-id":5144635,"id":"Q5144635"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"944d535d50537d086cf41582fd9b6a8da4c33ad5","datavalue":{"value":{"amount":"+0.7580693364143372","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":"Q2219076$4D323012-B9CC-40ED-8B3B-B37CDF51CB69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"22306f86ecbe244c29702ba1468c094f1d60f493","datavalue":{"value":{"entity-type":"item","numeric-id":4785506,"id":"Q4785506"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d359d47e07c5c1a3c5e9f96cdfddb8f841e5d9f8","datavalue":{"value":{"amount":"+0.7482414841651917","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":"Q2219076$24CDAB1C-D13A-4A3F-9A94-C497618C73DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2b0346cb07c892f61a7f5b431ff4ebc45d81b80c","datavalue":{"value":{"entity-type":"item","numeric-id":3410675,"id":"Q3410675"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0980b93cca52ac9b02c0badecb03304a841ced85","datavalue":{"value":{"amount":"+0.7368705868721008","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":"Q2219076$B193D89E-37D0-481C-BD7D-9C045C938750","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Dual and axiomatic systems for constructive S4, a formally verified equivalence","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Dual_and_axiomatic_systems_for_constructive_S4,_a_formally_verified_equivalence"}}}}}