{"entities":{"Q7027872":{"pageid":21670131,"ns":120,"title":"Item:Q7027872","lastrevid":77537207,"modified":"2026-05-05T00:00:40Z","type":"item","id":"Q7027872","labels":{"en":{"language":"en","value":"An SMT-based approach to the verification of knowledge-based programs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7984062"}},"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":"Q7027872$F777BF60-01AC-471F-B4C2-49A11B7AC8F6","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b83f23c99cf19661b6db511eb420ae087b89faaf","datavalue":{"value":{"text":"An SMT-based approach to the verification of knowledge-based programs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7027872$A97E6054-64E5-442A-B6B3-302BA795FFB6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"15310f8b3882178f7087c793014199d8d575a1e4","datavalue":{"value":"1558.68053","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7027872$08C40C95-440A-46B6-AE10-954A9D339ABE","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"78d1f3491448a10bd0253b750e9d2c8ea2622f24","datavalue":{"value":"10.1145/3700150","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7027872$487FDE94-4971-4F85-840C-1C2B43514B88","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"52000320d108ee6b6146ae320a672f6ae77321de","datavalue":{"value":{"entity-type":"item","numeric-id":785240,"id":"Q785240"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7027872$677F485B-2A78-45EA-AC92-E331DAECAFE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c76d101433f5e35590cea68128167d58f5915156","datavalue":{"value":{"entity-type":"item","numeric-id":2851355,"id":"Q2851355"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7027872$A93F9066-C136-4069-80CD-0050E27A4A72","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5e80469ccad547cffd757801ac819d677ad7e1e3","datavalue":{"value":{"entity-type":"item","numeric-id":1641033,"id":"Q1641033"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7027872$74B1EC4C-61B9-483E-B2B3-7A8C7315C39A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"0a4edb54a1ac9688e9e0cd95e98d133953c4bb32","datavalue":{"value":{"entity-type":"item","numeric-id":6174547,"id":"Q6174547"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7027872$6261230A-8D09-40C9-A6D3-45C57EB1A09B","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d9925518446645d219093152a820aba790417b61","datavalue":{"value":{"entity-type":"item","numeric-id":164203,"id":"Q164203"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7027872$E41CD4D7-A928-4CE9-9096-71149DC8106A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"eea347ba7555b724e15297c1d47ab41222d91cd0","datavalue":{"value":{"time":"+2025-02-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7027872$FF5CF6AF-EB4D-49C1-A160-47355ECBA872","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7027872$D1DEEE61-0D75-4E7F-8DC4-4B94CEFA5345","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"19e8b53914fe36a939b2f687be46776db2609217","datavalue":{"value":"03B42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7027872$E4DF2801-FA8B-4414-9AD6-0EBF6B3DCAAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7027872$27005EC4-D10A-4AE2-B453-9549C5DD5C0F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7027872$75FD8319-3467-4D76-9300-184866BE7F8A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"70abdaa10908dea15c7e3e0cc335602785664cee","datavalue":{"value":"7984062","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7027872$BFD6B5C5-E4BA-4914-99B0-2220C685340D","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7027872$85995DBD-7113-46BA-9D81-8219EBEE05D5","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb9f8004d477a3922fe8bde53d670f8b57c48852","datavalue":{"value":"model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q7027872$1C368835-DBF9-4D2A-8DFC-7FE9C85A8BFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"25b255b3f7f779539c5118a049f2680d4f791b91","datavalue":{"value":"epistemic logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q7027872$901A2C17-3054-41AB-97AD-88C98F5A2480","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8ec4d78ec35509138fe086cf8c2a2ba905307b05","datavalue":{"value":"epistemic predicate transformers","type":"string"},"datatype":"string"},"type":"statement","id":"Q7027872$4E2B41B0-1FA7-4A36-B9D0-15B9142E9F98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ae1478f0080b70574ea441c7d2a3b6db779c2f9c","datavalue":{"value":"program semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q7027872$5480ED9E-47D1-4929-A99C-C9FE81062E50","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":"Q7027872$D4AE5670-281F-427C-A551-C58AC0D3F8BD","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"4b0c7436976c5b9893e05c1462fed16a80d7904d","datavalue":{"value":{"entity-type":"item","numeric-id":5322945,"id":"Q5322945"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7027872$C6EAC70A-A84F-45FC-8747-585853D50F33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"adc87194f53a9552766b22cbe3fffae4e25dcae6","datavalue":{"value":{"entity-type":"item","numeric-id":2744124,"id":"Q2744124"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7027872$884C108C-AE82-452F-868C-39CBE8A9FDB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"05348a557d2dd187a82890860a29298cc18e12f9","datavalue":{"value":{"entity-type":"item","numeric-id":1109008,"id":"Q1109008"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7027872$A7F3FD34-6BB1-4614-9ECC-B4CA969620DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"67b8a6374b4fc895d89506f759c76e54380f8254","datavalue":{"value":{"entity-type":"item","numeric-id":4144755,"id":"Q4144755"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7027872$EED67B0B-862E-483F-AA05-1BDAD7F1E0D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9a51c4131406feb3360654a16bbe1b5f9a9ecfa1","datavalue":{"value":{"entity-type":"item","numeric-id":5361449,"id":"Q5361449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7027872$E334878C-85B9-4324-8676-DA27B81AC80D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2b5d4373326ddacd5ad0928810272cc7a23b3585","datavalue":{"value":{"entity-type":"item","numeric-id":5312933,"id":"Q5312933"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7027872$85ED88BB-C298-4A6D-81F2-FB032F6F47AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"247edb4d29125065a4b7bcb1f8e741cd7f4f6b4c","datavalue":{"value":{"entity-type":"item","numeric-id":5215818,"id":"Q5215818"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7027872$B40566ED-71B0-4D1C-9AF2-0DE906EF45F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d0e3a179147832b2b1c96869b8d44ccac54dac91","datavalue":{"value":{"entity-type":"item","numeric-id":4343990,"id":"Q4343990"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7027872$D0BEBC19-9EF8-4746-ABDA-8ABC34F35295","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"323dbd6fd6973b3663055cf97da83be885dd9ec7","datavalue":{"value":{"entity-type":"item","numeric-id":5569944,"id":"Q5569944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7027872$AD63964C-A2C4-4D24-BA0C-3C287A0DBCC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"57ee09d94bfcf54044ba878c48690e939ed437ef","datavalue":{"value":{"entity-type":"item","numeric-id":5486061,"id":"Q5486061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7027872$3DCC0514-64D1-4AFE-BF2A-BA32E2719195","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7d50c524c53d7f49976000982a6078db3bc09507","datavalue":{"value":{"entity-type":"item","numeric-id":5506377,"id":"Q5506377"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7027872$95350B3B-5858-41AD-8C0B-BEC1F5C9F3DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b762df6d7899899353ce32a9470e3db827ed0388","datavalue":{"value":{"entity-type":"item","numeric-id":3393399,"id":"Q3393399"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7027872$01F77C7F-8AD2-4009-9CD0-66A827F7723B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"768da93377b5dbe67ffc466d796d0d32932c2d63","datavalue":{"value":{"entity-type":"item","numeric-id":4301161,"id":"Q4301161"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7027872$ABAFD510-C512-4409-8FE2-076085AADE17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5a16832655d058fb294cac06bffb86b23e4284b9","datavalue":{"value":{"entity-type":"item","numeric-id":3618832,"id":"Q3618832"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7027872$DDE12025-8814-45BC-A6C6-150CDA390467","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a125502fa850f6a5ab3619570f7db924c393b3b","datavalue":{"value":{"entity-type":"item","numeric-id":3680260,"id":"Q3680260"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7027872$D49A9C2E-6978-4053-9CF8-A0E0FEEB36E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"33b3574f20806a66708da96ce707a437eabe8496","datavalue":{"value":{"entity-type":"item","numeric-id":6174548,"id":"Q6174548"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7027872$887591B7-D5E6-42A8-B110-F47CC23D5ED8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bd581593d9945acc067d150d7876e9a41087ba0a","datavalue":{"value":{"entity-type":"item","numeric-id":3457719,"id":"Q3457719"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7027872$BC47E6A5-0F76-45D8-A417-A81094564866","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"802f07812275fb2aa622ee7c7fe0cfed1f7c0e0f","datavalue":{"value":{"entity-type":"item","numeric-id":4648829,"id":"Q4648829"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7027872$F956DB6F-9725-4C66-B0FF-10E3B5A9CDF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"04adff89bc96cf899336247629fa57fcdf5761b4","datavalue":{"value":{"entity-type":"item","numeric-id":2716928,"id":"Q2716928"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7027872$AD9C9728-FBD6-45ED-8CB4-7907BDE30EF7","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"An SMT-based approach to the verification of knowledge-based programs","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/An_SMT-based_approach_to_the_verification_of_knowledge-based_programs"}}}}}