{"entities":{"Q4553283":{"pageid":6582875,"ns":120,"title":"Item:Q4553283","lastrevid":58268562,"modified":"2026-04-04T12:17:06Z","type":"item","id":"Q4553283","labels":{"en":{"language":"en","value":"Reasoning with finite sets and cardinality constraints in SMT"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6970797"}},"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":"Q4553283$ACB01D97-9DC6-4FCC-8E4D-9D50852E09E1","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"fd315f30d48b5b0bd2e2ba65430b82a20308ab6d","datavalue":{"value":"1403.68044","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4553283$F593527C-BB54-43E8-8E38-93D28CCB8FD1","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"47bceb738babf0c702cc831c90941770c7769e81","datavalue":{"value":"10.23638/LMCS-14(4:12)2018","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4553283$7C625BC5-AB4F-41E3-8B38-18828FC623C3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b62294fb13e708c6a17a9b331a0fc305e71cac6e","datavalue":{"value":{"entity-type":"item","numeric-id":1702887,"id":"Q1702887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4553283$A00704E7-7C58-46F6-8879-8AC361A99E1C","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":"Q4553283$9898718B-8972-4EA4-9027-97B96BF779D9","rank":"normal"},{"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":"Q4553283$07887F50-A063-46AC-A3A3-09E0521AB5C1","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":"Q4553283$B3DF4689-1187-4550-8B96-5B7805C42A75","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ceb376c62d58da4cb190e228be8e352c77702c07","datavalue":{"value":{"time":"+2018-11-02T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4553283$BB42141E-0167-49BB-886B-CACF78143AA8","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4a21c6e861c54e47b86b887622acbb54587f1b7e","datavalue":{"value":"https://arxiv.org/abs/1702.06259","type":"string"},"datatype":"url"},"type":"statement","id":"Q4553283$018ADD26-AD38-4952-A20C-8B9E332B5AE5","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"14cf74de25853c940589b125137b792dfb2d092b","datavalue":{"value":"68P05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4553283$48F659FA-5417-47F4-B660-A6412C7ABB16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4553283$9E79CA56-38EC-4A0A-93F9-DDC89BB97FFA","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"cfea5996b9e58ab7e6419d309c7c66c5261255b7","datavalue":{"value":"6970797","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4553283$32C3D82D-CEF1-4397-B521-E9F17AEACBD2","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1254a7c01d2970b87da2854c1fde40c268a1f55d","datavalue":{"value":"satisfiability modulo theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q4553283$8903919F-DCA3-4D13-B5E4-21E8CEE5B2B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a3bdfaf50a859f5dcfd6c0d4cd8eb8dd602821d3","datavalue":{"value":"finite sets","type":"string"},"datatype":"string"},"type":"statement","id":"Q4553283$74032C2D-FCFF-4DF9-B449-A92658F51197","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dfd2ae52b3325778b0c72742b08c947a3c4a2c65","datavalue":{"value":"decision procedures","type":"string"},"datatype":"string"},"type":"statement","id":"Q4553283$B65C7877-4439-426E-BD52-98F06B9BA771","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bd3fa568ce44545ce1c1bded3c45ecc37b43b7c1","datavalue":{"value":{"entity-type":"item","numeric-id":21467,"id":"Q21467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4553283$2D7134B4-0B1C-4A20-8F29-1F429A95776A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f29f161a221c0bedeec97e9d4ad10664227f4777","datavalue":{"value":{"entity-type":"item","numeric-id":16290,"id":"Q16290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4553283$C4CDD2FC-9FEA-4C3C-8528-0F8EC11E04B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"94a83aebbff287adfc2566cf5a58d543fa9638cc","datavalue":{"value":{"entity-type":"item","numeric-id":21152,"id":"Q21152"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4553283$0CA2D6C2-0A05-400A-800C-E23E71B43731","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"08e2f8f314529fb129405223c9cc6200110ac621","datavalue":{"value":{"entity-type":"item","numeric-id":52027,"id":"Q52027"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4553283$45313B1E-A636-4116-ADD5-0D8CA2E4C3FD","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":"Q4553283$0FBB8ADE-D771-485E-BBF5-9471673F7BE0","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"c489a44b8440c4e2128f84b8b64802addfcb1214","datavalue":{"value":{"entity-type":"item","numeric-id":4436966,"id":"Q4436966"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4553283$5E5D3C7F-9E66-4FA4-ABA1-7E188FE20906","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b3bd3de13a789153ea19b03e71b46c89e1650765","datavalue":{"value":{"entity-type":"item","numeric-id":2817911,"id":"Q2817911"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4553283$10B988B8-AA8D-4129-B794-9E9ACA1DCEBF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"819a2535befb2a67f49ee5e43432525215be36de","datavalue":{"value":{"entity-type":"item","numeric-id":4702972,"id":"Q4702972"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4553283$8F6B8FB6-45A3-4D93-BE19-790EB4634D94","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"126e5dfacc7f9aed01f6e192710147ed8c12ae25","datavalue":{"value":{"entity-type":"item","numeric-id":2817912,"id":"Q2817912"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4553283$F639A810-F00A-4A0D-8B8B-3784BD1AB1E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"30fc41e0c653eca7fb41362868af006e5eedba26","datavalue":{"value":{"entity-type":"item","numeric-id":2405249,"id":"Q2405249"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4553283$4676E45A-D9DB-4176-A878-17564770B66D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6d711889aaffc4bc082cba5a43c703005d0d18e8","datavalue":{"value":{"entity-type":"item","numeric-id":3454111,"id":"Q3454111"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4553283$ABCADEC8-0204-4BD3-A2DF-007978B2EB51","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f2d7e80e7b46001318a974cf441bfa45393a1480","datavalue":{"value":{"entity-type":"item","numeric-id":2740887,"id":"Q2740887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4553283$EA2B61D4-E775-49A5-8264-A8FDF099F098","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ee26a945150fb6c6a0518145fd0cdbe9cb7a0b0f","datavalue":{"value":{"entity-type":"item","numeric-id":4633533,"id":"Q4633533"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4553283$08602F76-0107-4896-8E6E-5F4B42EB9052","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"caaa4b84c8d83da8bae05dbdfffe44e7c6e954fc","datavalue":{"value":{"entity-type":"item","numeric-id":4503906,"id":"Q4503906"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4553283$18206673-0BC0-412A-98FE-CFAE6C426B69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d28d1219e29c4a80580daac11ef44292c3abd11a","datavalue":{"value":{"entity-type":"item","numeric-id":4933320,"id":"Q4933320"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4553283$27BB5487-9BFE-494A-8343-F0DC098E3B06","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1e690a622a61afeb0c2a7c388c1cf18ef89252c9","datavalue":{"value":{"entity-type":"item","numeric-id":861705,"id":"Q861705"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4553283$1FAB6955-3A77-45CC-883A-3D15710DE919","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1278276176b213e20723f5199a3fe875c19d6492","datavalue":{"value":{"entity-type":"item","numeric-id":3608775,"id":"Q3608775"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4553283$FEF05440-B094-4143-95A6-B4627D84291C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"79db93a0bb311f56c816d6ffc92dd7b60e23250d","datavalue":{"value":{"entity-type":"item","numeric-id":3455223,"id":"Q3455223"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4553283$8AE09752-CC01-4723-B101-A7BC03D7266E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7cdca2c13e6565f2cdd29e0b7f5ce54fce0c0a91","datavalue":{"value":{"entity-type":"item","numeric-id":5452719,"id":"Q5452719"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4553283$E78548F1-28D2-48B2-9533-E9DD37DF1E2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"12f38f03c6887d40db0efe17b75e1585b8b3e72f","datavalue":{"value":{"entity-type":"item","numeric-id":3741005,"id":"Q3741005"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4553283$CF6F53C3-8924-404E-86B6-39EE79CE6B64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"041f425d2424dea3c24ef7c01081663e6200bc4b","datavalue":{"value":{"entity-type":"item","numeric-id":5191097,"id":"Q5191097"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4553283$2E05C5C3-0CD0-4770-94AB-397B31CDBFC1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0f6489cf91e9b20f63ed7456f579d1977e07a3f9","datavalue":{"value":{"entity-type":"item","numeric-id":3075499,"id":"Q3075499"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4553283$27BEFDFF-718D-4DDB-88B5-F1AF7B986DE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bb03578ceee8d5f3eded579265395839113bf7df","datavalue":{"value":{"entity-type":"item","numeric-id":4737128,"id":"Q4737128"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4553283$7748443F-F1E2-4405-83E6-E20D7E702191","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"672069c2f7bea0c7be6341747d1ed79c343b3501","datavalue":{"value":{"entity-type":"item","numeric-id":812443,"id":"Q812443"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4553283$4004E89A-658C-4226-B329-E6AFFE661F2B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"33c4d926d34826d7576df7e06528133bf05a7fa4","datavalue":{"value":{"entity-type":"item","numeric-id":2817912,"id":"Q2817912"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"33126c2045b364876371fc4eea53040008c15ec3","datavalue":{"value":{"amount":"+0.9583909511566162","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":"Q4553283$BBE33E9F-7491-4CA2-A5F8-2C523088FC7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"274867b6fcc7d562f7a72620b27d5cfc445805bb","datavalue":{"value":{"entity-type":"item","numeric-id":3075499,"id":"Q3075499"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"097792a68eeb51dddbd9feca4f1f0094ca5ed1f5","datavalue":{"value":{"amount":"+0.8265353441238403","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":"Q4553283$9FFF7FAB-14CF-48FF-B8B0-849973283C32","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ffe2f0ec13b86eac2dc68a5e7531ccddd55c8042","datavalue":{"value":{"entity-type":"item","numeric-id":879977,"id":"Q879977"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1e7382509e1509918a366ebcbc11539571943eea","datavalue":{"value":{"amount":"+0.808501124382019","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":"Q4553283$709A275A-E6B9-4E8C-8938-878CEFD961C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4a3d36386d25301994c9d8622beead935a6ca46c","datavalue":{"value":{"entity-type":"item","numeric-id":5758056,"id":"Q5758056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e04fb7dc28712f3bf9d02c5564d03b401331504b","datavalue":{"value":{"amount":"+0.7935131192207336","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":"Q4553283$FEA8FCDB-601E-402B-A802-D9EF6191C37E","rank":"normal"},{"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":"4d4155a6c86d4f3b25b7e05712ea8291dd5d1920","datavalue":{"value":{"amount":"+0.7858654856681824","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":"Q4553283$8B589EED-D8BA-435F-8676-9E5607D22C8B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4553283","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4553283"}}}}}