{"entities":{"Q809617":{"pageid":811465,"ns":120,"title":"Item:Q809617","lastrevid":64539189,"modified":"2026-04-11T20:34:03Z","type":"item","id":"Q809617","labels":{"en":{"language":"en","value":"Experiments with proof plans for induction"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4213477"}},"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":"Q809617$79762C43-4A25-460B-B1F8-FF02BBF839FB","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0195faea28421eb95e1bf1f5a7e7c2d06d84fe04","datavalue":{"value":{"text":"Experiments with proof plans for induction","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q809617$B9248BD9-91E4-41BF-952A-6BE92C2CC495","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b5036a3d29b33ef4cdef8d9efd1c123f669cd4f4","datavalue":{"value":"0733.68069","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q809617$08B0DE01-46F9-4BB4-9904-8F03EEBAB00C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ffc27407dcb8ada9a8804603b5a5a479cd5cefa4","datavalue":{"value":"10.1007/BF00249016","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q809617$CEEE1582-ECFB-4EDC-A92C-585A084807CF","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d37a3d6bd9a0b44736f3bc6a6985f44383a95724","datavalue":{"value":{"entity-type":"item","numeric-id":438542,"id":"Q438542"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q809617$4F9ED6A3-B381-4088-BF6D-83FAC21D5E5C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f1b1c950eb38f4d88b02903eee30b03dcded1976","datavalue":{"value":{"entity-type":"item","numeric-id":685546,"id":"Q685546"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q809617$44A34024-7E4E-4EC7-A659-5902B950286D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"9915fee607d65e6b3e550829629b59bb040576a5","datavalue":{"value":{"entity-type":"item","numeric-id":809616,"id":"Q809616"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q809617$BD696BB8-6C4E-45B5-B56F-22EBCB03C022","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6df844f896d888573d76c54cedfde12049f28d2a","datavalue":{"value":{"entity-type":"item","numeric-id":540693,"id":"Q540693"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q809617$69A10C87-414A-45DB-9EFB-B70D9F33EB34","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":"Q809617$2E11ABE7-B51D-404A-8BE7-3C00B427C6B4","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":"Q809617$B19F384F-95D9-4E2C-8D1A-451637506507","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q809617$CFB7A67A-C481-4C68-B7E3-FDD0C9F0D1E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q809617$E0742601-3503-448D-B26A-9ADD83D3BEAC","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1ffdeca62254a408b26cddd068257a2423c68129","datavalue":{"value":"4213477","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q809617$DAA6BD1E-1B6B-41C3-9790-27C62DDA5076","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4518906703ac547f79888d08670823c3951a15da","datavalue":{"value":"program synthesis","type":"string"},"datatype":"string"},"type":"statement","id":"Q809617$B4CF91EF-0381-44FE-B6C1-AB2BB19AA8F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"aeabe59d4757581b815c17ebf3296713b3550096","datavalue":{"value":"proof plans","type":"string"},"datatype":"string"},"type":"statement","id":"Q809617$481D23C4-0E44-44F4-AB16-98AEC3033ED1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1f269977a25fe087b7007d36378986cca32ece60","datavalue":{"value":"combinatorial explosion","type":"string"},"datatype":"string"},"type":"statement","id":"Q809617$5DA9B634-2661-41D0-AF85-63D97B68E478","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q809617$5E35FA91-4724-4BF8-84EF-7394A3776550","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3b97b327acd29bc543e319ce1a45374500e4b98f","datavalue":{"value":"mathematical induction","type":"string"},"datatype":"string"},"type":"statement","id":"Q809617$A240B818-15E5-492A-9CE6-0133E84D6B75","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7c80ecf21428f980362763aa3ec34b156b15c6fc","datavalue":{"value":"tactics","type":"string"},"datatype":"string"},"type":"statement","id":"Q809617$5CC0B735-78CB-4AC3-8CA1-A8CEEC788A27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f27463e37810586c8ae270a4bebcc856a2ef7330","datavalue":{"value":"Searching","type":"string"},"datatype":"string"},"type":"statement","id":"Q809617$5688D18A-7A4C-43FC-B2E6-69C17A520304","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dce248baa6ddc45c558e1072a9ef8778d9930096","datavalue":{"value":"planning","type":"string"},"datatype":"string"},"type":"statement","id":"Q809617$D2468EE4-A434-4DD8-BCD7-FC540BB45EDC","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"3df0a4164685611697fae44bb675079bed3b8af6","datavalue":{"value":"Q56840274","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q809617$735CCF3A-1C2E-4A8A-AD49-BF6BA0F54AEA","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":"Q809617$0D18ACB5-9EBF-407B-84AC-7010FBA79965","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a49c6eab3f20625da110b159712fcc58d765d3c6","datavalue":{"value":{"entity-type":"item","numeric-id":31454,"id":"Q31454"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q809617$C702403F-C63C-4922-A13D-B30C55028BEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q809617$75B16E3F-B6C3-448F-A307-13FB4663DD7D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f10e7acb77aa2a053602f0044c4781346f0cbb55","datavalue":{"value":{"entity-type":"item","numeric-id":31444,"id":"Q31444"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q809617$0898DD3A-EAE3-456C-8EE6-5E8B9171F612","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":"Q809617$C19CF7CF-FCDE-43CB-998A-28E650EE8522","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"22a238ed6c54d87ec163b1a7cb181d6ef07206ba","datavalue":{"value":{"entity-type":"item","numeric-id":3804239,"id":"Q3804239"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q809617$C4A56E19-0466-4E76-A270-5787C2B78C0E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"88277b83497270dd7264f4c05874238f4bd557fb","datavalue":{"value":{"entity-type":"item","numeric-id":3490990,"id":"Q3490990"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q809617$C517B67B-EB2F-4F94-9DBC-2D4E0AC1BB04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5c5ae7e408b1d1201c271e00762d47096e39a012","datavalue":{"value":{"entity-type":"item","numeric-id":4111080,"id":"Q4111080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q809617$78C0EF98-A751-40EC-926D-D428660318CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d4205d0bf2b6063afa1cb652147b728e8c74a143","datavalue":{"value":{"entity-type":"item","numeric-id":3490995,"id":"Q3490995"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q809617$0C5C998D-DE55-4A32-820F-4369842B07F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6cc8abb92210655a5bd4143cbbadd6eadb52d635","datavalue":{"value":{"entity-type":"item","numeric-id":1801222,"id":"Q1801222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q809617$AD48347C-62E3-4D99-B9B6-59A4250FF011","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f720b9345321c44bb6d8cc0a16e6c705607f8508","datavalue":{"value":{"entity-type":"item","numeric-id":3783512,"id":"Q3783512"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q809617$EDF4F671-A04D-4F21-BA3B-9EDF166CC599","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"11fee3290184e0240c1fcdc78a5c0bf709606b2b","datavalue":{"value":{"entity-type":"item","numeric-id":1846747,"id":"Q1846747"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q809617$5B8F648F-6EDB-4587-9F00-B82FA4229A70","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"0c91a47892b27a1e195b7bb92713b5be4ec66a6d","datavalue":{"value":"https://doi.org/10.1007/bf00249016","type":"string"},"datatype":"url"},"type":"statement","id":"Q809617$41E1E743-22B5-435E-84FD-F086ABA3FA6F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"aa21fd2367411b0dc4ce07a5384ac4990851e2ec","datavalue":{"value":"W2034500240","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q809617$C9D009F1-2F7D-400F-86E3-6F37A7709757","rank":"normal"}],"P1635":[{"mainsnak":{"snaktype":"value","property":"P1635","hash":"c9a6e1347df787b6b847161ac5b3b66111e13fe8","datavalue":{"value":"journals/jar/BundyHHS91","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q809617$B54F6561-6578-4F7F-B6E5-E9A13EB5D845","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"19e5279983c8bdbae2df9b45319add3e13808ff9","datavalue":{"value":{"entity-type":"item","numeric-id":3804239,"id":"Q3804239"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a8fe324fbbefe7c92e9e963f633a1f66d6b9bd7a","datavalue":{"value":{"amount":"+0.8585702180862427","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q809617$ECC23C46-BCD7-4426-96CA-3CAA52935EAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"294488c3b85e860c2ccc9131090bac481e1175d1","datavalue":{"value":{"entity-type":"item","numeric-id":4428310,"id":"Q4428310"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"32eb759027d33d8890edba0d8083bf43081e4b87","datavalue":{"value":{"amount":"+0.7973027229309082","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q809617$A37A29A9-B209-4F27-B0D9-F57D4D42B33E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4fe360a6e5e30503c21cd5d94de528a82f553af1","datavalue":{"value":{"entity-type":"item","numeric-id":4530469,"id":"Q4530469"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"32eb759027d33d8890edba0d8083bf43081e4b87","datavalue":{"value":{"amount":"+0.7973027229309082","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q809617$39A6E35A-849F-4410-A21D-3DAB8AD51905","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b70983583bd7e5ea71011477dc85b183843e87af","datavalue":{"value":{"entity-type":"item","numeric-id":5464716,"id":"Q5464716"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"38b06ec4390b663771158e34f05fb74587a49b03","datavalue":{"value":{"amount":"+0.794641375541687","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q809617$FBF05E7E-C083-490F-A79C-94786B7C5B4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"12cfc954b1c18a434b6dbd57c8847a33d308f96b","datavalue":{"value":{"entity-type":"item","numeric-id":2389631,"id":"Q2389631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c645702ca9e11673e54bf74d5511ac6c4e3813ca","datavalue":{"value":{"amount":"+0.79393070936203","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q809617$14C4DA6D-7471-4774-B207-EC39F9846800","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Experiments with proof plans for induction","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Experiments_with_proof_plans_for_induction"}}}}}