{"entities":{"Q4928453":{"pageid":6958035,"ns":120,"title":"Item:Q4928453","lastrevid":51744743,"modified":"2026-01-19T19:37:27Z","type":"item","id":"Q4928453","labels":{"en":{"language":"en","value":"Quantifier instantiation techniques for finite model finding in SMT"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6176222"}},"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":"Q4928453$D457255F-4E6E-406B-BA3A-22BB28CE383D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2b981b55245dd3d1c6f840c6e288bc5021f77c06","datavalue":{"value":{"text":"Quantifier Instantiation Techniques for Finite Model Finding in SMT","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4928453$E79D9569-B401-4734-9F86-7FF964DAD4A4","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"515675e3d7bd89dab0e6489b6ce8c7261936bae2","datavalue":{"value":"1381.68275","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4928453$17CBE8A2-D272-4A90-8048-49E2304CB3BE","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f57b27e751adac03513ec5d9ee4d08ae3f20747d","datavalue":{"value":"10.1007/978-3-642-38574-2_26","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4928453$DBFB7CDA-870C-416B-B3CF-5E93ECFAC7D1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"84952d23570c02a49b2cbd6b6731071617699380","datavalue":{"value":{"entity-type":"item","numeric-id":518398,"id":"Q518398"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4928453$A3D00D54-94C1-491F-81C9-C1857B168AC1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"947e5398223830d4c80e75386dbd3c8e6dd67f1d","datavalue":{"value":{"entity-type":"item","numeric-id":429585,"id":"Q429585"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4928453$E160471B-3770-44B8-975E-6A53D3F35209","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ded5d73a1c3090755c930487a8f09176d403299b","datavalue":{"value":{"entity-type":"item","numeric-id":2881072,"id":"Q2881072"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4928453$77BDB81E-2AE7-4295-9C07-0289593E10C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4553da8c1048cfe4c8999aaeff5b09130cfe2ff7","datavalue":{"value":{"entity-type":"item","numeric-id":1064406,"id":"Q1064406"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4928453$BA7F8DF6-48C1-4659-AA8A-FA9D1967D03A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5374aaae6c4fa00723de88e8acb31ca46f3aaf1e","datavalue":{"value":{"entity-type":"item","numeric-id":518401,"id":"Q518401"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4928453$AA693007-CB34-4293-B7D6-C02D657E7AFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ad77f9f95b13763d1bf3e18f3ef5b6900b795f74","datavalue":{"value":{"entity-type":"item","numeric-id":518400,"id":"Q518400"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4928453$B5D1E027-AD9A-47FE-8414-1312BF367EEB","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"feba868a8cb9ecfadec66d8e8a91d447de952529","datavalue":{"value":{"entity-type":"item","numeric-id":4928424,"id":"Q4928424"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4928453$7ECB9405-8F6F-4F05-85D5-2C9CA4AD1710","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b84d2a34981f1c1a0d0fb543ea5aabc14a21194b","datavalue":{"value":{"time":"+2013-06-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4928453$21C0C5B3-C35B-4AB4-8A3C-B9FD3B2523C4","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4928453$66B54BFD-3F53-4F32-A51F-61D649AEE73F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a1ed9a0090c010e6029ab277d3dd7acf952a1a3c","datavalue":{"value":"6176222","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4928453$00765A0D-B9D4-4095-A035-33FA2F21C51C","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"83e2dec25ea583652d0e07d4393a843812f4b48b","datavalue":{"value":{"entity-type":"item","numeric-id":21686,"id":"Q21686"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4928453$C63CC3CE-035D-44FF-9F1E-42F03F10A533","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":"Q4928453$005E95FD-1CA0-4E83-BEFF-3B404C3105B5","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b5fe655b3c9f87115d6305bb299f38581311f4eb","datavalue":{"value":"https://doi.org/10.1007/978-3-642-38574-2_26","type":"string"},"datatype":"url"},"type":"statement","id":"Q4928453$7EC52DC7-BF5E-4262-97EF-9C8ACDABC7BA","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"230756b5da6572c771e8d7ff26ccadccd0b31e52","datavalue":{"value":"W2098095758","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4928453$1112C920-861E-496A-9241-06B75C921C3C","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a321b69eb32f47eec245538b125547d32b51872d","datavalue":{"value":{"entity-type":"item","numeric-id":4593094,"id":"Q4593094"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0685421314783dafe8e3400e94f17448bfeba9e1","datavalue":{"value":{"amount":"+0.879065215587616","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":"Q4928453$9912A6A7-FBF1-47AE-AA2B-0D941AEB8234","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"709211d935c435620f867d257bf161ec3a85cbd6","datavalue":{"value":{"entity-type":"item","numeric-id":3636870,"id":"Q3636870"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5eaee24832e7637cddde3e6884a88e415bbe3f42","datavalue":{"value":{"amount":"+0.8171815872192383","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":"Q4928453$EA95FE16-8CE6-4D26-8318-43F285CA1170","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"42cace2ddf6019b7cd2939e3da583d3a9bc71c2a","datavalue":{"value":{"entity-type":"item","numeric-id":2233503,"id":"Q2233503"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ceda7c6ada84a1c5ec770044020052c54e99b6b1","datavalue":{"value":{"amount":"+0.7904064059257507","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":"Q4928453$95807A70-52B4-4227-932E-CCD4CA003328","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"12aaa4a36bdf05dc06c575e9e83887fbf42b685d","datavalue":{"value":{"entity-type":"item","numeric-id":1037401,"id":"Q1037401"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"088bc0b4e93c8a209cb05a21dbd66f9c34153f21","datavalue":{"value":{"amount":"+0.7891303896903992","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":"Q4928453$C1A85573-010A-4C3D-89C0-1DCB9D515B7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9390b4ccc6dc9f08d9ed8cd2d7f1eed1c352e9ee","datavalue":{"value":{"entity-type":"item","numeric-id":3608772,"id":"Q3608772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"74a2bcfd6a5ea4047264ff277730047943c562ad","datavalue":{"value":{"amount":"+0.7797126173973083","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":"Q4928453$4580F0D0-D444-4B67-A592-DD9A6C7CD3B1","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4928453","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4928453"}}}}}