{"entities":{"Q4559809":{"pageid":6589400,"ns":120,"title":"Item:Q4559809","lastrevid":97325546,"modified":"2026-06-05T13:59:56Z","type":"item","id":"Q4559809","labels":{"en":{"language":"en","value":"Proof-relevant Horn clauses for dependent type inference and term synthesis"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6988657"}},"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":"Q4559809$09651D62-5015-4DB4-8BFF-DACD133EBE0C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"fb01977cd8556ad53c6c79988d28d135b4bb2dfc","datavalue":{"value":{"text":"Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4559809$C00A9F7D-4878-466F-B99D-D385FCCBB2B8","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6af0013de12fe374b2389afed808d9c1ae9d8983","datavalue":{"value":"1451.68323","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4559809$8F6A74A3-086B-41E1-B5A9-FC87C5F4F642","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f2e6f140877434cfd9fd1e8e1bdd1850acdbe408","datavalue":{"value":"10.1017/S1471068418000212","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4559809$1C8AA6B9-CAF3-4084-B675-9FAAD1224A4E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"78d52696cce5e5e7b30b955fe5f15748a5600173","datavalue":{"value":{"entity-type":"item","numeric-id":2119107,"id":"Q2119107"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559809$8CC2D04F-E79D-400B-8D0E-B1C18898ED11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b27769e9968e9fdaa00fa32144eb36042e431b7a","datavalue":{"value":{"entity-type":"item","numeric-id":4559808,"id":"Q4559808"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559809$F82D1A90-1389-459B-9C5C-CA8817DF4CD2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f9cbab8cb9619eb1f53de501c60c49def4220f6e","datavalue":{"value":{"entity-type":"item","numeric-id":604858,"id":"Q604858"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559809$D9A9CF86-78D0-4E4F-8C01-A833A12956FA","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":"Q4559809$D73877A6-469E-4689-B4AE-14E0CE25788A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3057b7b50937a91885954ebcb046fa2257c3f34a","datavalue":{"value":{"time":"+2018-12-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4559809$9536E911-E51D-4E62-A7BB-1B3C0BF71A2B","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"89864cc2b18fc5ba5e644d2454008b4c1fdc26e3","datavalue":{"value":"https://arxiv.org/abs/1804.11250","type":"string"},"datatype":"url"},"type":"statement","id":"Q4559809$DCF9060F-F611-4913-A792-D834D6041305","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4559809$084C8F72-4843-4191-9E2B-15F07D64248E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4559809$5D98D1B1-285C-447E-BEEB-04426A97596E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b492f281b8f52c724f2bc547e7e570cccf4bd5e0","datavalue":{"value":"68N17","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4559809$C7150959-CCAD-44C8-9BA9-AF024AA90877","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4559809$3603496A-9078-4D1F-958A-84DE0928CA9E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"dd0d7ffcd46f84493561dc06cbfa47c825dd1568","datavalue":{"value":"6988657","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4559809$477CFD38-9B6F-4528-8BD1-2E9695FED75B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b0166f1ddbe866ce3e3385c21e3a1c10afc5e804","datavalue":{"value":"proof-relevant logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q4559809$6C0CEF60-BBDC-4D9E-9A6A-DF699832EFE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0e431190495251d75e7d7f973ca704f4139885eb","datavalue":{"value":"Horn clauses","type":"string"},"datatype":"string"},"type":"statement","id":"Q4559809$68CBE82A-A3F7-46FD-B6FF-265DFB2DFAE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e22447b229c7a32c8d247e1ea4002861fd0fbd68","datavalue":{"value":"dependent types","type":"string"},"datatype":"string"},"type":"statement","id":"Q4559809$5ECF6E30-AB72-4EAE-9694-523D6024CF1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"07672cd9efb7a614e96dc9a58bd5b5685cbf3a1d","datavalue":{"value":"type inference","type":"string"},"datatype":"string"},"type":"statement","id":"Q4559809$8CFE70A5-5C9E-48BD-B58F-D72FE61A005D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2ce8922b2d37907222f852b12ec9cee646fdf210","datavalue":{"value":"proof-relevant resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q4559809$AF150741-2A65-4147-9809-126B0780EBD1","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2b02b46847f3d7e3a5825b9484a88607b98dbd14","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559809$923895A1-8638-49E8-B1CD-8D7086614190","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"be9a1fdbfd35f7a816de32e6d9d9a2a21796c942","datavalue":{"value":{"entity-type":"item","numeric-id":14061,"id":"Q14061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559809$84E19A6A-D64F-4E67-B71F-658805C63647","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a94daa7865c51c0d2412cced8422ea9361d06e30","datavalue":{"value":{"entity-type":"item","numeric-id":21343,"id":"Q21343"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559809$BF58E8D7-007C-43E5-AA42-69E589264F9F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3b770a87ca9a9c88e8d7293f2ff0eb880186c71f","datavalue":{"value":{"entity-type":"item","numeric-id":21669,"id":"Q21669"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559809$6B4B4B48-4F9D-492C-A44C-C7805D36D866","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e603d7c91a5659a0e67ae5a0b1fc4700fb0830e5","datavalue":{"value":{"entity-type":"item","numeric-id":31834,"id":"Q31834"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559809$B0D62337-3D92-4784-8964-2F062D47F84F","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":"Q4559809$4BC84253-9C2D-4D39-A1C1-6F75433CE9BA","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1af6faeaa96bc7cdaf3630e5a348ae8661139c01","datavalue":{"value":{"entity-type":"item","numeric-id":5398331,"id":"Q5398331"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559809$710BBDA6-5326-4026-8DC9-F9DEC41C10F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"20d69065fe873ad58ccd92876034942e696180d0","datavalue":{"value":{"entity-type":"item","numeric-id":2409746,"id":"Q2409746"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559809$462ED9F4-4EC1-44C0-B443-402BE13E4A30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6e9b5196a22fbb287ea0d893577e0a54523feae9","datavalue":{"value":{"entity-type":"item","numeric-id":2628299,"id":"Q2628299"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559809$EDE052E8-121A-421D-B8B9-BBE6F73C712E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d43f11a5e6fc21caa581e9ac1e35682b1839d73e","datavalue":{"value":{"entity-type":"item","numeric-id":3075246,"id":"Q3075246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559809$E96C7E71-534D-4499-9FAC-E1C3F8C89E07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0c3c69fa2672b8fa81e2d2be45ac3f1049ef642d","datavalue":{"value":{"entity-type":"item","numeric-id":5277716,"id":"Q5277716"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559809$6CC289D8-2DE0-4B38-B98F-058E96EEE6CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"05e9eeec6bb7769b1db1e07b9255b3d8a4e90e69","datavalue":{"value":{"entity-type":"item","numeric-id":5962831,"id":"Q5962831"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559809$7904FC77-FE38-4996-93AC-2484D0EC24ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"91bd407bcecb63e1d4876dcd09d799ba25c8af78","datavalue":{"value":{"entity-type":"item","numeric-id":4391451,"id":"Q4391451"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559809$EEEAC330-71F9-4FA7-A354-93DDB9EC7133","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"436d4ddccf9258c9f31fa193f202f774ffec18b8","datavalue":{"value":{"entity-type":"item","numeric-id":1250704,"id":"Q1250704"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559809$5CCEF80D-769C-49D5-A624-7512E4E435E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6b19eae06ce0ec3719d39a65466af8f728d39032","datavalue":{"value":{"entity-type":"item","numeric-id":4912883,"id":"Q4912883"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559809$79C1D5E4-C812-4398-B9EA-BB862E3F90D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a90a510f27550100d45a2ef21dd83bca5c9e1966","datavalue":{"value":{"entity-type":"item","numeric-id":5747747,"id":"Q5747747"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559809$5F4D9A07-DF90-4912-A367-262038CA6552","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7af009b1b1ee6ba839f21ce70ab3fef4eeae3348","datavalue":{"value":{"entity-type":"item","numeric-id":2364699,"id":"Q2364699"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559809$B2CC3C9A-B616-4A09-AE22-7CAEA8FD8F56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"149c6701797bc70b9623feda8cb44be3225ef16c","datavalue":{"value":{"entity-type":"item","numeric-id":5746216,"id":"Q5746216"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559809$FE0053F9-9F5B-4E45-9CBD-700239FEC7C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a007c6459a88d6afaab3912f3980a8bcc870bc6","datavalue":{"value":{"entity-type":"item","numeric-id":5451969,"id":"Q5451969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559809$D1284B83-5459-48C1-A001-75AB85CC212E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"552cf0c368b7ac55c2f6d32e41dd23a5e27d1fb8","datavalue":{"value":"W2964059082","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4559809$749B8F48-9449-4EDD-A3CD-1B0DA6156C0B","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"f383cbb18ecd3bd2e8c18bd68df3ca634f6a2569","datavalue":{"value":"Q129410361","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4559809$7BAA1CB0-E0AD-4C4A-A992-A2FAA3030F5C","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6a3fdab42aa36146f56037c1a7937389fbaafee4","datavalue":{"value":{"entity-type":"item","numeric-id":4508310,"id":"Q4508310"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"693bf80443ac2f873b02bc9ad50e2543af36d4c7","datavalue":{"value":{"amount":"+0.7712690830230713","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":"Q4559809$3A53AA13-F70B-455B-B4A8-6A9E5DFAD216","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"95184a3deb447e059c5a798e81c8c44969fcd365","datavalue":{"value":{"entity-type":"item","numeric-id":5743587,"id":"Q5743587"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e55ecf9113a43edab7fc5d6a4c3dbedfee300f70","datavalue":{"value":{"amount":"+0.748112142086029","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":"Q4559809$D201C3FA-0EAA-4785-B390-0449D2925182","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"83ead96eb0dad59b33308a29c10c00c5949abf9c","datavalue":{"value":{"entity-type":"item","numeric-id":2723415,"id":"Q2723415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fc58781d99dd4e27f2e6ca1322ec3ab310c36e5a","datavalue":{"value":{"amount":"+0.7413097620010376","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":"Q4559809$2FBFD81E-B323-49CE-ADC8-237D3352D835","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6375d904022100cb81376160eb9f0da8c95dfdf0","datavalue":{"value":{"entity-type":"item","numeric-id":2941181,"id":"Q2941181"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8c45ff289ff5847540c45ef31bab8d3dc02b9cbe","datavalue":{"value":{"amount":"+0.7413094639778137","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":"Q4559809$1596E560-245E-49B6-8F11-DD136CF53D18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ec2f0bb38b56f759cbb69a7dc3cbce032e16f8c6","datavalue":{"value":{"entity-type":"item","numeric-id":5055716,"id":"Q5055716"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2e281636df0836b6e256d2c00f140dc50b0c3e5d","datavalue":{"value":{"amount":"+0.7387161254882812","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":"Q4559809$E33F0344-20A9-4025-B901-EE68E9FDFE77","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Proof-relevant Horn clauses for dependent type inference and term synthesis","badges":[]}}}}}