{"entities":{"Q861715":{"pageid":863563,"ns":120,"title":"Item:Q861715","lastrevid":64957734,"modified":"2026-04-11T23:21:31Z","type":"item","id":"Q861715","labels":{"en":{"language":"en","value":"Mathematical induction in Otter-lambda"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5119744"}},"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":"Q861715$C7D46DD3-3187-40B2-91DB-A7475AA3BBFC","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d6b83cc29f33760e31f66b5bb9bb773ef6b60039","datavalue":{"value":{"text":"Mathematical induction in Otter-lambda","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q861715$E00164AE-3AD3-4293-81C8-70C449EF09CD","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"84dd2cf7fd24fd622d4e80bedcce4ef31184006a","datavalue":{"value":"1107.68093","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q861715$4AF84F02-AF84-4864-8102-6AC3EF7A5B1C","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":"Q861715$3D004698-3886-46EB-AB57-0B0A11361C0C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"35bf8729f5a833a26eee340dee2bdc3e7c14d114","datavalue":{"value":{"time":"+2007-01-30T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q861715$363EE2E9-E6A7-471D-93A3-19DE5A78E764","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q861715$A44CCBD0-BAF7-4E73-9198-8EF408776A09","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d217c9d330dda397d00551d3d960213fca11fc3a","datavalue":{"value":"5119744","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q861715$478FB7C4-17A9-41B6-8689-4C9EB12B230A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"600bd15b3215cbdd5d1fc962488ac0a8a1a6bc21","datavalue":{"value":"first-order prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q861715$1848F4F5-4228-4536-B029-7EF452B0CD66","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a20a062630d1bb5cf9aa5d669cd08fbd3eee7671","datavalue":{"value":"automated deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q861715$90B4A886-1107-4552-B17F-4C6B454AA68E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a1c8eddecc5ce394430330a44a53dc94ae4fe184","datavalue":{"value":"computer proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q861715$65B18A2A-5BE1-4AC2-8175-B265A94AC4C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c3922eb0b8235fb2b824bcb3eaa0c8d395dbd512","datavalue":{"value":"unification","type":"string"},"datatype":"string"},"type":"statement","id":"Q861715$D4F1CEA8-A374-4767-9C10-A61FF60E1093","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3b97b327acd29bc543e319ce1a45374500e4b98f","datavalue":{"value":"mathematical induction","type":"string"},"datatype":"string"},"type":"statement","id":"Q861715$0B096AB1-9AD4-43E5-A31A-F1C7AA68A6D7","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"bce2cc6380726fb10d79b2328ed8cc6bcf2ac9d3","datavalue":{"value":{"entity-type":"item","numeric-id":1224088,"id":"Q1224088"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q861715$8051D05C-E781-424E-8647-9AC230FF5323","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9c40cf9a35904f638a7cabef2bc178bad46391f7","datavalue":{"value":{"entity-type":"item","numeric-id":13717,"id":"Q13717"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q861715$9D28BE48-664D-4038-8E86-7E3A97AADA7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3956bdfa35577363f46fde3b4b27208e12ab55a8","datavalue":{"value":{"entity-type":"item","numeric-id":20335,"id":"Q20335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q861715$5FD4607E-98D9-4D7B-909E-B7ABF5652D91","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1e7b4d238eeafa5b21b1ef85a0d6b8900bfdc422","datavalue":{"value":{"entity-type":"item","numeric-id":15442,"id":"Q15442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q861715$FA86A01C-1902-450A-A59D-9478073CF4F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2e07b63a7544a6d7c83390f82ddae368b77e124c","datavalue":{"value":{"entity-type":"item","numeric-id":19570,"id":"Q19570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q861715$A9CA1B36-420C-477B-B19C-ABA9E565C5D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3f1ebf2accc5d6c6b3c7a81ee7493fd53a6bf250","datavalue":{"value":{"entity-type":"item","numeric-id":40618,"id":"Q40618"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q861715$E6580C0F-BFB6-4829-AFBB-FCFE80289D87","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":"Q861715$0709BF78-9FEE-4B11-9244-1E6C79FCC312","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"3b6a17663fb19ad47ec8b3ba25674b57cc49e146","datavalue":{"value":"https://doi.org/10.1007/s10817-006-9036-z","type":"string"},"datatype":"url"},"type":"statement","id":"Q861715$5E0A0E5C-6671-43E2-BC1C-B69C0EB02CB1","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b05108de8276187419ae103914d92da0ecf1bd08","datavalue":{"value":"W2033513250","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q861715$16A398E0-D7DE-4411-8F38-D91B24F07BF1","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"fbb5c820fca2abc8b866bacf26774dc3344f359c","datavalue":{"value":"Q115056505","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q861715$3AAD9E90-E4DD-468D-81CA-A7793ED4503F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b3ad0eeac3b2d9aea59d4e0a75de4182d01753ee","datavalue":{"value":{"entity-type":"item","numeric-id":1923825,"id":"Q1923825"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q861715$7E599F27-69AF-458A-AAD3-A14FD49A255F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a28ce065a492e192f300a4c25b3939254c4181ea","datavalue":{"value":{"entity-type":"item","numeric-id":1134540,"id":"Q1134540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q861715$ACC4C747-BCBD-4A5D-B995-25D9070E598C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c0843e7f8e29d84aa6b7b4f9a110eadf9b3b1959","datavalue":{"value":{"entity-type":"item","numeric-id":1134541,"id":"Q1134541"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q861715$82296C61-ADF9-49FC-8DA8-F7B9AC332C1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5a3ed83efa9c31fe937c116368ddc1008d2da01e","datavalue":{"value":{"entity-type":"item","numeric-id":5307080,"id":"Q5307080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q861715$B1464904-4E03-4A9B-8C1A-FBE9A3AABCCF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9f4ec34970699a60fee9b67f04e9456c847a6819","datavalue":{"value":{"entity-type":"item","numeric-id":861715,"id":"Q861715"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q861715$9800206B-D48A-45D4-87D8-1D7953BC4088","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0aad2711eb9c64a58dada485191047b8af29959d","datavalue":{"value":{"entity-type":"item","numeric-id":4040283,"id":"Q4040283"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q861715$4B65D1B9-8FC9-4F8A-9197-5BD46D9CDFE8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"635d658e492778c40a0dc6463613126938b64c17","datavalue":{"value":{"entity-type":"item","numeric-id":2751365,"id":"Q2751365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q861715$AE4F42F7-2092-49F5-A030-4B24608451CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6bfc2f52353af05e515090f56fb57e55f420097d","datavalue":{"value":{"entity-type":"item","numeric-id":1122363,"id":"Q1122363"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q861715$962391FC-6F23-49A1-B800-6ECB79D03709","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8cef60f49122cbdc8855980bc9949c7fcffb3541","datavalue":{"value":{"entity-type":"item","numeric-id":5444850,"id":"Q5444850"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q861715$751844F2-1057-4959-B88D-E809BFEA38B7","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b5487380ebec71b22667375096763216b635d7ab","datavalue":{"value":"10.1007/S10817-006-9036-Z","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q861715$1D9AC96F-D3B7-4D59-8BE5-379ED981D0FD","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"add424b5fb4252367fb8ddba535c3d17f35ed52c","datavalue":{"value":{"entity-type":"item","numeric-id":5575526,"id":"Q5575526"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d8239224e768edf914713982b494ac3d3ee540b3","datavalue":{"value":{"amount":"+0.84445745","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":"Q861715$3B1A31FC-9EA8-40FB-87F4-4B49E7A435BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"39bb720b7c1477bdd9fa3da132be1b604f98822c","datavalue":{"value":{"entity-type":"item","numeric-id":2721238,"id":"Q2721238"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"64271aac7e61c54b3177b55f62c74535324a51e8","datavalue":{"value":{"amount":"+0.84277403","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":"Q861715$09278211-3AFF-48E5-AF13-6F1C56FA4C2A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Mathematical induction in Otter-lambda","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Mathematical_induction_in_Otter-lambda"}}}}}