{"entities":{"Q287358":{"pageid":289125,"ns":120,"title":"Item:Q287358","lastrevid":60714714,"modified":"2026-04-10T18:41:20Z","type":"item","id":"Q287358","labels":{"en":{"language":"en","value":"On definitions of constants and types in HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6585632"}},"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":"Q287358$6F4CD699-41B9-47CE-8514-8A7E655D0A05","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"daf535f45cf9c5418c5d912456804da84981e101","datavalue":{"value":{"text":"On definitions of constants and types in HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q287358$89990932-35A4-4488-BE71-5C5A8611D490","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"675f7e8f3f9c056644d321f11c3c52091c2533a5","datavalue":{"value":"1356.68173","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287358$05403D5F-F375-432D-8148-CBEEB82889C0","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a0326155ee2776709b948d74abcb135838e086e1","datavalue":{"value":{"entity-type":"item","numeric-id":287357,"id":"Q287357"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287358$D9537BB3-32BC-4B54-A1F9-D90496507E27","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":"Q287358$B172F29E-13B6-476C-9C01-7D189D2C7E0E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b626bb78b3e93b3076e6958296f7f25e2e74c3ab","datavalue":{"value":{"time":"+2016-05-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q287358$2F7A5926-5FCD-44BF-9392-C43C649E3E5E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287358$E4284639-4FDB-4B42-8445-DAE257BF7FF8","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d85f733b3065acb6c0fe2daee7c9692f5318e2ec","datavalue":{"value":"6585632","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287358$EBFCACB6-0956-4E17-8CC0-CB11FE0035D7","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q287358$D560848A-5B9A-4DF1-83BB-2582F6DE809A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q287358$9C854620-0888-437A-A1A7-1C6A6532B9B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"86883f625eb9ea1d0f9d5e4e00110dbc1e213e44","datavalue":{"value":"conservative extension","type":"string"},"datatype":"string"},"type":"statement","id":"Q287358$FFBD0257-5D14-484B-8950-727005032F84","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"45a5c1b9649094350fee1338ad2df123e34ab03b","datavalue":{"value":"Q59476343","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287358$E3241922-E930-4B3D-87C4-B71D593D2671","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"da46e63319fb6c951253404cb70a44966cec8883","datavalue":{"value":{"entity-type":"item","numeric-id":22253,"id":"Q22253"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287358$2671418D-E199-45FB-9885-3183FAAFA8F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5dbdd618fcd9894cc43913fda0ef46a6ceb0f2e1","datavalue":{"value":{"entity-type":"item","numeric-id":5798021,"id":"Q5798021"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287358$47006B4E-B553-4AEA-B283-CEC7EFE590BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0f77c0a86943e8d93be63fc22f23daf955241422","datavalue":{"value":{"entity-type":"item","numeric-id":2879274,"id":"Q2879274"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287358$D50A73EE-144B-4C7E-B67A-D586D5A767B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"283b457c1aa928df8cba388628638010a8a9e043","datavalue":{"value":{"entity-type":"item","numeric-id":4016540,"id":"Q4016540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287358$89CBDB65-9ED3-421A-8A21-2C42BBCAB83F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"045ab0aeb38b209f13b6f5a37c1d619046f27d51","datavalue":{"value":{"entity-type":"item","numeric-id":4078028,"id":"Q4078028"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287358$A76A2116-DBC8-448A-BEEB-EA021B6FC6DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aeedc506ee95714a79cfc16f82862182df8774bc","datavalue":{"value":{"entity-type":"item","numeric-id":3613408,"id":"Q3613408"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287358$B0790A5A-6E03-4E23-B79C-8987F47C22B8","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":"Q287358$90C8B238-A0E2-4163-B2B6-9C83D6F071ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dc149579e2c0f9cf6c6f1a082b600b053a6569c3","datavalue":{"value":{"entity-type":"item","numeric-id":3183533,"id":"Q3183533"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287358$5BF6C11C-7C3D-4961-90CF-1C37780CAF79","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ca6926d9a2864657c63c8ba6d81f03198b036942","datavalue":{"value":{"entity-type":"item","numeric-id":1595929,"id":"Q1595929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287358$1EC51526-8EE1-4768-89B0-03BC9D5D59CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5bbf3fd853a4036d3cac2ccc1f0a3b4a11edb981","datavalue":{"value":{"entity-type":"item","numeric-id":2248021,"id":"Q2248021"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287358$7BE6742E-F686-46E0-9916-D47176DB63BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"999b14224255809098a606c16262602638de58e6","datavalue":{"value":{"entity-type":"item","numeric-id":2879260,"id":"Q2879260"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287358$DF0314DA-3DED-400C-BD8D-21EAE3629144","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ba312c695aa52705a7646f3d7672bc8e08dee39c","datavalue":{"value":{"entity-type":"item","numeric-id":5219926,"id":"Q5219926"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287358$EA23A2D9-CB37-4771-9475-5FD705D315E6","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":"Q287358$C93A0BA6-9385-4812-B67A-9E5FC225A7CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7a2c73ea523922ddf10917d5a60c3c9e9df84e94","datavalue":{"value":{"entity-type":"item","numeric-id":3995087,"id":"Q3995087"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287358$7FF1FDAD-D21D-4273-9C2C-900DAC6082D5","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"56183f18c1b7292025f517695163436751950f86","datavalue":{"value":{"entity-type":"item","numeric-id":22253,"id":"Q22253"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287358$D77ECC76-6695-44CC-B2E2-24DC7A1E88E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8b2040a476017b43b21bd352cfec0a67d631d6d4","datavalue":{"value":{"entity-type":"item","numeric-id":18467,"id":"Q18467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287358$FF2A5072-E8C0-4631-BE04-6F9FF3EDBB38","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":"Q287358$83C63929-D580-4C3C-B434-43E4EEDFB4CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"468fad61234030d4d4bd64e4991e6e30fb2af1d0","datavalue":{"value":{"entity-type":"item","numeric-id":29451,"id":"Q29451"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287358$3A475F01-3A1A-45A8-80AA-E06589399EDD","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":"Q287358$F5D6E988-4BC3-420E-A2FE-96F3EB82B487","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":"Q287358$EF1A37FB-121D-4361-ADFB-EF0B7D584009","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bcaf3b20cd7fd897f2f47a708bad9d4f554cb6fa","datavalue":{"value":{"entity-type":"item","numeric-id":14553,"id":"Q14553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287358$41A64E8A-2977-4B86-A746-7071A8B14A73","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b222922e2b373ab7fb2b7a049f9de07c755ee255","datavalue":{"value":{"entity-type":"item","numeric-id":16770,"id":"Q16770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287358$046595BF-4031-4129-AD93-0F512CCE4EA7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ad35e1f036cc1a37637a9bb57b386a55e86e9fd2","datavalue":{"value":{"entity-type":"item","numeric-id":18673,"id":"Q18673"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287358$341EA5A0-5FBB-441F-884C-E1133DCADF5C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"801a319db4682ef4442b12d14dec7cb54b5357be","datavalue":{"value":{"entity-type":"item","numeric-id":44336,"id":"Q44336"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287358$12BEB078-8EF8-41E5-B493-5404586B5139","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":"Q287358$98327AB0-B894-4D3F-AA4B-428530C48455","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"30013ba2822857df41f8ee803071fd3b99b24673","datavalue":{"value":"https://doi.org/10.1007/s10817-016-9366-4","type":"string"},"datatype":"url"},"type":"statement","id":"Q287358$4F6CB9CC-21CE-4623-89A3-B8440BCB0095","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"667502653f468a790bbcb65dea68c2ac40a76352","datavalue":{"value":"W2294931363","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287358$CF52C424-70B7-446A-B6B1-6B41E0B33EC1","rank":"normal"}],"P1635":[{"mainsnak":{"snaktype":"value","property":"P1635","hash":"4a73b66e392c9395da8c183f5c688a8636cf5b03","datavalue":{"value":"journals/jar/Arthan16","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287358$6762030D-F28E-4672-8C62-8735CD0D3122","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"18299bd99b685392c470d82978307fbcf07fa40c","datavalue":{"value":"10.1007/S10817-016-9366-4","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287358$5D56F4FC-9D27-46B8-8343-E2C29FE822D5","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"33d9d91864fd36c9cf69a0a0271de5d035ba5751","datavalue":{"value":{"entity-type":"item","numeric-id":2879260,"id":"Q2879260"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"18ccf5e11a48a9be3f5729ec80b9b4ae2a32b893","datavalue":{"value":{"amount":"+0.7811332941055298","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":"Q287358$1A0F570C-8520-4230-9DA7-34DDD82EFDD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f007afffaa9d82c697dfde08e38474d46ab399f3","datavalue":{"value":{"entity-type":"item","numeric-id":1739913,"id":"Q1739913"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0926e30a1347a4a1dd3659b730a0ba6a41bb8172","datavalue":{"value":{"amount":"+0.7774130702018738","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":"Q287358$D2EE00DE-8869-421F-9F22-B850D04542E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"19914ff8362a88c613e25c3bea458e1c7b08dd0c","datavalue":{"value":{"entity-type":"item","numeric-id":2945636,"id":"Q2945636"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"76f1178b440149a25f2ecdbfd1c6a0c80802c202","datavalue":{"value":{"amount":"+0.7744643688201904","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":"Q287358$373DAE6C-FBF4-443F-AEF2-7A6E55E5241F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"08a4d9babdd0dc4f3d4a84fe7e41ccc98bd845de","datavalue":{"value":{"entity-type":"item","numeric-id":4964711,"id":"Q4964711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c386aff9f9974048454f0a104cb634ef82a54871","datavalue":{"value":{"amount":"+0.7506594061851501","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":"Q287358$1A2D23C7-4054-43A8-94B8-B07DA6AFE02C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f2ad198c7057067a7e23ab0fd94490a08ee71ecc","datavalue":{"value":{"entity-type":"item","numeric-id":3024873,"id":"Q3024873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9ba70f6dc4a8ad742e24a02c5500d43d5a56abd6","datavalue":{"value":{"amount":"+0.7394339442253113","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":"Q287358$5E227B1F-DA79-4503-B3E3-7FDAE8983C56","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287358$D77B1E19-0C1E-4339-AE5A-460E952F6EC8","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"On definitions of constants and types in HOL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/On_definitions_of_constants_and_types_in_HOL"}}}}}