{"entities":{"Q7027872":{"pageid":21670131,"ns":120,"title":"Item:Q7027872","lastrevid":76765380,"modified":"2026-04-25T01:22:12Z","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"}]},"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"}}}}}