{"entities":{"Q7361841":{"pageid":31521062,"ns":120,"title":"Item:Q7361841","lastrevid":105369776,"modified":"2026-10-07T13:38:39Z","type":"item","id":"Q7361841","labels":{"en":{"language":"en","value":"Knowledge-based programs"}},"descriptions":{"en":{"language":"en","value":"AFP entry KBPs"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"2c55817fc8404e71ef070cf40185de3a5acee2da","datavalue":{"value":"https://isa-afp.org/entries/KBPs.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361841$069D6FB3-719F-4A9E-8383-C2B34F62F096","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"83c297f9d20352ea42cab9969ba7b8ed227e2a66","datavalue":{"value":{"time":"+2011-05-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361841$D53AADCF-6945-4268-B5D0-491614AC6FF8","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"81cd49afe7b0c7730911232a5003ad6efb86ef85","datavalue":{"value":"Peter Gammie","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361841$216A0286-26DB-464D-8E1A-5D9487A9DE0A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8b256d9789a74bd941bc6c5a5c7dec2c0ecfc369","datavalue":{"value":{"text":"Knowledge-based programs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361841$5E3BD609-6747-4875-A579-3AB0450ECAAC","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"53889439efa990832eb121c08722e432683bdfc5","datavalue":{"value":"Knowledge-based programs (KBPs) are a formalism for directly relating agents' knowledge and behaviour. Here we present a general scheme for compiling KBPs to executable automata with a proof of correctness in Isabelle/HOL. We develop the algorithm top-down, using Isabelle's locale mechanism to structure these proofs, and show that two classic examples can be synthesised using Isabelle's code generator.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361841$2D7A75C4-969F-4EDB-A154-2F5F2501788C","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"403738ebc449032b2c0b132c2ef1a436783bf929","datavalue":{"value":{"entity-type":"item","numeric-id":3183526,"id":"Q3183526"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361841$48AB063E-C6D7-4B2C-A7BE-434BC976E259","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a7ac3d7ec2b15acefd0efec27878eb9b4d230b02","datavalue":{"value":{"entity-type":"item","numeric-id":3867808,"id":"Q3867808"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361841$7272AD85-66B1-45D6-BC54-32D9CC11792C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"86a51682206d507eefa10fca5eab6a2bf98ec271","datavalue":{"value":{"entity-type":"item","numeric-id":1763061,"id":"Q1763061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361841$D40ACDE1-9133-4EDB-95EF-FF423E216EC7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1ea1e49654139a8bf01fb7d2509265fe22e72d56","datavalue":{"value":{"entity-type":"item","numeric-id":1026424,"id":"Q1026424"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361841$E51E92AA-BE4C-4194-8DB7-E1C229BCCEBB","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":"Q7361841$AAC3ADC2-F212-4703-B028-54C3EF2E2596","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6fc65e36060e1ae572d6566999dbaedabd05f274","datavalue":{"value":{"entity-type":"item","numeric-id":983522,"id":"Q983522"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361841$546D00D4-229F-471C-9A37-2AF6157797BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22a5a326924c9f9f3cf0f5061fb0ff950ccfad0d","datavalue":{"value":{"entity-type":"item","numeric-id":5747660,"id":"Q5747660"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361841$46F91285-E947-4EEC-BA84-53EA91BA387C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4dea4591678b15a6cab034d35b86cc0cea33c36d","datavalue":{"value":{"entity-type":"item","numeric-id":2565501,"id":"Q2565501"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361841$E55AC94C-296E-4B5F-98F6-A7F12D0353AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"857d58e6cf6a08774c10e1ecad1e4218c0cb01d1","datavalue":{"value":{"entity-type":"item","numeric-id":5705941,"id":"Q5705941"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361841$9F84EB88-9576-4533-9DD7-58A753A4A3FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f76b2805ab30acd042efa64a78eed36e3cf5fb85","datavalue":{"value":{"entity-type":"item","numeric-id":2370664,"id":"Q2370664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361841$7440B26A-6D9F-4B31-A834-83595A050C0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9689d3285995afb42633d6587b8f7ef68cfb9e38","datavalue":{"value":{"entity-type":"item","numeric-id":5756774,"id":"Q5756774"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361841$DE28A1F7-5D18-4944-A2FD-8D470A6F668E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"efd8ae02adfedbc0c31ce15b0873e8f177400bb2","datavalue":{"value":{"entity-type":"item","numeric-id":2554307,"id":"Q2554307"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361841$1C329675-F21E-4EB8-9071-75BB33C72985","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"91ed9fc3eb12713a9175063c08eca78a2683dead","datavalue":{"value":{"entity-type":"item","numeric-id":5137342,"id":"Q5137342"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361841$C2ACBD78-6292-48DE-A6E8-48DF406EA45D","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":"Q7361841$B038964A-6DF1-4FD5-BB00-B9F566ECB992","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"94a2193ae14199da925d7af311a9e576826127c4","datavalue":{"value":{"entity-type":"item","numeric-id":1383157,"id":"Q1383157"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361841$058C6569-2E6E-4032-9B72-406CA2219B06","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1bab0742153e7c673f92f7bcfbd9abb7d04d6539","datavalue":{"value":{"entity-type":"item","numeric-id":1193742,"id":"Q1193742"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361841$A9F3A9BF-CE2D-4277-823E-0F366E17BD0E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"49821ed381a97cd75d73a147e2022ad36627abe3","datavalue":{"value":{"entity-type":"item","numeric-id":5738907,"id":"Q5738907"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361841$E461EE78-2AA9-414A-B9C3-62CF055F879B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"19f6c194330051269cbb2031658aa6b4220e257c","datavalue":{"value":{"entity-type":"item","numeric-id":4702189,"id":"Q4702189"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361841$2BBDE203-6EB8-40A2-9078-AA9DCC33DC71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5c6ae9995834210b0974f14d3d0975fe462d18d1","datavalue":{"value":{"entity-type":"item","numeric-id":4508297,"id":"Q4508297"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361841$7F2EF3F1-4374-49BF-9711-56F84E952B89","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2990e15db3ec1299bacd39e760b2d345098c103a","datavalue":{"value":{"entity-type":"item","numeric-id":4845472,"id":"Q4845472"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361841$9826E7C0-37C7-47BB-81EE-B5D0B57FC1E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"931c42c28f22f89fe1b66164f9ececc2021ac1a2","datavalue":{"value":{"entity-type":"item","numeric-id":3558332,"id":"Q3558332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361841$1705CD85-94CE-48B6-810E-6B2522B2A71C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0fe5b32ebe1b29b2edc3575e3da562e9dea8cd2f","datavalue":{"value":{"entity-type":"item","numeric-id":3376919,"id":"Q3376919"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361841$C0316FBA-2E67-410A-BB1A-EB5F50981C88","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2be2ce44bdf80df52f5a97dfe72ac01ea51570a9","datavalue":{"value":{"entity-type":"item","numeric-id":4045961,"id":"Q4045961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361841$50BF3C8B-5101-470B-9829-E010AC6557A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4c704ff998b44e195f6134a4f2cef8f379bf3acc","datavalue":{"value":{"entity-type":"item","numeric-id":4180316,"id":"Q4180316"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361841$A663C5DC-DD72-4615-B849-94D9472391DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361841$376DA4FB-28E0-4700-BAE8-4EB08F2A94BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"65fa25ecef461a83ce03679a7bacb00b33cb4090","datavalue":{"value":{"entity-type":"item","numeric-id":3801084,"id":"Q3801084"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361841$23F802E7-5B26-4D8C-AFBF-ADD1FAEE1781","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"68be494fc7d5864d1d2b8840b65dee952d16f98a","datavalue":{"value":{"entity-type":"item","numeric-id":6567777,"id":"Q6567777"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361841$1F107836-1A6A-4FFB-B550-4ED662C023C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5a70244376fd4d1562b321cd168af407a5c82ef","datavalue":{"value":{"entity-type":"item","numeric-id":3574001,"id":"Q3574001"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361841$FD39171B-6865-423B-B44E-D1CB67B331D4","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361841$FDCA07F6-2847-4460-A01A-7D5B1BBB8840","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"1954018ee2fbe7a1674df4032b4e8f1c6489eae7","datavalue":{"value":{"entity-type":"item","numeric-id":7361316,"id":"Q7361316"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361841$8CA393CB-4465-4DC5-B2B1-71CC36564E5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"b3a2297d5bff32b90586f57127478a7b0e327c28","datavalue":{"value":{"entity-type":"item","numeric-id":7361170,"id":"Q7361170"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361841$5C0DE890-49BF-474D-AD46-4376E5523C95","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"73d93a21b0749f7f2c51d7daeb11b162660cd756","datavalue":{"value":{"entity-type":"item","numeric-id":7360784,"id":"Q7360784"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361841$03F9505D-F75F-4294-AB26-649787549EFF","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361841$76BD9F6E-F4E6-4C9C-8286-5BEF84D567EB","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Knowledge-based programs (AFP entry KBPs)","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Knowledge-based_programs_(AFP_entry_KBPs)"}}}}}