{"entities":{"Q4633544":{"pageid":6663125,"ns":120,"title":"Item:Q4633544","lastrevid":90104531,"modified":"2026-06-04T19:14:54Z","type":"item","id":"Q4633544","labels":{"en":{"language":"en","value":"Satisfiability modulo heap-based programs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7050649"}},"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":"Q4633544$F6BBFB54-B921-4A6E-BEDE-19D588FCCB92","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"911963fcb12b2d319ab812b98211ed30fff0c83d","datavalue":{"value":{"text":"Satisfiability Modulo Heap-Based Programs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4633544$0884B552-D5DD-4968-BE6D-CB1D106BFC8F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"29d9c51926aaa0a4456259c474528fffdc1138ca","datavalue":{"value":"1411.68028","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4633544$967BDA10-4989-44B4-881D-45CC2ADE3D05","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f0182ae886af3c841c5fdfeed2bbe13c8cfdf9dd","datavalue":{"value":"10.1007/978-3-319-41528-4_21","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4633544$007F6F4F-E25C-436C-BE43-FA704C030CE7","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a423a466fbecbb20f333bdb71f0b06a2cb01ab3f","datavalue":{"value":{"entity-type":"item","numeric-id":2234105,"id":"Q2234105"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4633544$171A3120-DD4C-43CC-9F46-EC625C74A286","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a29a8668613ef6f9130a40b44c1110c148f42ec0","datavalue":{"value":{"entity-type":"item","numeric-id":488229,"id":"Q488229"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4633544$F83D00FC-1A29-4B20-A57C-96B525D37548","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7350aed0b0267db3934820cd5357095f0cb6b7b1","datavalue":{"value":{"entity-type":"item","numeric-id":238508,"id":"Q238508"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4633544$1589FF98-6D2E-4F02-A3E0-A86530492CF0","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d4ba228bb5693c2e3eb7592c46c7d713183c8c65","datavalue":{"value":{"entity-type":"item","numeric-id":2864836,"id":"Q2864836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4633544$BEBA3454-3518-4313-9FFC-6050DBA7076D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"24db5d32115f39913353e80bae577d976822bb5c","datavalue":{"value":{"time":"+2019-05-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4633544$4C7920E6-ACBA-498D-9544-C7357F2F7B4E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"fdd860292dbf0476ad73fafd86e13803f1e5503d","datavalue":{"value":"https://ink.library.smu.edu.sg/sis_research/4937","type":"string"},"datatype":"url"},"type":"statement","id":"Q4633544$AEB7F1E6-0F25-4481-BC22-B7D91A36AF4A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4633544$56FD2EC6-DD2B-42A3-808C-3920DC2CC485","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4633544$BEB79DD8-DA16-484A-9DA5-E75AB53597CE","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e0aaec7d868f52d3a63ae2302e39e1727f54c094","datavalue":{"value":"7050649","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4633544$D2572E49-B681-4350-B9F0-56420B050772","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dfd2ae52b3325778b0c72742b08c947a3c4a2c65","datavalue":{"value":"decision procedures","type":"string"},"datatype":"string"},"type":"statement","id":"Q4633544$EB66739A-CBA8-420C-AC9F-6043D7D2D602","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"252f9f9ed9fe8ca406cc19fba38a46c0414791ee","datavalue":{"value":"satisfiability","type":"string"},"datatype":"string"},"type":"statement","id":"Q4633544$1952F5FE-A6C6-4577-85F6-CB3159BDE0F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"938358769b4f58ad078254388a41b1d2ec82e622","datavalue":{"value":"separation logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q4633544$051F3577-EB59-434E-8BA0-9BC06CC6C753","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ec380ca252be3c5f710d69356f4a05c9923ebeab","datavalue":{"value":"inductive predicates","type":"string"},"datatype":"string"},"type":"statement","id":"Q4633544$B41E3B50-97E3-4CD0-99C2-DA52ACDCC384","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c8255afe24ff623e2eec5328fe47d34a79bf3589","datavalue":{"value":"cyclic proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q4633544$C616809F-C240-4FD5-A39D-2A1DCAC294C1","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":"Q4633544$951F4237-F5D5-469B-A0E5-ABDAA44C5548","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"2861a2480e0600270a2611e06ed67d54309f1c71","datavalue":{"value":"W2502150621","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4633544$095422B8-B9FF-4D2C-83D8-CFB26EBE4184","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"250834f45f057a927abfea28e9f0a9bff54c14a0","datavalue":{"value":{"entity-type":"item","numeric-id":4635608,"id":"Q4635608"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4f01fed09f9a31c47a9a3664fbeec174e4a93a2f","datavalue":{"value":{"amount":"+0.8491821885108948","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":"Q4633544$F8344CDF-C0FA-4743-BE04-427F0C5C60D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4d1337f6f778fe290fe3a403311747133f44a1a0","datavalue":{"value":{"entity-type":"item","numeric-id":1990511,"id":"Q1990511"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a5681d98eba0fe6e6614576e8fdee69fa5f8a77e","datavalue":{"value":{"amount":"+0.8221789598464966","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":"Q4633544$E4188C77-7FEC-4C5D-A2AA-8B173A788050","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"321dfc3b4c9c7651a8484ba5234ad14e8d589acb","datavalue":{"value":{"entity-type":"item","numeric-id":3179308,"id":"Q3179308"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"48962e9be52aec321f7bf85f3ce5ea0fa8ebb732","datavalue":{"value":{"amount":"+0.8196820020675659","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":"Q4633544$E503F144-A1CF-4486-9272-579D621CDC40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5d4009fbf74228d50438a3bfacb9dc9b9fa992e6","datavalue":{"value":{"entity-type":"item","numeric-id":2164251,"id":"Q2164251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"36555023f1390c27b3d1b9c581a91953d60004d4","datavalue":{"value":{"amount":"+0.8170410394668579","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":"Q4633544$BBA08256-1A98-476E-82DD-B4455B256948","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4f24451847ad4eb0ec48494a5ae1d33727204ae0","datavalue":{"value":{"entity-type":"item","numeric-id":5408433,"id":"Q5408433"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a34ab27a79a80a07879a4ddbdd5f779facaa775b","datavalue":{"value":{"amount":"+0.8159435987472534","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":"Q4633544$5C22EA0C-0D4F-4F0E-8F0A-6C26A9B8EE63","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Satisfiability modulo heap-based programs","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Satisfiability_modulo_heap-based_programs"}}}}}