{"entities":{"Q816208":{"pageid":818056,"ns":120,"title":"Item:Q816208","lastrevid":64551504,"modified":"2026-04-11T20:39:33Z","type":"item","id":"Q816208","labels":{"en":{"language":"en","value":"A complete mechanization of correctness of a string-preprocessing algorithm"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5007758"}},"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":"Q816208$3A93CE8E-DDA2-4D3A-9484-A0A94C994421","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f4276ee7a2b6f251ace09cb9332862a7b734058a","datavalue":{"value":{"text":"A complete mechanization of correctness of a string-preprocessing algorithm","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q816208$591B90EB-009E-4E61-A2C4-88B23079292D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"645f12bb55fbcbe296d11886de7520894d30d954","datavalue":{"value":"1085.68149","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q816208$95ADEA3A-826A-45EB-ABB5-AD69B56CD4DF","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b45ca94dcba2704987f936f4ff73a33f6f53d6f6","datavalue":{"value":{"entity-type":"item","numeric-id":816206,"id":"Q816206"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816208$694780F9-DEA3-4577-89FD-7A2D354B5356","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"62473f5497f1f89186bab469652d8b9aefe97ede","datavalue":{"value":{"entity-type":"item","numeric-id":816207,"id":"Q816207"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816208$E7FA8B9D-72E2-424D-9836-7BEF0B3CCE7F","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"70551fcc6e89042fc26ae9242a005533b44a2d7a","datavalue":{"value":{"entity-type":"item","numeric-id":169908,"id":"Q169908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816208$B3D07EAD-DD97-44E5-8256-C7E575C3C375","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d5a46ca8715888f9181d63a117c8c9aa412098d3","datavalue":{"value":{"time":"+2006-02-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q816208$67B95E4E-F5AC-4DEE-8F95-8BBF5793B93B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q816208$BD145ED8-F309-4D96-BAF2-1417FDE84341","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"3f97694d44af155a68434cb72eabc6a4d5dd5227","datavalue":{"value":"68P10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q816208$3ECE74E6-7E86-4367-AAE2-BAB4034BD039","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a0173b49019261d7805d9e2343de9753668b962f","datavalue":{"value":"5007758","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q816208$231CD841-8D87-4FFB-91FA-758B08BAFD74","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f02f4db7bd17ba3fbae1be6bcee13dc9e5aa86bc","datavalue":{"value":"formal methods","type":"string"},"datatype":"string"},"type":"statement","id":"Q816208$CB55F8B9-E2A4-4AF5-8502-93AC8D6269C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2450e02f50939b46b52c3140c8d1d485cebe36e5","datavalue":{"value":"pattern matching","type":"string"},"datatype":"string"},"type":"statement","id":"Q816208$CFD8D511-AA5C-4848-8CF1-CF6FD7EE048A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q816208$FAC951A7-AD61-44E4-A551-201215EE734D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b3d3d0d2409011411be91984a4137a1c90ca04ff","datavalue":{"value":"PVS","type":"string"},"datatype":"string"},"type":"statement","id":"Q816208$3CC7D9D7-C904-4C1D-A034-0C9F2F67DEAB","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"27b6ae20da44d6f09b655d9481cc0df08a8ffcdf","datavalue":{"value":{"entity-type":"item","numeric-id":18826,"id":"Q18826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816208$AE90DF49-4C8D-486A-BFFD-1AE90CA0A938","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"17cfe6afe68a54e81dc559ef2cd5a702765207b0","datavalue":{"value":{"entity-type":"item","numeric-id":25375,"id":"Q25375"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816208$94B5E2EF-5D14-4058-A0FA-32690E16C6EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816208$C33E80AC-6097-429B-B1BB-6B8945173791","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816208$AEA097F4-E6D4-42CE-B77F-95B5D8503092","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2b02b46847f3d7e3a5825b9484a88607b98dbd14","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816208$01F38E09-3ECA-4080-B07E-13E4867C01A4","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":"Q816208$1C77B952-B03E-425F-AF8D-ACFF707FB836","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a4fd47df2bd70bcfa40fa8bcd6376085ef68c1d2","datavalue":{"value":"https://doi.org/10.1007/s10703-005-2243-0","type":"string"},"datatype":"url"},"type":"statement","id":"Q816208$E1D7ACFD-1813-4279-A8AD-193A1877F2B4","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ae239177f4334d2c21e24cb507ba76392188fb88","datavalue":{"value":"W2008530822","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q816208$77F1DE10-1934-41D8-989C-1FDF95A8A653","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"bd3d06510851d82dfb1e7b6453192d4ed8bc5f3e","datavalue":{"value":{"entity-type":"item","numeric-id":4385510,"id":"Q4385510"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816208$48764063-B51D-40C0-B107-DDAEC94BB357","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"74e200c4f897ac4cb0c5ae9f1bab6477c1d7e3dc","datavalue":{"value":{"entity-type":"item","numeric-id":3090391,"id":"Q3090391"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816208$4394C633-7D2C-48B1-A79C-FF74A90B2C85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"090e4b104dd3f76f7e7cbd674cb41b2227a87ff1","datavalue":{"value":{"entity-type":"item","numeric-id":4692502,"id":"Q4692502"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816208$B3784026-0C66-4523-9410-5A27FF01CD2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"11eefd7e7dc86c1755a8db4c6825e6e9fdeb6d39","datavalue":{"value":{"entity-type":"item","numeric-id":3619797,"id":"Q3619797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816208$3E6A300F-A92D-4A55-8E7F-9A594B864336","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df6d745c28f41f3f6887e89cc1ca892988e70309","datavalue":{"value":{"entity-type":"item","numeric-id":5287513,"id":"Q5287513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816208$8392F48C-C208-49ED-B0D5-55E12035D8A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"138d808c1a0d7bbfa300ea1020e86219b9fb4bf4","datavalue":{"value":{"entity-type":"item","numeric-id":4229812,"id":"Q4229812"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816208$DD038438-DFA2-44B2-ADC3-C80E4A40BB52","rank":"normal"},{"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":"Q816208$BA11040F-5B00-436E-9A00-0EBFF5B5DC13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4968b8cabc6e7e2146fbbb19353be5139e1037e5","datavalue":{"value":{"entity-type":"item","numeric-id":4002642,"id":"Q4002642"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816208$AFC5EBCE-12F5-450B-9650-AC286CEE4592","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e1b88cf6e3a397ac11d53df2834c5ae5f2e6e6eb","datavalue":{"value":{"entity-type":"item","numeric-id":3891776,"id":"Q3891776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816208$480493C8-8132-41C4-827E-984E6F3364F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c7721eed45b9710530b7b58c997a4776836d5e85","datavalue":{"value":{"entity-type":"item","numeric-id":1853605,"id":"Q1853605"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816208$5845433A-7ABF-43AB-B7AD-F5925D383D1C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9092d0fee6fe1cbfaccbbd7a6309d60bb36d140e","datavalue":{"value":{"entity-type":"item","numeric-id":1924627,"id":"Q1924627"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816208$68AE1F4D-5BB4-498C-9B94-D0533C99E51C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"122a82d925981d2bcdd58674c0810d1b2b47a0c6","datavalue":{"value":"10.1007/S10703-005-2243-0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q816208$7FD89C4F-2F4A-42E3-874D-FF81D98C2BED","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e5a38c66ab2bdd65ff3d01bfc97043b16083a970","datavalue":{"value":{"entity-type":"item","numeric-id":2051812,"id":"Q2051812"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"40e5657604e7e303ce9f2ccd9a4fe30aaa55ff28","datavalue":{"value":{"amount":"+0.8388537","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q816208$345BFB1A-9DBE-4FAE-B1CB-95B109F2A49D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"17ec553daf91da49b905a87f1f13aa91cbd1186e","datavalue":{"value":{"entity-type":"item","numeric-id":1403072,"id":"Q1403072"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a510feccb9cb06b5b2387f438ae7d057bd441895","datavalue":{"value":{"amount":"+0.8373362","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q816208$221FB7FA-E27E-450E-875A-D12B3EA35D8C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b78168612ce8c6dd76d3615f11091ac9852c506c","datavalue":{"value":{"entity-type":"item","numeric-id":5061883,"id":"Q5061883"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ec6fe1418ca2d8845b977058dea145541c1f201d","datavalue":{"value":{"amount":"+0.834853","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q816208$D2084556-69CA-4651-AFEC-F23EE698CE1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8e1ce8e829975cee099ed3bc76d1c3b3da14a382","datavalue":{"value":{"entity-type":"item","numeric-id":4608614,"id":"Q4608614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ec6fe1418ca2d8845b977058dea145541c1f201d","datavalue":{"value":{"amount":"+0.834853","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q816208$71002AA8-3A0A-4C18-AD0B-4B072747F9EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1eeadda1685ffcda0409727ef7e3fb0cd7984877","datavalue":{"value":{"entity-type":"item","numeric-id":3075486,"id":"Q3075486"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"15092b7c48754b51ff1b6cabd02d85c4e7f9529a","datavalue":{"value":{"amount":"+0.8333078","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q816208$76A39E95-9709-4755-A3F2-82EC6DDEF4B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cd33b9c81053b88101cb2412ce8e1ea1aa49eca1","datavalue":{"value":{"entity-type":"item","numeric-id":1853605,"id":"Q1853605"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1805baaf5efded2aeb32f5e5bab77d0eb700de5a","datavalue":{"value":{"amount":"+0.831826","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q816208$87FAE186-4242-4489-8C5F-8ECE815812C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f4eb1de9692bd4a5efb433c155e896e596a3020b","datavalue":{"value":{"entity-type":"item","numeric-id":850497,"id":"Q850497"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"240c4fcc789a98583bbc7e9dfb006f6a407117a2","datavalue":{"value":{"amount":"+0.83112526","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q816208$35EECECA-ABC4-4EA2-BDBA-500C7750E741","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dbb3ca15e02a8a61fcf6e9bd29c66d7baa99fcca","datavalue":{"value":{"entity-type":"item","numeric-id":3617765,"id":"Q3617765"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"48a3c263ab85a3c11108233f6af003f446174248","datavalue":{"value":{"amount":"+0.82708347","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q816208$DA18F93B-5196-491F-AAFE-E0369196A9FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"964b145461e7fb364cf3495de52f801fd1ab0e81","datavalue":{"value":{"entity-type":"item","numeric-id":911767,"id":"Q911767"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2c8232b4c8876df181ed0f09c2789abb61c05197","datavalue":{"value":{"amount":"+0.82597816","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q816208$511FEFE2-0852-48C1-BCE9-1FBE89494F26","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A complete mechanization of correctness of a string-preprocessing algorithm","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_complete_mechanization_of_correctness_of_a_string-preprocessing_algorithm"}}}}}