{"entities":{"Q4819003":{"pageid":6848583,"ns":120,"title":"Item:Q4819003","lastrevid":74719908,"modified":"2026-04-15T00:01:55Z","type":"item","id":"Q4819003","labels":{"en":{"language":"en","value":"Polymorphic lemmas and definitions in $\\lambda$Prolog and Twelf"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 2102945"}},"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":"Q4819003$A05F3A4B-10C4-427A-B065-A9D5541F317D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0a53c2231314fe4f0b879e048226f6475e2d3292","datavalue":{"value":{"text":"Polymorphic lemmas and definitions in $\\lambda$Prolog and Twelf","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4819003$78025D76-E395-405C-B90C-BD5FE4054C8E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"563a5ee09b2a9a236cccd08268ece46336b76a94","datavalue":{"value":"1085.68015","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4819003$DC500CFD-B0BC-47A2-887E-C6132464BFA4","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"2ca44e9be32bef20429261b3711fb389f8e2e344","datavalue":{"value":"10.1017/S1471068403001698","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4819003$8CD07F0D-13CA-4F32-AF36-8812A8C2C1E0","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"fc26ae99955b17096664472ad434caf6f770734f","datavalue":{"value":{"entity-type":"item","numeric-id":1663237,"id":"Q1663237"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4819003$FDBEA5C6-77C2-477F-89CA-AEA2C2EB76AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c3098c31aaa054039cc5414efb85f4a6bce38102","datavalue":{"value":{"entity-type":"item","numeric-id":590551,"id":"Q590551"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4819003$81C73D96-4A39-4F8A-9D59-309CEAC840BF","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"36bb0dcc3009bb4f4979cdb33a56e0ede194fc63","datavalue":{"value":{"entity-type":"item","numeric-id":2845119,"id":"Q2845119"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4819003$77D68866-02B2-4F1F-9BB6-FAC4CFE9C004","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"80836874fe663944c89061f0420200b4dad391b3","datavalue":{"value":{"time":"+2004-09-24T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4819003$A2A76990-B8B4-491A-9ED7-0634FE1826C2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"b492f281b8f52c724f2bc547e7e570cccf4bd5e0","datavalue":{"value":"68N17","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4819003$52BD2CEA-DD00-4903-B7ED-5638781513ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4819003$B1A851C6-3971-4CF0-A2FA-373E57C5F365","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6d5182b328e8196c4b76175888f30b0e4e4f0185","datavalue":{"value":"2102945","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4819003$90CACBEA-A8B4-450F-9F20-C354C9FC76AE","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q4819003$027436F1-4347-4ABE-914A-9CC902AA84AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"edc71abbb0eb29d287fae2ef615d24c8d5b85163","datavalue":{"value":"higher-order logic programming","type":"string"},"datatype":"string"},"type":"statement","id":"Q4819003$315138A3-70DF-47A1-B50D-9AF41DE4F31D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66040eec798fa7d182443c16b59531175d83cf5e","datavalue":{"value":"logical frameworks","type":"string"},"datatype":"string"},"type":"statement","id":"Q4819003$E40FA254-3D18-4385-BB13-9EF10E298FE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c47bd69800ec9a3c8fdb3c483630a46ac282cb0d","datavalue":{"value":"polymorphism","type":"string"},"datatype":"string"},"type":"statement","id":"Q4819003$29F041C3-59E3-4413-AE2C-88D4F7742DAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b90ba581de713a3df5c41b7c4f044c0002164b31","datavalue":{"value":"proof-carrying code","type":"string"},"datatype":"string"},"type":"statement","id":"Q4819003$00690230-5187-44A3-A1A8-B7F1F9F191C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"78ec50a529530cc24a5b60862a36f6f703ab2c20","datavalue":{"value":"Lambda Prolog","type":"string"},"datatype":"string"},"type":"statement","id":"Q4819003$9193FBD8-BBA9-492D-9FA2-90F53A9286D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8a7faf2d5c8d76731eb2c0fa9732494500b1c909","datavalue":{"value":"Twelf","type":"string"},"datatype":"string"},"type":"statement","id":"Q4819003$A6977F3A-A8FE-4590-8A29-82CF3A50628C","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":"Q4819003$57CC704B-895E-40CC-9F28-2470F6D2D003","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"f5583adf25a95b72293e889fb441a264ee013fba","datavalue":{"value":"Q124841043","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4819003$45BB98EF-9BEA-4AE9-A7DE-5D09F2563666","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ed2a8b95a2e9f2d2392d01b0ba9729d077ebd785","datavalue":{"value":"https://doi.org/10.1017/s1471068403001698","type":"string"},"datatype":"url"},"type":"statement","id":"Q4819003$D061A581-E4C3-48AF-A414-A394BD09FBA1","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"c4ab2629c0e366cd8af7ef26f0f1fcfc8e703dd0","datavalue":{"value":"W1980229219","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4819003$9D2A26BE-44AA-4EEF-AB2A-DF223294B0C6","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"44ec43f150e0dbc8e2356d4a810ffb760b54eafc","datavalue":{"value":{"entity-type":"item","numeric-id":6488533,"id":"Q6488533"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a505bdd00d468b1214884e886a33d2d6bd6cef23","datavalue":{"value":{"amount":"+0.7864130735397339","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":"Q4819003$CF5FE967-38E5-41A0-B5D5-7CC0603214ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b5eaef786744ca6e888c6b7ce9c19c81d510cdb0","datavalue":{"value":{"entity-type":"item","numeric-id":2763626,"id":"Q2763626"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2be3ea3fceb6c071623491a1af4b846decdac5a3","datavalue":{"value":{"amount":"+0.7746979594230652","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":"Q4819003$AE5F103C-0ED6-4F72-A23B-1C194C862C70","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4f9d59bdc6ae437ece8127a1d514a0d68e56907a","datavalue":{"value":{"entity-type":"item","numeric-id":3491030,"id":"Q3491030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"39141e09bca9faf1b4ea0bf7b71a52b08de5b637","datavalue":{"value":{"amount":"+0.7708944082260132","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":"Q4819003$88957FEE-3923-4CC9-AFF3-7851A87F1511","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b75590232e3192300cf7d05455774af1c6a88083","datavalue":{"value":{"entity-type":"item","numeric-id":3523179,"id":"Q3523179"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4b2433ad82aa68857c97016777d0d0d4c2c1b344","datavalue":{"value":{"amount":"+0.7450043559074402","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":"Q4819003$63284CE9-6770-4AA0-B429-94A106676927","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f3ef072fb71a8f1cd37ad6a71751c23ae314c430","datavalue":{"value":{"entity-type":"item","numeric-id":4249901,"id":"Q4249901"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ca71e1a42aca98cee4d53b0cf9cdd64a4652c949","datavalue":{"value":{"amount":"+0.7409844398498535","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":"Q4819003$FFD227A2-8491-482B-A3A0-F3061E058CD7","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Polymorphic lemmas and definitions in $\\lambda$Prolog and Twelf","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Polymorphic_lemmas_and_definitions_in_$%5Clambda$Prolog_and_Twelf"}}}}}