{"entities":{"Q4644353":{"pageid":6673934,"ns":120,"title":"Item:Q4644353","lastrevid":58316925,"modified":"2026-04-04T16:57:22Z","type":"item","id":"Q4644353","labels":{"en":{"language":"en","value":"Predicate pairing for program verification"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6877188"}},"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":"Q4644353$E2B31B9F-753C-44AF-95A9-EF5D77451364","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5a143ecda18708792e5cc664111e95b2c7bcd9a7","datavalue":{"value":{"text":"Predicate Pairing for program verification","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4644353$3F00780C-A7D0-4681-BAB2-095E2DDDB001","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2ad71ace67d29441e3a8affa64cdd8b4ec0aeb82","datavalue":{"value":"1478.68153","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4644353$5A18AF53-870A-46C9-A7D8-78734D1BCD60","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7e875d2234a7b75e120e0c20e8c22b9fbc72744a","datavalue":{"value":"10.1017/S1471068417000497","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4644353$8BE1662D-2253-4B6B-8583-301E31F57735","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":"Q4644353$40096E67-9B30-4681-8C93-7AD0BE96E157","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":"Q4644353$D736B215-07DD-448D-B08D-AD69A68597E8","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":"Q4644353$03D810AE-76D6-46DB-AE30-03A213E3E499","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":"Q4644353$57D877D8-B739-42B5-9714-676C6B133160","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":"Q4644353$989FD5C2-8084-407C-8761-AAC1CD759FAB","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":"Q4644353$619FA855-4885-46EE-B562-2D8838ED1A81","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"1b4bdbd5e1ca720c88a16a645d0b846a670a83d2","datavalue":{"value":"https://arxiv.org/abs/1708.01473","type":"string"},"datatype":"url"},"type":"statement","id":"Q4644353$D8BF26F7-1435-4DA1-A093-5FCD9CFBB15E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4644353$A9D5CC5F-DE7A-4CEF-BE28-E4C589A536D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4644353$841E2F34-9688-4E6A-8E06-319FFAE4A662","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b492f281b8f52c724f2bc547e7e570cccf4bd5e0","datavalue":{"value":"68N17","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4644353$1A6FB4FF-01DF-4E55-84FB-F458926A6249","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2b01c4c352cd1bc4c76caf5fa9e7b68276152510","datavalue":{"value":"6877188","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4644353$50391C9A-384E-42BE-85F9-055160D3A1E3","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c50d987ab7c3ea2a41cb6aca681d912964971ed8","datavalue":{"value":"program verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q4644353$B91484D4-1B40-440F-82F9-C488670E5C69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8e47d18da5a3cc46f307e12b53d17a8f72c7da71","datavalue":{"value":"constrained Horn clauses","type":"string"},"datatype":"string"},"type":"statement","id":"Q4644353$7DE2B831-42D8-4FCD-BB63-AC9F84C9B472","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3ae3f0d13ad92818eaf45462f9d67f2d319a5148","datavalue":{"value":"constraint logic programming","type":"string"},"datatype":"string"},"type":"statement","id":"Q4644353$36263046-4FA6-40B4-8C1B-152FB3DF6048","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"322ea768f2b97508db847d80bb51e98a654d6c56","datavalue":{"value":"program transformation","type":"string"},"datatype":"string"},"type":"statement","id":"Q4644353$C2010178-2C9E-4465-BCC9-7A1D2101D8C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"92bfd70eaa0d003cf5f76cede11fce70470d1f73","datavalue":{"value":"relational properties of programs","type":"string"},"datatype":"string"},"type":"statement","id":"Q4644353$8AFF79E7-FB84-4D5B-BFBB-C8DE6B089DB6","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":"Q4644353$C647A624-2385-48BE-9529-A6E15CC8C5F0","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":"Q4644353$F0BA9F1F-2FBA-44AF-BB8B-FEA41F00FC58","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"902d58911cf57d61e4e30d431d92c375a51f10b6","datavalue":{"value":{"entity-type":"item","numeric-id":3452246,"id":"Q3452246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644353$4DD70DEE-3F8C-4B49-BC3F-DB710E66A148","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":"Q4644353$C1AC465D-DF3F-49CF-A189-9DD6082EDD14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2f2b1ebc1ae7ffc3042b5e838a24da8662374478","datavalue":{"value":{"entity-type":"item","numeric-id":5898633,"id":"Q5898633"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644353$379BCF5E-C47A-4C97-B8A3-914BEEB5873F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"995a3a5c42994c6db5c9ecb05a842b528a1d92e3","datavalue":{"value":{"entity-type":"item","numeric-id":2891406,"id":"Q2891406"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644353$5C4FE759-8CD4-4120-B4E9-2C929595BA4B","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":"Q4644353$C3302C8E-B142-43EA-BCAF-121F565F24CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e68b34a2955d7a99c7c7b2eadae5af33fc6bd2ff","datavalue":{"value":{"entity-type":"item","numeric-id":3187012,"id":"Q3187012"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644353$1DF6718C-91A1-4F24-8515-77F97F0ACDDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6cb34b6e7428e42f8251fed44fb40d3732a20e55","datavalue":{"value":{"entity-type":"item","numeric-id":1664383,"id":"Q1664383"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644353$DAF47042-4DFD-4112-A87C-779C06BF95E3","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":"Q4644353$00C2E3BA-E10D-46E0-8B6B-FB8834A2E2D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"824d7586a86fe6f70db23718bb2fca961f066999","datavalue":{"value":{"entity-type":"item","numeric-id":4285643,"id":"Q4285643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644353$18ACC3D0-E073-4E31-8DCB-5C9C652A48A0","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":"Q4644353$99F7D465-4B1C-4B79-8439-08FEC2EB3FA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8a9e6dd0047866bfc8e77788fb7e9f9e563b66da","datavalue":{"value":{"entity-type":"item","numeric-id":4633561,"id":"Q4633561"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644353$7DDC0366-21BD-40F8-BB50-5945501EB5E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"288b725ab687a95bc6670d223f1b01dcbcb6a8cf","datavalue":{"value":{"entity-type":"item","numeric-id":5326329,"id":"Q5326329"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644353$AA4D89B0-2057-436E-92CD-315BB78BB6EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"98855e5f63a687d22ad5b8fcf60eef7c9c99fe2e","datavalue":{"value":{"entity-type":"item","numeric-id":938300,"id":"Q938300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644353$A929F120-B1EA-4BA3-8541-F65DB926FB99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"323dbd6fd6973b3663055cf97da83be885dd9ec7","datavalue":{"value":{"entity-type":"item","numeric-id":5569944,"id":"Q5569944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644353$FDE7D06B-A5E7-4EC8-A70B-66C706EB2101","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5c184a968cc4e5306fda681741508fd66f4b9c69","datavalue":{"value":{"entity-type":"item","numeric-id":4391452,"id":"Q4391452"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644353$7644B365-63D6-4EAC-91B0-C4FDFE3286A6","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":"Q4644353$7EE24888-FDB3-49D1-8E43-D2A714677309","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dce3c2e75c2ce94c37447123ec1c37ac00aeec39","datavalue":{"value":{"entity-type":"item","numeric-id":4452606,"id":"Q4452606"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644353$A56CA308-9A25-4F75-80FC-64C5DAC06E64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"606b55142cd4468a9a74e0ea3982d2b3991333cb","datavalue":{"value":{"entity-type":"item","numeric-id":3992908,"id":"Q3992908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644353$A0BD8741-06BE-461B-B083-98F0BB13EBD3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"52b946fb2f63c0dda27fa5ba25a5cecdec9a1c9a","datavalue":{"value":{"entity-type":"item","numeric-id":4229041,"id":"Q4229041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644353$3A0F3092-00EC-403F-AA25-A63E14DE3CE9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"03c75790c9dd4ffc2c395fdf76c21f0ca40efe2d","datavalue":{"value":{"entity-type":"item","numeric-id":5504599,"id":"Q5504599"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644353$235A8BE0-BD26-413A-8D1A-E3DB79CAA6E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e61caeb9ccf34c77ec2a456b135b01b408ce9535","datavalue":{"value":{"entity-type":"item","numeric-id":853733,"id":"Q853733"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644353$E15EC046-D1C8-4493-B421-ABA3E1406304","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bc8d76c6c2a703677e15081f90265ace1b4e83d2","datavalue":{"value":{"entity-type":"item","numeric-id":4305629,"id":"Q4305629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644353$B3F70B1D-AA2E-484A-8FC2-A7134955F7C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4005b1ea71aceae7826269dffb4b9e393524a878","datavalue":{"value":{"entity-type":"item","numeric-id":2281656,"id":"Q2281656"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644353$99C63E0B-8417-46E4-A178-8B976348E28A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aa2ecb01d1000f707b2d4e9dd305373c58ecfc0c","datavalue":{"value":{"entity-type":"item","numeric-id":3636883,"id":"Q3636883"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4644353$D61E8F4C-45AD-4B61-93FF-93BB281AAD3C","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ac0115479f78da3ec2407693b324926474cb63ec","datavalue":{"value":{"entity-type":"item","numeric-id":1671163,"id":"Q1671163"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4506314705923f398571eb2ec0333baae83c4fd3","datavalue":{"value":{"amount":"+0.8558731079101562","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":"Q4644353$4108569F-9933-4C22-9344-7C6ABA399C29","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":"d2a0153bc5214e7991b2443e02531c3303e04960","datavalue":{"value":{"amount":"+0.824139416217804","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":"Q4644353$D3E0F4F9-D702-49BF-8E4B-577D9C4A7F3E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e410a22aa42a04ba3966858f89a4b8e65bd18138","datavalue":{"value":{"entity-type":"item","numeric-id":4593003,"id":"Q4593003"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3ffd9d260d6fc4c3a620b862d544c88d469f5159","datavalue":{"value":{"amount":"+0.760833740234375","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":"Q4644353$9182F30A-D2E2-4B45-B684-BB8ECE1E1C9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3f1ababec7ad08320487551d5fd7dcd8e4e6cb2e","datavalue":{"value":{"entity-type":"item","numeric-id":5233234,"id":"Q5233234"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5f1bddeb7e48da69932a316e4a8e3ff171f5c741","datavalue":{"value":{"amount":"+0.7593705058097839","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":"Q4644353$42DA683D-9F46-4E67-805E-D1A47267AA86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0819deb17284ae696ab95b266fd2839a405b9311","datavalue":{"value":{"entity-type":"item","numeric-id":832229,"id":"Q832229"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0b981f74d8ccdc45fd94829f5ff1ca7741ff887e","datavalue":{"value":{"amount":"+0.7506380677223206","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":"Q4644353$794A1998-75D6-4036-9B7E-E518294FAE2A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4644353","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4644353"}}}}}