{"entities":{"Q2871875":{"pageid":2882595,"ns":120,"title":"Item:Q2871875","lastrevid":51900746,"modified":"2026-01-20T12:22:03Z","type":"item","id":"Q2871875","labels":{"en":{"language":"en","value":"Two-level hybrid: a system for reasoning using higher-order abstract syntax"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6244448"}},"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":"Q2871875$592D2B79-D68F-4483-9CC7-90F1D47282BC","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"466b668b23b70f8920544455389bb93c658cb31e","datavalue":{"value":"1278.03062","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871875$65C66DAC-0A90-43AF-88EA-4976C62E9940","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8135914452c3b1bd839ce74f3161ea4765c65f58","datavalue":{"value":{"entity-type":"item","numeric-id":287276,"id":"Q287276"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871875$7DA82AA0-209D-4510-8EB6-FE1C6C5E9D6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"0b915c5b45e1342b9fb2d86d7d4ef63560f48d76","datavalue":{"value":{"entity-type":"item","numeric-id":2871874,"id":"Q2871874"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871875$828F62AC-4FD4-40B2-A36A-39C79CAA11A4","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":"Q2871875$9AF40F50-CA1C-4675-AADA-963067247E76","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2c704b287c68a3d4d8361a025642d6eba13574eb","datavalue":{"value":{"time":"+2014-01-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2871875$B2A33902-7845-42B7-B46B-50C89B504863","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5445447bcee9c6fd248a24455b47f3ae211c866d","datavalue":{"value":"http://www.sciencedirect.com/science/article/pii/S157106610800039X?np=y","type":"string"},"datatype":"url"},"type":"statement","id":"Q2871875$2775F1FD-032D-40D2-AD5B-4E595FB25FAE","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871875$7EF48C5B-DD35-44D5-8263-2E32997B9486","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871875$325658AB-61E0-4D79-9144-D5CE4C7CED1F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"45a9c82d40c5673b67006186b7c75491cbabafbf","datavalue":{"value":"6244448","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871875$BA59E3F3-A3CF-40BE-9C12-A102BD589C97","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8026960d6f36428821b4502bc1641829b1806e7e","datavalue":{"value":"higher-order abstract syntax","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871875$38CEDF25-C105-41AF-9907-5BF8568B505E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871875$1174F68B-47DB-4284-B00D-901DB3F6C56F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fa8a6101ff90bea77f851517b5a991ddcaf7286b","datavalue":{"value":"induction","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871875$EAFF3FAE-58FB-48B7-99B1-3B56C86150D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"017465942dbd8ba7ebab45a45af0183e273a4234","datavalue":{"value":"variable binding","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871875$4D6D2E5F-432C-4D74-8EEE-1FC3656DDE2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"42f0513e500ea6cb630e73925875c7d53ca8d8e1","datavalue":{"value":"Isabelle/HOL","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871875$7A4795B4-EFF3-42A1-80EA-E67973A9561B","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":"Q2871875$421068F9-09D9-4DDD-8220-41AEEF222445","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871875$40143576-4627-493D-A3FF-1ECD9528CF4C","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":"Q2871875$DB12FE09-4C86-4852-A13A-7EF6489336E4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"333e47a034532880dbaa1fdb35187ef5232cf98f","datavalue":{"value":{"text":"Two-level hybrid: a system for reasoning using higher-order abstract syntax","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2871875$D042DD34-51D3-493D-AB8A-8366FEB32B51","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b47167d4bb944e79729d3ca171d41ed04cd2ec74","datavalue":{"value":{"entity-type":"item","numeric-id":438569,"id":"Q438569"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2f2d079fa75281a7aa998883e84b15dd3b6c196b","datavalue":{"value":{"amount":"+0.8934919238090515","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":"Q2871875$B3AFE2BE-837E-4D53-9761-1E781D8C82AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"66668ed7158b07726d83fc60cbfbe89a17acc37b","datavalue":{"value":{"entity-type":"item","numeric-id":5747652,"id":"Q5747652"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dc6147cd394996bd0e511796fc7bd67bde9b9f11","datavalue":{"value":{"amount":"+0.8537464737892151","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":"Q2871875$FA8426A6-CACA-419A-8612-6CEA7AC4B003","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dacbd805b7b44902c13309d5bd3b30627095ad8d","datavalue":{"value":{"entity-type":"item","numeric-id":5738952,"id":"Q5738952"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ab6f2a7286af2c8cdcc3a278366bb3087dc60052","datavalue":{"value":{"amount":"+0.8340913653373718","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":"Q2871875$F95BC1E9-6B32-4AAF-821F-B9F8E843DFC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0b2a6ec1f489d756f6b308bccbd87a5b30a3aae9","datavalue":{"value":{"entity-type":"item","numeric-id":4484329,"id":"Q4484329"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1aa7614e4e5303bac6e77a07beb8c4ef96c28097","datavalue":{"value":{"amount":"+0.8281303644180298","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":"Q2871875$686A2C2E-BF6C-48A9-A552-D4E17058F257","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2d49e8faf4fe3121fa0f30303597bc67bfb868ac","datavalue":{"value":{"entity-type":"item","numeric-id":4484341,"id":"Q4484341"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"28a5649221a8c7c0008b17fd18f127c4c240d177","datavalue":{"value":{"amount":"+0.8215993642807007","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":"Q2871875$D09824E3-90CD-4B76-8A49-B5C3620E9725","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2871875","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2871875"}}}}}