{"entities":{"Q5389080":{"pageid":7418654,"ns":120,"title":"Item:Q5389080","lastrevid":58561341,"modified":"2026-04-05T18:30:57Z","type":"item","id":"Q5389080","labels":{"en":{"language":"en","value":"Rewriting-based quantifier-free interpolation for a theory of arrays"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6027837"}},"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":"Q5389080$793CF0FC-CF31-4D88-9012-80694F254C8A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0d008fb24bb9bc2dc7dffe32cf4de0cba8f2218b","datavalue":{"value":"1236.68179","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5389080$7F6FAF1C-7214-4C62-9F72-645F8E08B6B4","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7b1bce7f658807241618c24b1a425d03bccc6443","datavalue":{"value":{"entity-type":"item","numeric-id":479813,"id":"Q479813"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5389080$47A54157-19EA-4545-9AA5-A12D060296FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"44f075398e4ccd740a9ac00697271020232935ff","datavalue":{"value":{"entity-type":"item","numeric-id":284229,"id":"Q284229"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5389080$CE37184E-BEA5-48FE-B096-F2EFCA8790D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7a648f5f5c43d7007feb24ddb34b99c77877b620","datavalue":{"value":{"entity-type":"item","numeric-id":219438,"id":"Q219438"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5389080$040B6F24-652E-42B1-83EF-14F48A579EE4","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"85ed9f287d2ea9a2dac92419860840c9949df976","datavalue":{"value":{"time":"+2012-04-24T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5389080$5E7855DA-DC80-4FCE-A913-20D8B43F6353","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"442f3298bc26042f0d48e6dcb4dd84180d22023d","datavalue":{"value":"https://arxiv.org/abs/1204.2386","type":"string"},"datatype":"url"},"type":"statement","id":"Q5389080$576E80AB-2B72-4CB9-BF73-AF42FE206BF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P205","hash":"807c4c66b3801fb2f96cbcb74dbf5731b1f42e22","datavalue":{"value":"http://subs.emis.de/LIPIcs/frontdoor_884a.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q5389080$294CE5D1-8B69-4D94-ADBF-F5F954D33E78","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5389080$CAF625A9-9329-4D08-8F38-3264BDFF4230","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c636094cc8b933189eabd7c009d327f829bc6ac4","datavalue":{"value":"68Q42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5389080$29A11E5F-30A8-40E7-81D6-9DBD82BF6DBF","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1c8bd3bfcc5e2099e9335b0857e3fbf056d450f8","datavalue":{"value":"6027837","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5389080$E9387C9D-7ACB-4D86-8F47-82893393CEB6","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"476e70cc5d552d5cdc76575cc73d40a8bfb4b86e","datavalue":{"value":"rewriting","type":"string"},"datatype":"string"},"type":"statement","id":"Q5389080$77546393-5A8A-4B4E-80E5-7897C7AC8326","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d9bc6474ad8409ef4528af84655741b6b5be3d7c","datavalue":{"value":"interpolation","type":"string"},"datatype":"string"},"type":"statement","id":"Q5389080$75DDA114-76E5-4857-AE55-0224D2E482EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3270f1a4769ce41d92ad7a61e341b778f67336e6","datavalue":{"value":"arrays","type":"string"},"datatype":"string"},"type":"statement","id":"Q5389080$07C8EAC7-1853-4966-98A0-2DD303865FAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"379a567f0f983e236f95705804d342510fc41004","datavalue":{"value":"model-checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q5389080$6CDE98B6-F621-4151-9948-FAD2F90AA446","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"776ec61ea9403d0c48a81eefe331d6bd9e850b8f","datavalue":{"value":{"entity-type":"item","numeric-id":20435,"id":"Q20435"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5389080$AD1304AD-B836-447F-83DD-D3F3C6CC030C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b194bd31d37c1243d7e8c5eddae754651b6b0ca4","datavalue":{"value":{"entity-type":"item","numeric-id":18941,"id":"Q18941"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5389080$6C0B4D25-5365-435C-8FF2-B47E8CE9F292","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":"Q5389080$75306A2A-8621-4B92-8198-D342B0399868","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"62e50458851c1324d969c882280556d188a72fb0","datavalue":{"value":"W1509079171","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5389080$9E0BD119-0A08-4599-8E6E-61007A0F0210","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"737f1a02d671512bda3a50d05f08ff0d7e5e3d80","datavalue":{"value":{"text":"Rewriting-based Quantifier-free Interpolation for a Theory of Arrays.","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5389080$082E934D-37B5-445B-9B65-B0B78320B5A4","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6c57d54f63c1799f3fa733530a7798d720d4c984","datavalue":{"value":"10.4230/LIPICS.RTA.2011.171","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5389080$197EA366-BEDD-496F-AAA0-5732FA28473A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dfa5b8ee219383bf057660ccaa8422e52df4e875","datavalue":{"value":{"entity-type":"item","numeric-id":2887061,"id":"Q2887061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cd36dc5affb7476b5c8d5f5e94aed8bb2d81ee73","datavalue":{"value":{"amount":"+0.949566662311554","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":"Q5389080$8FDFEC91-CB6C-4A57-851C-ED3360F60886","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"daa9afc57ffd58556591d3bffe0ed72033c0f499","datavalue":{"value":{"entity-type":"item","numeric-id":3172885,"id":"Q3172885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"531786723871a18a072793cb9f3747b321f46499","datavalue":{"value":{"amount":"+0.9139124751091005","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":"Q5389080$35D64FFD-0D01-4D3F-8FFF-79ADEEDF5D1E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"33b9f803b485945da86faf8cbeb621e43e8d77e9","datavalue":{"value":{"entity-type":"item","numeric-id":1799115,"id":"Q1799115"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3b938958cdb1928978c7cf9a5eb33236185c6c59","datavalue":{"value":{"amount":"+0.8296098709106445","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":"Q5389080$8BD488E7-74C8-4D09-B911-8B36DE71E314","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"192babe1f332f85d504aff10a4562aaa3e265788","datavalue":{"value":{"entity-type":"item","numeric-id":5308386,"id":"Q5308386"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"726198dc978ccb4fd213581e64897463c1c64e2c","datavalue":{"value":{"amount":"+0.7770808935165405","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":"Q5389080$807CDE25-B296-46EF-ABA7-02C7C49F4124","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e412e6216b54f0d01b161d965adaae87ffed390b","datavalue":{"value":{"entity-type":"item","numeric-id":2575736,"id":"Q2575736"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0e3576a3bfcade9f3bb0fdaef68e3afab7f8b0e7","datavalue":{"value":{"amount":"+0.7770388126373291","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":"Q5389080$1F5F1F33-A57D-4EDC-AD22-38BDDDA2E2C9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5389080","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5389080"}}}}}