{"entities":{"Q7361250":{"pageid":31519289,"ns":120,"title":"Item:Q7361250","lastrevid":105364361,"modified":"2026-10-07T13:35:19Z","type":"item","id":"Q7361250","labels":{"en":{"language":"en","value":"The string search algorithm by Knuth, Morris and Pratt"}},"descriptions":{"en":{"language":"en","value":"AFP entry Knuth_Morris_Pratt"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"830c59a2e64cb1b347b2e61a8b50382921902adf","datavalue":{"value":"https://isa-afp.org/entries/Knuth_Morris_Pratt.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361250$DA8CC16C-C152-409D-8232-00C7F45C3AEE","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9bd6b55577e7ffdb7837b8ca322f8a7d1011d8a1","datavalue":{"value":{"time":"+2017-12-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361250$9AF975C6-3DC3-4C4A-8728-4BB30D90F4C4","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"7367b16d2a7a3d3a354751cf4004ad9db8d21825","datavalue":{"value":"Fabian Hellauer","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361250$FFB8958A-D652-4B4F-874E-6E949C3E5E87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"7545c5768cca6bd4b47e52bfec18c22cb81849df","datavalue":{"value":"Peter Lammich","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361250$124CD648-DEEE-48AF-80A1-A4FAA071F89F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"43a706250b8e964d17331dff1d6f6fc46a5d1eb9","datavalue":{"value":{"text":"The string search algorithm by Knuth, Morris and Pratt","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361250$7AB8D05F-7CE7-4700-A80D-1840FF9CC45E","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"55848613e228a509c7a35e96c21f2720128c093d","datavalue":{"value":"The Knuth-Morris-Pratt algorithm is often used to show that the problem of finding a string s in a text t can be solved deterministically in O(|s| + |t|) time. We use the Isabelle Refinement Framework to formulate and verify the algorithm. Via refinement, we apply some optimisations and finally use the Sepref tool to obtain executable code in Imperative/HOL .","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361250$46E1777F-EC36-4B24-A990-F3F4EA633D1F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"cac7f741f9b1e3426d597355d63b43bdf762c36a","datavalue":{"value":{"entity-type":"item","numeric-id":4148937,"id":"Q4148937"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361250$3682A7DC-76D0-4F80-99A5-41DEFFDD4D49","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":"Q7361250$B418E1AA-4FA5-44B9-AB3C-FE8B73EF5628","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"6df1e1600a3acc40d1b0a9c9cf7cbc177462ddf9","datavalue":{"value":{"entity-type":"item","numeric-id":7361373,"id":"Q7361373"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361250$A5519367-A045-46F0-9753-509EBA140F9B","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"1157f6239d5752bb0ad1cee836272bd46c6bf40f","datavalue":{"value":{"entity-type":"item","numeric-id":7360772,"id":"Q7360772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361250$CC0702BC-5A83-45BE-903F-80FF76263BCB","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":"Q7361250$DDCA8499-8335-4784-8D0F-CEB45B8C0FE5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The string search algorithm by Knuth, Morris and Pratt","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_string_search_algorithm_by_Knuth,_Morris_and_Pratt"}}}}}