{"entities":{"Q4559806":{"pageid":6589397,"ns":120,"title":"Item:Q4559806","lastrevid":97325519,"modified":"2026-06-05T13:59:56Z","type":"item","id":"Q4559806","labels":{"en":{"language":"en","value":"Solving Horn clauses on inductive data types without induction"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6988655"}},"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":"Q4559806$F900CFD0-5A29-44CE-BFF0-6436514B0951","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"357c5e5ed17cb8ea64256311a249548be87161eb","datavalue":{"value":{"text":"Solving Horn Clauses on Inductive Data Types Without Induction","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4559806$70CF7A56-2112-473A-B3A6-33C9297D7F71","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"60aec28d80bfb79f5fdef38369ed27fa7f0f486d","datavalue":{"value":"1451.68172","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4559806$B186D08C-61F8-459B-A9F8-A793DDB362E4","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7188f44b72491d2b096bca67a82e688d64954d9f","datavalue":{"value":"10.1017/S1471068418000157","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4559806$FA53082B-F8DF-40A3-B42E-C32E2FD95979","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"848f825b7d044d82deceb7cfe1f0d1c0ec5247c6","datavalue":{"value":{"entity-type":"item","numeric-id":1664381,"id":"Q1664381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559806$3EE756C6-F404-4AED-8AFB-1BD7811B8625","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6ad0fb3e6789b1b1570ed736e8448792de0de85a","datavalue":{"value":{"entity-type":"item","numeric-id":1664382,"id":"Q1664382"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559806$781D2C03-51B7-42F9-89B2-80D3591FAD46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a87226e249edb34abf2b072fcc5b9b500b03b478","datavalue":{"value":{"entity-type":"item","numeric-id":673495,"id":"Q673495"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559806$10EE31E7-24BB-4A23-BE68-EB071CC961AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1b380511e08624421de73be74130c083d2234aa7","datavalue":{"value":{"entity-type":"item","numeric-id":673494,"id":"Q673494"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559806$674B6FF9-0478-4867-9229-BCE943743D7E","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":"Q4559806$CB859596-08B8-402B-8D08-9E2B5EEDA710","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":"Q4559806$D6A5FCDC-8100-424F-A95A-5341F8B8E6EA","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"99da87270ace3445d0f1e99e7c781782077209cd","datavalue":{"value":"https://arxiv.org/abs/1804.09007","type":"string"},"datatype":"url"},"type":"statement","id":"Q4559806$EA6F7228-380B-4A38-B486-979714CF239F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4559806$94855F05-02AE-4EEC-BDE0-A3E8FF4C9401","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4559806$0C7EB786-6CEB-4004-A16D-E9CB3517CC1D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b492f281b8f52c724f2bc547e7e570cccf4bd5e0","datavalue":{"value":"68N17","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4559806$F4C667CE-0484-4AB0-8D1D-D7125E8A927F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"fd704ba40784b1a253476b595033d30459b6f136","datavalue":{"value":"6988655","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4559806$64A7DB5A-2FA2-4032-B5C5-BC815D2435B5","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c50d987ab7c3ea2a41cb6aca681d912964971ed8","datavalue":{"value":"program verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q4559806$D39FDF0B-281A-419B-84E9-6E1C277AC0B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8e47d18da5a3cc46f307e12b53d17a8f72c7da71","datavalue":{"value":"constrained Horn clauses","type":"string"},"datatype":"string"},"type":"statement","id":"Q4559806$2EEACDBD-697C-49D1-8BB8-042DBCEA22FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3ae3f0d13ad92818eaf45462f9d67f2d319a5148","datavalue":{"value":"constraint logic programming","type":"string"},"datatype":"string"},"type":"statement","id":"Q4559806$583DC23D-4ACB-4965-A671-A5766FCD5A4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c2710a3e7b11911831dbb8f491dcf476baab7504","datavalue":{"value":"inductively defined data types","type":"string"},"datatype":"string"},"type":"statement","id":"Q4559806$440A0FC3-7285-40DD-9CFF-5C7F6DFCAE3F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"322ea768f2b97508db847d80bb51e98a654d6c56","datavalue":{"value":"program transformation","type":"string"},"datatype":"string"},"type":"statement","id":"Q4559806$41251423-899D-4E89-991C-34A2F88BA261","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"91dd7e13f71e3e62484b361def521e363c006e6b","datavalue":{"value":{"entity-type":"item","numeric-id":16380,"id":"Q16380"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559806$AD2FC432-600B-4641-8F38-2A46D1A8FE2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"875fd2341d7eaef60a26a549ea0c9adfdf328e2e","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559806$4B499EA3-FAE9-43C4-ABEE-493B4481E579","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3cd8007490a248a080808f77e0123c492d98333d","datavalue":{"value":{"entity-type":"item","numeric-id":17497,"id":"Q17497"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559806$BA4686F0-E587-4F7F-AA1D-FB3E2D6A2CA1","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":"Q4559806$317BA968-4602-41C1-A700-04D6DE7379E4","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"2518ba6a38fa213a00f5ef7c14d9debc5928424c","datavalue":{"value":{"entity-type":"item","numeric-id":2947164,"id":"Q2947164"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559806$729B3D29-5064-4E24-8F6E-E1796834EA4E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d331af7e92433b34c365e6444eec7a3e4b80ac8b","datavalue":{"value":{"entity-type":"item","numeric-id":4593003,"id":"Q4593003"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559806$5C73C251-DBC8-483A-9812-0B0721BCA451","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e686760572df5641bfac6bcee2da65d060471e37","datavalue":{"value":{"entity-type":"item","numeric-id":4589602,"id":"Q4589602"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559806$E2F4347D-28EA-493B-A79D-B865AF758BB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0705daecc5ffa3855114e3599480f53a82f40e64","datavalue":{"value":{"entity-type":"item","numeric-id":4939538,"id":"Q4939538"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559806$6A7D0D1E-52DB-462B-A6DD-9546C2AFFFBE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5ca4f823ca2e82e86e612699cdb65f38c133999d","datavalue":{"value":{"entity-type":"item","numeric-id":4052071,"id":"Q4052071"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559806$D36D12A4-116A-4774-968D-543E2748CBDF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f64b95fb93857a7fee214f8d1058a95819db0427","datavalue":{"value":{"entity-type":"item","numeric-id":671648,"id":"Q671648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559806$49851DE6-BBBB-46E6-853D-0DAA8C9F4186","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e357561b24d9113100e0759ecfadf0c69ade7ba0","datavalue":{"value":{"entity-type":"item","numeric-id":673496,"id":"Q673496"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559806$E8D5A571-9A25-458B-B13B-156940324DDA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6fcf4186c4480f5d344cc9880618b00ccbaf1502","datavalue":{"value":{"entity-type":"item","numeric-id":914358,"id":"Q914358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4559806$EAF7C480-81DB-484E-9558-E6418A742E9B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d38d531ebfcb6c94fc098771aa782e50b1cbb06b","datavalue":{"value":{"entity-type":"item","numeric-id":2164260,"id":"Q2164260"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cff9a58188170de9e280637fb26ebbeee2bf1246","datavalue":{"value":{"amount":"+0.7940322160720825","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":"Q4559806$CE3A56EF-2C05-4A56-924D-6501268C32E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8d029eaa256dcadd504eff29734e46b2e1f7a941","datavalue":{"value":{"entity-type":"item","numeric-id":1664383,"id":"Q1664383"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8221b659a0d6a0c0c16d881d59d479d5f4284fac","datavalue":{"value":{"amount":"+0.7760905027389526","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":"Q4559806$B9C2362F-0340-49C9-BC76-18E2CC1397B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d43e6e0d0ae7a229d36a7947d6edc16ba52ad99d","datavalue":{"value":{"entity-type":"item","numeric-id":5015369,"id":"Q5015369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8e4609e3460cfa4803ce109b179896b860df53b9","datavalue":{"value":{"amount":"+0.7566704750061035","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":"Q4559806$E7DFBAD4-2BF5-43CA-BC80-E84590438E01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f5a5bb51e3095387c40d880ae273a0fce71d2c1c","datavalue":{"value":{"entity-type":"item","numeric-id":2947164,"id":"Q2947164"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fb67f321d21f52b0c12be632cbf73d081a256424","datavalue":{"value":{"amount":"+0.7532534599304199","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":"Q4559806$1D58E2A0-FA84-4D5C-9B1F-B57AC2AB0929","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"93d9f92e014b8cf89953501d123fe5a2e8592152","datavalue":{"value":{"entity-type":"item","numeric-id":5016384,"id":"Q5016384"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9f1377dc72cb589df81b50e6772bee66e3d3bd84","datavalue":{"value":{"amount":"+0.7519863247871399","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":"Q4559806$5293826A-0B5A-4DA1-B93C-1060C907B829","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Solving Horn clauses on inductive data types without induction","badges":[]}}}}}