{"entities":{"Q4644355":{"pageid":6673936,"ns":120,"title":"Item:Q4644355","lastrevid":58311927,"modified":"2026-04-04T16:28:23Z","type":"item","id":"Q4644355","labels":{"en":{"language":"en","value":"Tree dimension in verification of constrained Horn clauses"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6877190"}},"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":"Q4644355$F93CEF66-145E-41FD-AA8B-ADBFDC3FFFC8","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8bf1de64733406adbd3c456f0b1b065265776bb2","datavalue":{"value":{"text":"Tree dimension in verification of constrained Horn clauses","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4644355$B2FFCD7E-E286-42A0-BD15-565D13C93066","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9b2a6ae54c4322cc4f7c38f2daacc36998525993","datavalue":{"value":"1478.68165","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4644355$D745F6B1-59EE-4C0B-B432-4902A97D12F8","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1c51a131224e7908488df45163cbbf2885730f78","datavalue":{"value":"10.1017/S1471068418000030","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4644355$4FAD619F-C772-4B21-999B-B9138948A87E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"f60cc7b23bdd947bfabaeff972c6281f9d07b25a","datavalue":{"value":{"entity-type":"item","numeric-id":681334,"id":"Q681334"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644355$01D44E62-3CD2-4531-AC92-3C6717A8C4CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f2c13ddb28c279be9eed2b39004f69512bab7c50","datavalue":{"value":{"entity-type":"item","numeric-id":238502,"id":"Q238502"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644355$E71EDA2D-E63B-4F29-8863-0B487793BAE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"32615fc5fb5dd13879921120a1ebbaef0bfe0d44","datavalue":{"value":{"entity-type":"item","numeric-id":453530,"id":"Q453530"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644355$FAB0B666-62E8-4BE0-8967-E1741387D9C3","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":"Q4644355$31309F10-928F-4FB3-8E0B-3C656A74EE9B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3b8198e5532e16196bbd5031625b4993403e9d10","datavalue":{"value":{"time":"+2018-05-31T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4644355$3F14D4B0-2C89-4893-8976-2E79A4B424F3","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"beecca7bf8f0367eb467b95f53a3ac4ba66eda24","datavalue":{"value":"https://arxiv.org/abs/1803.01448","type":"string"},"datatype":"url"},"type":"statement","id":"Q4644355$0A76F8AF-A109-4E75-AAC8-08E8AD580123","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4644355$72B03619-07B5-4FBD-B488-A6E497AEA396","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4644355$102993B4-0308-405E-BFB2-3DE8B450E7D2","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9318caf609503c3a7c78b83210ee79fef410bfce","datavalue":{"value":"6877190","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4644355$522351A8-8B2D-4785-AB88-84AE1A7F804F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"47511de611e7ca7c7f052290389ebfdae4c32892","datavalue":{"value":"specification","type":"string"},"datatype":"string"},"type":"statement","id":"Q4644355$3EF9E031-907C-42C6-88FD-5B5AFAE77811","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4ca9d50db1dfae5b9e3f00a896c80d6fbe7b0364","datavalue":{"value":"analysis and verification of systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q4644355$3B847224-BFE0-4C4A-BE21-5C2BB718DE13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0e431190495251d75e7d7f973ca704f4139885eb","datavalue":{"value":"Horn clauses","type":"string"},"datatype":"string"},"type":"statement","id":"Q4644355$5878488E-3723-49DB-8845-149BBE913DBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"837ac8ca4950e6221523747a44253ce00e92f9ce","datavalue":{"value":"tree dimension","type":"string"},"datatype":"string"},"type":"statement","id":"Q4644355$1C2C7DD5-5E31-41A3-BA0B-7763239B4B81","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"85575b60ef4d0a8413d3c895be2530b8915bc3fb","datavalue":{"value":{"entity-type":"item","numeric-id":16612,"id":"Q16612"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644355$59715DE5-B492-4A26-BBF7-EADF083CAB1E","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":"Q4644355$2FC6BE25-6925-4011-9633-B12DEEAFA1F5","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":"Q4644355$0ABC0CA6-2957-4E88-BE69-9C962D263D5B","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"69afe669909fd49bb6ef3208a12ea6ce27a44ccb","datavalue":{"value":{"entity-type":"item","numeric-id":4398769,"id":"Q4398769"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644355$7A6AFB52-B5E7-42B8-B190-915EB32BF356","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f69f8f34a60bf9705498c10e9caa4fa85b208af2","datavalue":{"value":{"entity-type":"item","numeric-id":1884876,"id":"Q1884876"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644355$415FD070-6C3F-46F0-A4BF-46A1446689C3","rank":"normal"},{"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":"Q4644355$46917793-C302-495E-B6D6-DFE54B8583CB","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":"Q4644355$F148F1F6-7EFE-4CD7-A7A2-A3E6906DB7C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bd64829d7a6aea806e84c4d0e05bf37f087864b3","datavalue":{"value":{"entity-type":"item","numeric-id":3590943,"id":"Q3590943"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644355$B9569333-674B-4B17-825D-5628CB313355","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"315ca477012cc40bb4745637b4fc7cc906fb2ef7","datavalue":{"value":{"entity-type":"item","numeric-id":2999782,"id":"Q2999782"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644355$121FDBD2-FF24-4419-B98F-60FF7F36A736","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fdfb6f4c3cb2a513720d0512ac6ad9a80b12c309","datavalue":{"value":{"entity-type":"item","numeric-id":5404898,"id":"Q5404898"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644355$3BB5A5E8-9C70-493E-94F5-73AD1B3EE9C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0a39da4a57272edb02d6053b5209e8619838564d","datavalue":{"value":{"entity-type":"item","numeric-id":3613383,"id":"Q3613383"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644355$2499E3A2-F0C3-455F-814B-B10079FB5710","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"acde43aadb68c83ae4d51574dcef8cc0958b2d7d","datavalue":{"value":{"entity-type":"item","numeric-id":3392921,"id":"Q3392921"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644355$5831A82F-E3A4-43DC-B25B-858A0B2A0105","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"445ffe708f46664a7fb3c95abfc0aea70b84e1a2","datavalue":{"value":{"entity-type":"item","numeric-id":2893101,"id":"Q2893101"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644355$E689A0FD-2746-4511-B4EF-65526DA75358","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e29a9e63db651327a88d88e2cdc75e51e9cd4afb","datavalue":{"value":{"entity-type":"item","numeric-id":2843329,"id":"Q2843329"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644355$FAD8A377-90AC-4D05-8445-660E3B460EC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"471abb3e7f4ab1ef1a7fc449604429dc98060673","datavalue":{"value":{"entity-type":"item","numeric-id":4245932,"id":"Q4245932"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644355$AB6CCF10-300B-429F-83E4-768979D3E18C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ab124a7373ba82029ffdcc597bda7b4f27aee620","datavalue":{"value":{"entity-type":"item","numeric-id":5287559,"id":"Q5287559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644355$CD8E24EB-790B-4237-A3BE-DA6C2971DC36","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"572996969ef39baefa4f0047a98961f63b9d6df0","datavalue":{"value":{"entity-type":"item","numeric-id":681335,"id":"Q681335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644355$7BBD9522-CBF4-4BAB-BC41-BB82C8421D24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5ca31605dad676d482d4e2d9ed5a4e54a411a1e1","datavalue":{"value":{"entity-type":"item","numeric-id":5015369,"id":"Q5015369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644355$B6D30A04-00D8-4F1B-AE4C-B67FA16081C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"80a1f57d31f37ba9bd0f9ba09187b833ecd83362","datavalue":{"value":{"entity-type":"item","numeric-id":4645746,"id":"Q4645746"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644355$89DC16A2-CEC0-415B-8BE7-39AB2C1B9799","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3b58947cb7a079bac0db1d082fc9f925471e0be3","datavalue":{"value":{"entity-type":"item","numeric-id":4023828,"id":"Q4023828"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644355$6F974F4A-31A3-4D91-9E02-CFB8FBEFCABF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"51f2ca6ecb8880c6f3ec68b373b2d00ee09d7f40","datavalue":{"value":{"entity-type":"item","numeric-id":2828307,"id":"Q2828307"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644355$DF69A406-A73F-435A-96A7-3CB7755032D5","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"13edc0fc1f71c1d3887ba4f9fd0d0a1aff5ea951","datavalue":{"value":"W2964124669","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4644355$2F1D8522-E332-4911-8524-4296CA1022F0","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"db7a7ce2ef86edbcda7a73ae36b4679337817949","datavalue":{"value":"Q129837133","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4644355$79F611F4-1B86-43C5-9BA9-7139360799CD","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9a2829ee7f5621f0f381ec164ab8665b84e3adc5","datavalue":{"value":{"entity-type":"item","numeric-id":681335,"id":"Q681335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cb58179b80c552bcb1f31be0439e7f336cb119d7","datavalue":{"value":{"amount":"+0.7370491623878479","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":"Q4644355$37DF1084-0294-4CF0-8E41-E34BC8E5FA91","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d0710bcb54d08efe82099eceeab9ddba784fcf2f","datavalue":{"value":{"entity-type":"item","numeric-id":5172644,"id":"Q5172644"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f1b6cbf5e03db1622265a4ce8ba51c3444940d7f","datavalue":{"value":{"amount":"+0.7322708964347839","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":"Q4644355$163B7E15-D1E3-4F3A-9251-5F72FD234D55","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":"e296516e515fdb8eca54e0bb9a6b2b9ff49e2b47","datavalue":{"value":{"amount":"+0.7189264297485352","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":"Q4644355$7871AD4E-6AE2-42EA-9C43-8166A0220012","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"75868a3bf204a6bf4c593cce4cab82fe98820348","datavalue":{"value":{"entity-type":"item","numeric-id":4559806,"id":"Q4559806"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7d13fde992c112b42fa9c8c8c79793833a48c8c3","datavalue":{"value":{"amount":"+0.7081640958786011","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":"Q4644355$49B36A16-F852-43B0-85C8-29BAEB4148AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e47925fed405dd2cdc4dcaed33128e48e175efde","datavalue":{"value":{"entity-type":"item","numeric-id":5016383,"id":"Q5016383"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cc44c5f1a92548491756c29ce77afa1f88941640","datavalue":{"value":{"amount":"+0.7019813656806946","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":"Q4644355$FA61C90D-01A0-4B6F-8A36-D065EE634155","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4644355","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4644355"}}}}}