{"entities":{"Q5875443":{"pageid":7904994,"ns":120,"title":"Item:Q5875443","lastrevid":40873689,"modified":"2025-04-12T05:19:39Z","type":"item","id":"Q5875443","labels":{"en":{"language":"en","value":"Verified Decision Procedures for Modal Logics."}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7649980"}},"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":"Q5875443$3EF66A32-E536-4FE3-B235-C0216C3CA081","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"fc763e2b57fbbac9d48da18f7f760623205de858","datavalue":{"value":{"entity-type":"item","numeric-id":2673305,"id":"Q2673305"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875443$B04EA83B-4569-4F70-98A5-0717FC669BEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"9764b5e3183836adae29ba3fef393bcd0832967e","datavalue":{"value":{"entity-type":"item","numeric-id":229747,"id":"Q229747"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875443$1941D56A-3E94-471F-85BE-8353852EEE65","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6695abe38664d65c38747de7b5fe54d9caa92dea","datavalue":{"value":{"time":"+2023-02-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5875443$F89F8002-FFAA-423C-828B-3490FF19FEB1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875443$9D6E5725-41DD-498F-8C97-8E132D78C7FF","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3aa0eb65636d9e6cde9193db06cf628c57d3fa03","datavalue":{"value":"7649980","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875443$9B07C26E-1E85-494E-97CB-33523536FEC9","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f02f4db7bd17ba3fbae1be6bcee13dc9e5aa86bc","datavalue":{"value":"formal methods","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875443$1BE291A0-9C63-4DA0-A139-29BB3B077230","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875443$2CF92B6A-DD33-40EB-9232-9E8D17070A1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f1dda010537b7b36bd45151721146f720815706e","datavalue":{"value":"modal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875443$D219F739-8F78-434F-88A9-32B83156644E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4e8fd89fa28c0f6c3672ef10c3a2104586281edb","datavalue":{"value":"Lean","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875443$681D8AFD-9771-4DA9-ACC0-CA90EECA7CA9","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9dc96d31725a42b8712b814e265dc136a76d4196","datavalue":{"value":{"entity-type":"item","numeric-id":21815,"id":"Q21815"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875443$304BD696-6804-4208-9F21-D935869103B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"39d1d25ae8c00cfad058b188db36fd61dac09925","datavalue":{"value":{"entity-type":"item","numeric-id":27041,"id":"Q27041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875443$4EA51BF9-9647-4234-B0B4-E8E38EF552D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b73e63da46ad72634f3f2787f78c121045ed2916","datavalue":{"value":{"entity-type":"item","numeric-id":35221,"id":"Q35221"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875443$6549E57C-AC61-44B1-9CB5-25B52DBFFC07","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":"Q5875443$BF5EECDA-A683-4977-B6ED-B1BE6C27BED4","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":"Q5875443$CE02E9E8-4F08-4774-80A9-663FE087EB02","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"1d36a5a4b11c12104fb79827212574be40a4ef4a","datavalue":{"value":"https://drops.dagstuhl.de/opus/volltexte/2019/11086/pdf/LIPIcs-ITP-2019-31.pdf/","type":"string"},"datatype":"url"},"type":"statement","id":"Q5875443$F96E5762-3586-4855-99F2-622ED138323B","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"00a04f3257209273a080ebaf55433867ce665a0c","datavalue":{"value":"W2978361984","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875443$C77FAE4F-498F-484F-8FB9-E0EF11FBE38B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"392323808426c020cf2a99c44a1ead5c296e63bc","datavalue":{"value":{"text":"Verified Decision Procedures for Modal Logics.","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5875443$CCAB7521-7FDC-4482-80C3-3EADB02B139A","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"10110e06488ba400c21fbfc09aa0605286705b15","datavalue":{"value":{"entity-type":"item","numeric-id":2851822,"id":"Q2851822"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875443$4587E93C-52E8-40F1-802B-25CB18CFD6A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"36370121c36b0c2edeeeafe9a4528a350aba816a","datavalue":{"value":{"entity-type":"item","numeric-id":3523171,"id":"Q3523171"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875443$8A86DA58-49C6-4A22-A2B2-B18C41B98E87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"89d0eb12d2bb9d4287d7eb22f6da2759f846111a","datavalue":{"value":{"entity-type":"item","numeric-id":4406531,"id":"Q4406531"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875443$69B9DEA2-A7CB-4E3F-9167-515B367619A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6b7672984695ebd8205b2327d3a9eb3180fc9209","datavalue":{"value":{"entity-type":"item","numeric-id":1977575,"id":"Q1977575"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875443$A71700EA-43BA-4B2E-B8F1-427E910BBA9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"00c2d672d21d4d5af646f31d9599e67b8b6b153b","datavalue":{"value":{"entity-type":"item","numeric-id":1663234,"id":"Q1663234"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875443$A2FDDBFB-E203-416A-AB98-AB6DC2342683","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8242928870aab67343ad0152eb7ca8357168f7f3","datavalue":{"value":{"entity-type":"item","numeric-id":3454108,"id":"Q3454108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875443$48585879-69E5-47AC-976C-3CFEE015C42F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cf1aae49eb6b5d7cf3c74c68e06df16ab076f84f","datavalue":{"value":{"entity-type":"item","numeric-id":2753601,"id":"Q2753601"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875443$B95106FB-11E9-4DB6-82F8-AB2044D01063","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7a848ab10b49b8034fa7a7c3ea1c75dd27f93d21","datavalue":{"value":{"entity-type":"item","numeric-id":3192179,"id":"Q3192179"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875443$03529585-4E59-420B-9194-B280E7BC5E42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1d08596f8f0726fe564215fde6dd8caf61109ac9","datavalue":{"value":{"entity-type":"item","numeric-id":3192204,"id":"Q3192204"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875443$030BDF9F-641C-424B-9C21-536B496C00C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2df88df617383e402732a7ccdf3a5a43ea499743","datavalue":{"value":{"entity-type":"item","numeric-id":4645239,"id":"Q4645239"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875443$A5ED52EE-333A-471B-84C9-07B6CC4D3A86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"99ffbea81034595aebc9c4b96e785de56f2029ca","datavalue":{"value":{"entity-type":"item","numeric-id":2351147,"id":"Q2351147"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875443$D1DB9625-D893-4C60-BCCB-766AA84BD889","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d7ef381d718ff3d567687169a1320ca1dd0ccfbe","datavalue":{"value":{"entity-type":"item","numeric-id":1791171,"id":"Q1791171"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875443$BD44CAB7-935F-4144-80A5-B0CEFE3D61CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eec2568f4fb49cd31d8af7174cf456f4fdeb8249","datavalue":{"value":{"entity-type":"item","numeric-id":3010369,"id":"Q3010369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875443$A5D78A00-5139-417B-855B-7D7FFF73A933","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3dced7fd9d1f2d0b0d6bc79efb06acf36aab2e44","datavalue":{"value":{"entity-type":"item","numeric-id":4928458,"id":"Q4928458"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875443$08399494-4769-43BD-A49F-E3D6EA51323D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"13d9af80fb394b6d4ce6a003c012f88c509797ce","datavalue":{"value":{"entity-type":"item","numeric-id":2652481,"id":"Q2652481"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875443$E205A0BD-1F97-4AED-B846-CE6C41BD95EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6c3a48dc71ab7bc77b1ce9ffe6a02b960104792e","datavalue":{"value":{"entity-type":"item","numeric-id":5796041,"id":"Q5796041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875443$27E06390-116C-42D4-BFFB-A9D03E744398","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"174e3f2701a2bacd196e2d244539c0776079d382","datavalue":{"value":{"entity-type":"item","numeric-id":4858037,"id":"Q4858037"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875443$35D21AEC-B3BA-4793-8E3E-946572384B98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4243a855a95d15dcc52f4675bed6925988c3cdd1","datavalue":{"value":{"entity-type":"item","numeric-id":3183543,"id":"Q3183543"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875443$3C811A7A-A05A-411D-B0EF-DA29D8792859","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"38602d2b7fd482d2c85a2b53c450a23a2740fb43","datavalue":{"value":{"entity-type":"item","numeric-id":1663242,"id":"Q1663242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875443$FDB35773-D540-4422-89DB-16051A606C7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9b5595e66b8729293652ffa35d013832b424ee2a","datavalue":{"value":{"entity-type":"item","numeric-id":5747763,"id":"Q5747763"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875443$9CBCCC4F-163D-48C1-86A3-535EA0804F88","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fdd2ee201ccc4cecbec5cfb490e6a3352daba1aa","datavalue":{"value":{"entity-type":"item","numeric-id":3619270,"id":"Q3619270"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875443$E7EB75EF-FB4D-4E7F-BCF8-A2EECDAE83AC","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c0ba0e0ced7b6a724af6bfa75813d12c02c08a2b","datavalue":{"value":"10.4230/LIPICS.ITP.2019.31","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875443$9E42F75E-F473-42C0-9485-8E119C36804D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5875443","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5875443"}}}}}