{"entities":{"Q757074":{"pageid":758923,"ns":120,"title":"Item:Q757074","lastrevid":64103328,"modified":"2026-04-11T17:39:57Z","type":"item","id":"Q757074","labels":{"en":{"language":"en","value":"Generalization in the presence of free variables: A mechanically-checked correctness proof for one algorithm"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4193140"}},"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":"Q757074$2989C85C-40F5-4206-A779-4CE5457325BA","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cc1665101b2185f4eeeabf48e7ee728cd8629abc","datavalue":{"value":{"text":"Generalization in the presence of free variables: A mechanically-checked correctness proof for one algorithm","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q757074$B0355FF7-6D41-47DD-965A-6A78107653FD","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c54b7456c319710091f6f1af937c2d09c595cb2d","datavalue":{"value":"0723.68072","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q757074$934D9479-C637-4525-B873-A9D72E934992","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d902687668f502658b9f12c7d8c3b6eed2523a4a","datavalue":{"value":"10.1007/BF00249356","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q757074$CD09D3AB-73E4-4F10-ADD9-E4D71B8C6CFA","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e6bbab2ea230ef82cf7d72bee404dd827d5aaeed","datavalue":{"value":{"entity-type":"item","numeric-id":230814,"id":"Q230814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757074$58FEF3AA-C752-4B38-B4C7-9DA880F8CFB3","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757074$1294CABB-7489-4B09-9724-34C8891B2231","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"391107ffc7a24346d69c573e292e4ff4587e3aaa","datavalue":{"value":{"time":"+1991-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q757074$61BF7AE3-8585-4A15-8B7D-7953A1CBA733","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q757074$17E7035C-DFEA-4512-96FE-839EF208FC4D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q757074$9FBBEB4B-08D6-4B14-8A80-3376B190F3C1","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e05967d0c1b01d64d5a59c4fc14c435373a5725d","datavalue":{"value":"4193140","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q757074$F82A1FDA-964F-4D1C-8217-9CC21862681F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"69020b90f2a295125077d4c830cfc6ef19605b9f","datavalue":{"value":"free variables","type":"string"},"datatype":"string"},"type":"statement","id":"Q757074$AC07267A-0180-44CE-9BD6-1F791DAFC469","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"88524e08f921927037ac8f544920df56683b67bc","datavalue":{"value":"proof-checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q757074$92AA7E01-D86D-4179-A436-856DA0A42410","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1dc9283eec564759c117cc6888635408907541c0","datavalue":{"value":"case study","type":"string"},"datatype":"string"},"type":"statement","id":"Q757074$391101A2-B52F-44BC-91D4-EBE5A98B7B79","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"67935c9745e86097c5a009e8bb47d5846729f37a","datavalue":{"value":"Boyer-Moore theorem prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q757074$0CAF092B-A21C-474E-ADDE-CDBF31C1294E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"32089794c559051e9fe3202986acc490c45fac8d","datavalue":{"value":"generalization","type":"string"},"datatype":"string"},"type":"statement","id":"Q757074$8A218AAE-EDF9-4042-8850-DA959FABD31D","rank":"normal"}],"P1463":[{"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":"Q757074$2C68C67E-A194-49B0-9FB9-23257BBE2A09","rank":"normal"},{"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":"Q757074$1F2876AD-FE9F-49DE-B740-AB3377FF192B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a8f057223c758d6b8295ecbdef4842faac2ccb72","datavalue":{"value":{"entity-type":"item","numeric-id":19253,"id":"Q19253"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757074$54B121A6-A1CE-4276-AA2F-DCB81904A47A","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":"Q757074$B51C11D0-B645-462C-B742-1C384CA3119B","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"12190f9905af836a184e6c2b8d54ab945d519f3e","datavalue":{"value":"https://doi.org/10.1007/bf00249356","type":"string"},"datatype":"url"},"type":"statement","id":"Q757074$959A703B-6DC1-4CFE-BD10-BBA375A89B12","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"f25214f941f53a79c1a6b11250366f1b10ef2472","datavalue":{"value":"W2011482734","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q757074$59BECB0C-6A40-4B80-86D8-41051FBF94B4","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d908e08ad0c92e66a3fe593f78c2ee7606034207","datavalue":{"value":{"entity-type":"item","numeric-id":4647499,"id":"Q4647499"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"56ba9db9f8e561075f23492798f124873bfd317c","datavalue":{"value":{"amount":"+0.83805937","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":"Q757074$4D0E8B20-AA52-4790-A273-251E9FEA5A38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3df2062477e400153324e8a42104b32141a25c9f","datavalue":{"value":{"entity-type":"item","numeric-id":2265798,"id":"Q2265798"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f52d5f7570da8f7a1ef21cc72b307bc8bc80edfa","datavalue":{"value":{"amount":"+0.8301405","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":"Q757074$27D5D1C3-BC36-4854-B1E0-65B8D7E6C7C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ec13e45ef748ecb11067afb389d5e76fb4ef4d18","datavalue":{"value":{"entity-type":"item","numeric-id":1601844,"id":"Q1601844"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fdbd77ebf32c56f9e75c88fa2d7550b31fc80704","datavalue":{"value":{"amount":"+0.826646","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":"Q757074$32579D7F-F5FA-4C0A-B472-5E3D5B09B664","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f1166311918e3c6af2922eb749de591eb423ccf5","datavalue":{"value":{"entity-type":"item","numeric-id":4736998,"id":"Q4736998"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1e4e8efeb787338d25f165e13c7dff9019c789f2","datavalue":{"value":{"amount":"+0.821758","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":"Q757074$DFE557DC-15B2-4CD1-8F7D-C8B6D0AE2069","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"95d94cbff399b52ce290d6665cc0895afd6f85f8","datavalue":{"value":{"entity-type":"item","numeric-id":5307075,"id":"Q5307075"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fa7b30b294126a7298d745babc04fd00f3f41e88","datavalue":{"value":{"amount":"+0.8180567","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":"Q757074$084F2FAA-ACCE-4A7A-93B6-ADB3A67D6B89","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"323796dcb37a3b4cbae9a2fc72c1089915817e8e","datavalue":{"value":{"entity-type":"item","numeric-id":5012056,"id":"Q5012056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e322eaf5f85d06ae6ee206df9b25a62284616e97","datavalue":{"value":{"amount":"+0.8167582","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":"Q757074$C044E2F0-1CA4-422E-BCD2-DE63778B1310","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1ad899c7f970aa799dee1b66ebbeb719da938c51","datavalue":{"value":{"entity-type":"item","numeric-id":5234895,"id":"Q5234895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8e007a3afedc8edf64a0612aea321cbf8aead27b","datavalue":{"value":{"amount":"+0.8154373","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":"Q757074$5BC85593-9339-4917-8528-AFADE2776031","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9b8276ca81ef811bc52b0536aea4bd09cca2edcb","datavalue":{"value":{"entity-type":"item","numeric-id":5299583,"id":"Q5299583"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1767c3f99801766761ba75fa5fa97fed2ae602fa","datavalue":{"value":{"amount":"+0.8144813","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":"Q757074$A10C5CE0-7793-44E7-9E17-39698B4DE9ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ecde783ffcecb2434079b39068a97bff8336fbeb","datavalue":{"value":{"entity-type":"item","numeric-id":5554975,"id":"Q5554975"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ad28806fbc8fe98052e285cdbe853b54ad8527fc","datavalue":{"value":{"amount":"+0.8144652","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":"Q757074$503C8371-D68F-42C6-959C-23C59CDFD8F9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Generalization in the presence of free variables: A mechanically-checked correctness proof for one algorithm","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Generalization_in_the_presence_of_free_variables:_A_mechanically-checked_correctness_proof_for_one_algorithm"}}}}}