{"entities":{"Q2423767":{"pageid":2434510,"ns":120,"title":"Item:Q2423767","lastrevid":74198118,"modified":"2026-04-14T18:54:49Z","type":"item","id":"Q2423767","labels":{"en":{"language":"en","value":"Formalization of functional variation in HOL Light"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7069248"}},"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":"Q2423767$5701C369-9CA4-4C7D-AB36-CE04277B1358","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"fc1d3d44482f0dbfc4daa78712f66aca8b845a2d","datavalue":{"value":{"text":"Formalization of functional variation in HOL Light","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2423767$4259ED60-3A16-477A-9402-3B170CA4AC68","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"972a69a2a7d6425bb26c055d30b15ab7af6d7631","datavalue":{"value":"1423.68427","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2423767$21AAA91C-2DCF-43EB-9C49-A2529B56A588","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e66e50d381800d17b26cd1baab7968215c6122c2","datavalue":{"value":{"entity-type":"item","numeric-id":2031405,"id":"Q2031405"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2423767$6B078AEB-7F5F-4BD2-AFC5-19B3889D24C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3d718f2f7e46bc75441b1903120d3afa836e7b32","datavalue":{"value":{"entity-type":"item","numeric-id":1956042,"id":"Q1956042"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2423767$D526A87F-44F1-4C06-86F8-E26939074EEA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"fb41e43426ff3ff3f8a93f102f45b1fd00efc7eb","datavalue":{"value":{"entity-type":"item","numeric-id":826357,"id":"Q826357"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2423767$9AA61680-E656-4662-9AA3-F3589A60F569","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bad697f6be27ac07cc0bac5f2074dc40ed884baf","datavalue":{"value":{"entity-type":"item","numeric-id":258539,"id":"Q258539"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2423767$AE8014E3-C44E-4022-83D9-7F331F7B8CFF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"fca25263e9f5aaf26ec4c35ce7597172123f183c","datavalue":{"value":{"entity-type":"item","numeric-id":298821,"id":"Q298821"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2423767$12CA109D-C713-4B03-B810-9B27AAA930B1","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"2532b82fbfd494721e144e8b872f80867d7316e9","datavalue":{"value":{"entity-type":"item","numeric-id":246441,"id":"Q246441"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2423767$6E41D18F-44DD-434D-9749-0CE176C709DA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"42d1f5c0f5e8db34a69e71d479f8d7faaf3c37a6","datavalue":{"value":{"time":"+2019-06-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":"Q2423767$4336B8FD-E6AC-416C-9471-E13C01DD6025","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2423767$1EDF9A67-3C74-4A6D-A3F0-55F67E93B9DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e878bf69634dde290ca1a436388e1109fae71408","datavalue":{"value":"49K27","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2423767$B44180A3-C7C6-408E-876B-388717632226","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a8f164cbd438e8dd4249bc0bb406573fec20a47d","datavalue":{"value":"7069248","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2423767$FFD2DBF6-C72F-4739-A922-AFA34A71F8D7","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ab63512fdbd6c307b5aa191311d8d9533d09503d","datavalue":{"value":"functional variation","type":"string"},"datatype":"string"},"type":"statement","id":"Q2423767$8BD3398A-136D-4764-8C40-81127688E5D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3f77828a999bc8c675695ac154d25c13bb4e2b70","datavalue":{"value":"Fr\u00e9chet derivative","type":"string"},"datatype":"string"},"type":"statement","id":"Q2423767$682420E4-1519-4831-9E1C-28A11ACCDD27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5e51fee68a701f8b81834c2df76ea4b753fa94f5","datavalue":{"value":"continuous function space","type":"string"},"datatype":"string"},"type":"statement","id":"Q2423767$DBFF2CAC-E5AA-460F-9BDE-28872941AE96","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2423767$60BF91C5-B651-4903-AB83-C2F271609DFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9f5004e76eed31b1e2520bfbf1b797adc35e1b8e","datavalue":{"value":"HOL light","type":"string"},"datatype":"string"},"type":"statement","id":"Q2423767$1E34F7E5-2EC7-44EE-8C77-DE53D50AD0C2","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2423767$2D64CEF7-89B1-400F-8142-019AC8244C78","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":"Q2423767$018BA1B3-18D9-411D-8431-4ABD23935166","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ee80fa482e8c030191fc3263e069d0dc0cdf7815","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2423767$347EF969-C11B-4887-A57B-4EFE8888145A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"872fd15c13425cde672f9d01c85cc24654e9455d","datavalue":{"value":{"entity-type":"item","numeric-id":40272,"id":"Q40272"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2423767$D5A63827-927E-42D5-AFAD-2BA3CCF8115D","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":"Q2423767$6AD83D3B-D9F0-44E8-9B79-72FC7CAFE92F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"472e3341927a1d03435e322d18019adec6836b0f","datavalue":{"value":"https://doi.org/10.1016/j.jlamp.2019.04.004","type":"string"},"datatype":"url"},"type":"statement","id":"Q2423767$73733ADD-F7F1-41C5-B1FF-FD31BCD715ED","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"24ffc00fc09c102d95ca0d9ba06ad426595fca5b","datavalue":{"value":"W2940065749","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2423767$C01504FF-209B-4A22-A363-587A476DFCA9","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"3b5045e17431ae100adc29ee6860720ac72d87fa","datavalue":{"value":{"entity-type":"item","numeric-id":5302561,"id":"Q5302561"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2423767$CCA3A5B2-9FDD-4809-B333-9ADE19BCDC24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"17a69741364102658aa60a87b94db8d7506ce725","datavalue":{"value":{"entity-type":"item","numeric-id":3183517,"id":"Q3183517"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2423767$0A30A9F7-7C4F-4FC3-A1C1-D60BA1814151","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77f4334b25d43b9293350a877e2d317280ca55a9","datavalue":{"value":{"entity-type":"item","numeric-id":3543646,"id":"Q3543646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2423767$B34433C9-161D-4AEE-BDEC-34B3686F8529","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9b06809062082b8f9f5dbc080e3987837376fa3d","datavalue":{"value":{"entity-type":"item","numeric-id":3499750,"id":"Q3499750"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2423767$D331B6CF-0A44-461B-BD03-7492FB5A6564","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"12c8a3564e858c76081a725f4bc7b45ddc58f100","datavalue":{"value":{"entity-type":"item","numeric-id":2360828,"id":"Q2360828"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2423767$71877159-213D-44D4-A98F-5D5862475994","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"52ae0373da0365d3cbebb0eb58e31edfe536299a","datavalue":{"value":{"entity-type":"item","numeric-id":1666338,"id":"Q1666338"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2423767$9B55460F-9E8D-47FE-AFBC-8EC5621851DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc90f519741959885c97856c7164fc497d5566b1","datavalue":{"value":{"entity-type":"item","numeric-id":2973239,"id":"Q2973239"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2423767$7C763875-43EE-4BD3-AAE6-B1929FD28DAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e4b498ee6e6da5028f261924fcf793055d69f3ad","datavalue":{"value":{"entity-type":"item","numeric-id":333325,"id":"Q333325"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2423767$0572E2E5-FB33-49C6-A4DC-DD2AA5B1C5FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3b819f2c80f9e04e31e7f8a5919a6260d006131e","datavalue":{"value":{"entity-type":"item","numeric-id":2294128,"id":"Q2294128"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2423767$6FEF38EE-2F32-4986-BE6A-46D894B3313C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b0ef84619234e2e46e8c4513d6d1ef3cba6f5b65","datavalue":{"value":{"entity-type":"item","numeric-id":1945903,"id":"Q1945903"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2423767$C588F2CA-FF2F-4648-B640-AE5EBDD7500C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84ae1bad2fa7d150795b80eddc204103d5933133","datavalue":{"value":{"entity-type":"item","numeric-id":2766799,"id":"Q2766799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2423767$95E70418-30B4-41B1-97BF-10650E1FB6CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3d49eb451a0aa7cf50ddefb651ea8beb466724dd","datavalue":{"value":{"entity-type":"item","numeric-id":2879271,"id":"Q2879271"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2423767$5EFBA0C0-C42D-4B4E-85AD-AD1468A5D7E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a80628d93ffe3b4f4fdfe3e3ce938e4b4721d341","datavalue":{"value":{"entity-type":"item","numeric-id":5332396,"id":"Q5332396"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2423767$CBD8CCC3-AD6F-4D02-9377-DEB0C04A2AB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"64ac3997363ba4713c6a121bce0d63fc786f5e43","datavalue":{"value":{"entity-type":"item","numeric-id":4230801,"id":"Q4230801"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2423767$DF7CFE06-485F-4655-8936-66AB81B024EE","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"2f111155b4fdf74fec4efe566fe6a64136baf872","datavalue":{"value":"10.1016/J.JLAMP.2019.04.004","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2423767$904E211F-B44A-461D-AD9A-C6B3A039BF0C","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b5e8f8950192242021036f7a946566d5cbb1d1a6","datavalue":{"value":{"entity-type":"item","numeric-id":2294128,"id":"Q2294128"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"61210bed8baea4593b85d7fbc8a10c586290fbda","datavalue":{"value":{"amount":"+0.7915967702865601","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":"Q2423767$6FC68F7D-80C3-45A0-948B-776DB5082C42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"40a358107e0aa52d0d1913166ea142904824186e","datavalue":{"value":{"entity-type":"item","numeric-id":2364690,"id":"Q2364690"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"78a05f7d4aa59c11232b06fca67d37f03e490b2f","datavalue":{"value":{"amount":"+0.751261830329895","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":"Q2423767$82586C79-F3C4-42D8-AFF9-8F7FD9C7342A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"436458a6c9fbc133317520106194cab8d362cf2c","datavalue":{"value":{"entity-type":"item","numeric-id":2323452,"id":"Q2323452"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f872acc876e29e5ddaa8ffb43a717637a1b5c92a","datavalue":{"value":{"amount":"+0.7201545238494873","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":"Q2423767$08A00AD3-3E42-445E-80A9-10FE4B2D3CD4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"38e974a1c65932c531eadf63f649a23137ae8a55","datavalue":{"value":{"entity-type":"item","numeric-id":3453127,"id":"Q3453127"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cabca380fb7fdfa026429cd9dd24c38d73d189b4","datavalue":{"value":{"amount":"+0.7118859887123108","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":"Q2423767$64FD46E5-D92F-42ED-8226-97DB0F4058F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"895f01dbe4514afaf4e58308193c557e5a7e265f","datavalue":{"value":{"entity-type":"item","numeric-id":2375439,"id":"Q2375439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"431ed32e284dd42bbd0f0fc00f2a06c16fefa745","datavalue":{"value":{"amount":"+0.7101051211357117","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":"Q2423767$1436D350-A1EE-4EB9-8FB0-7E3D821175BE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formalization of functional variation in HOL Light","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Formalization_of_functional_variation_in_HOL_Light"}}}}}