{"entities":{"Q6957141":{"pageid":21246372,"ns":120,"title":"Item:Q6957141","lastrevid":84072539,"modified":"2026-05-09T09:38:53Z","type":"item","id":"Q6957141","labels":{"en":{"language":"en","value":"The QSMA algorithm for quantifiers in SMT"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8065837"}},"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":"Q6957141$70CA9649-A5AA-4D8A-A906-894AC6B37F3E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cf7e87af687c437d62c4790ccb7b2475429c6ed9","datavalue":{"value":{"text":"The QSMA algorithm for quantifiers in SMT","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6957141$BC27C3D6-159A-4A50-9C00-0AC6D02B682C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"01a48b1b7d45dd50ed28b160f98e938322721ca9","datavalue":{"value":"1569.68097","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6957141$2822C696-0069-451B-B3FA-851CD5F6AB06","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"34b620f780e7966da22e72bd17eaef80dade0566","datavalue":{"value":"10.1007/S10817-025-09727-8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6957141$7BCA9AAB-C153-41D4-ADE9-97755FCBE806","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b455290f5b835c3773a6eb2262897ac70e7a163b","datavalue":{"value":{"entity-type":"item","numeric-id":287273,"id":"Q287273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$D403CEBE-DEF7-4AF4-A1FC-114F05536DCB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a6be8d909a46685b6a24cecd253b3dd33cd2a6cb","datavalue":{"value":{"entity-type":"item","numeric-id":832718,"id":"Q832718"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$7AC1A600-A3B6-4EE9-AF66-2E9715FB8549","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ff3e9206bbbe5042a5d33d0c7ec71b4324fa2a97","datavalue":{"value":{"entity-type":"item","numeric-id":6492730,"id":"Q6492730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$E11351D4-0EE8-47BC-A620-882FE4356B1D","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$0ECC5AB4-70FF-4DEF-B87F-80E135E73291","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"efad754626f161cd66c554302db22bd9c4d46e2c","datavalue":{"value":{"time":"+2025-07-16T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6957141$2DAC53CE-8285-4D1B-BD55-1E365C189A3C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7083a5d146d78edf9fc7469a5d9b0c104122f1b7","datavalue":{"value":"68R07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6957141$51A8C3D5-C9D2-457F-920F-048FBEF694F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c15287dbb142f8dc10ab92a91b8457ac3c169cd3","datavalue":{"value":"03F30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6957141$0E2E153E-349F-4621-A8D1-8B3A8FA1FCB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6957141$2DF1F2C8-0980-4564-AADD-AACCC9225400","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"11eb8bc97cd68a25a3209f8d921a8fb8d87fbbb9","datavalue":{"value":"8065837","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6957141$CD3E12C4-8E26-4C43-A8D8-A441B4609DA2","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$8DDE52C6-A5EF-4226-91CA-5479C15D70A6","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ac8daf9b2a0058692665d0c45ec7b53d7ff6b82e","datavalue":{"value":"satisfiability modulo theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q6957141$FBF06D31-C82E-4471-BAC7-C7453616C0D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4b395e8f6acd180e1625664cf0f73ca38f664e9d","datavalue":{"value":"satisfiability modulo assignment","type":"string"},"datatype":"string"},"type":"statement","id":"Q6957141$A10D050A-6EB4-40A7-9AB2-6CD1FD353D25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09fac802f13dc4cbe78b2d293cbba412de4b80d6","datavalue":{"value":"quantified satisfiability","type":"string"},"datatype":"string"},"type":"statement","id":"Q6957141$9EBD552C-DDE7-4A8F-90C1-DC9BF02C7255","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5af7b8c7e3b06f94bf95b0151705740e4ea5f853","datavalue":{"value":"automated reasoning in arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q6957141$FBBD2599-51C4-4F7A-ACD9-84AF53908D8C","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":"Q6957141$C6FD53E2-58B1-45D9-9669-1A23479067E6","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"f49cdde0e4e93beb3ec22ebb07bdb6ff64fe9a7c","datavalue":{"value":{"entity-type":"item","numeric-id":3655193,"id":"Q3655193"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$6D69BA71-AB54-4284-92E3-4C221A4D9963","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4df9e36bc833a6259fe4525e20648c4deed4f643","datavalue":{"value":{"entity-type":"item","numeric-id":4928427,"id":"Q4928427"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$897031F0-AF7E-4A22-B711-6E3E3144285B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0ccddffba771795151957f5712724106bbb0cab2","datavalue":{"value":{"entity-type":"item","numeric-id":1707598,"id":"Q1707598"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$AA8F771A-FB21-42F7-AF6E-41917381ED6C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d645e2b876ab109a4fadcb1ed7f0c554bc73185c","datavalue":{"value":{"entity-type":"item","numeric-id":2303254,"id":"Q2303254"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$A26B6270-6461-40E0-B067-5A16C7F5CBA6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3abb1020d45fa27ad50fa120d6a14f8aaf93020e","datavalue":{"value":{"entity-type":"item","numeric-id":832719,"id":"Q832719"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$6F08D5CE-F16E-4F18-A92D-B343AE1E0244","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"286458fd3ded729595cf517c5ce50298b378a890","datavalue":{"value":{"entity-type":"item","numeric-id":6492731,"id":"Q6492731"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$EE77F1E9-EFE1-4920-838A-58F90D0E2858","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f85fd02f887f9e6cdc6efa73686f469882f2acf7","datavalue":{"value":{"entity-type":"item","numeric-id":438533,"id":"Q438533"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$71978C0E-EAAC-4C98-93DB-EAF869F7340E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"64edbd4b0368a46cc24983dcdc802e4982142495","datavalue":{"value":{"entity-type":"item","numeric-id":5310200,"id":"Q5310200"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$3B2DA2BB-D958-409E-9F0A-A176DFAB8CF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec2601a05a1e709fca09151d43fc2b61e821dace","datavalue":{"value":{"entity-type":"item","numeric-id":1355986,"id":"Q1355986"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$74E1B805-8946-4202-91BE-198CFF1B3CD2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c4d7798eba50e0ffe1e4306d4a4aa338f6be7be4","datavalue":{"value":{"entity-type":"item","numeric-id":4079605,"id":"Q4079605"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$2A40FB9A-C047-4BB3-A6BD-37C6168B2ACA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b4f714dbb33bba32b50777c1d77c1cb7ff5fe56","datavalue":{"value":{"entity-type":"item","numeric-id":3608773,"id":"Q3608773"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$F0139545-CB79-41C7-9877-DF8F3BDC9B6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"46b48d71d3c521c2ab242461308274d7f131a2c9","datavalue":{"value":{"entity-type":"item","numeric-id":5747779,"id":"Q5747779"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$A9C9C937-EAD6-497D-AF83-8BD362823BFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7ddeddf292e13fd796c5c20e153357856b636f89","datavalue":{"value":{"entity-type":"item","numeric-id":2926635,"id":"Q2926635"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$41C47899-0A63-4005-8DF8-B613AFC5F479","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1daf6c1b27d4e2241acccb436e068cfc4f24ffff","datavalue":{"value":{"entity-type":"item","numeric-id":3546294,"id":"Q3546294"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$BB53266C-5D56-495A-865B-F9788CF0D122","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f426d61b5e73f09c762af22502a76e1d6d446b2d","datavalue":{"value":{"entity-type":"item","numeric-id":3636870,"id":"Q3636870"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$6EF3D91D-EEB7-424C-AD57-3BA0B1484FEA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1d425524c539f34b2c20b8cfec23a758c1eb81a6","datavalue":{"value":{"entity-type":"item","numeric-id":3608772,"id":"Q3608772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$EEF5BD01-E01B-432E-9678-0E56D94FCF2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1ef8a8532db5854f5d22fa31dcae929508b22146","datavalue":{"value":{"entity-type":"item","numeric-id":2096440,"id":"Q2096440"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$7682B28C-C8B7-450B-9961-B17E0C5ACBD4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d77121ca06023666fb3b31fe1611bc7b34ff56df","datavalue":{"value":{"entity-type":"item","numeric-id":2908506,"id":"Q2908506"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$DBB77BD6-DEE2-4AC3-B1AD-C1317CD8A793","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bc7fd1c06b6b3c0329e20dceff33f96926c84dbd","datavalue":{"value":{"entity-type":"item","numeric-id":832268,"id":"Q832268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$521468A6-D40C-4D8D-9D20-C6230AAF1C75","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f1060c39f6c78c6c906f6922c72b026efa0999e0","datavalue":{"value":{"entity-type":"item","numeric-id":518396,"id":"Q518396"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$7F53179B-7410-4D3F-A683-9629BE8D2CCD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"817ee4f5358d83048f7143c1c798ef96590ad2ef","datavalue":{"value":{"entity-type":"item","numeric-id":3608415,"id":"Q3608415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$42392096-E63B-4705-963B-1B4D0005E4B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"76f085e060cc02117b4ec73931c77617da801d17","datavalue":{"value":{"entity-type":"item","numeric-id":2473386,"id":"Q2473386"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$18CF4B4B-EC29-4CD5-846A-0FCB7E17CA1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0bbe72cc116925a801c6363ae53a473520b6daad","datavalue":{"value":{"entity-type":"item","numeric-id":688575,"id":"Q688575"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$8AB1E1FC-FB45-4670-9728-2C24552DC5E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f33ee1e9bddd5e600f5b1d8c8cfae347a7631b92","datavalue":{"value":{"entity-type":"item","numeric-id":3140556,"id":"Q3140556"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$4ABCCE85-391D-4BB9-AABB-25564B42060C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a6d3461230a65825b317043f52f4641daf8389e1","datavalue":{"value":{"entity-type":"item","numeric-id":1799131,"id":"Q1799131"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$7B5166AB-8B00-419B-B6D2-765E7E6CCF52","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"490c323d20b25705645788916701d4577fbf06c1","datavalue":{"value":{"entity-type":"item","numeric-id":6940547,"id":"Q6940547"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$8DDD5A71-ED2C-4274-8C48-35B783C18D79","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"011fd911330c176d4f644d0d384d2eb0c583ecf8","datavalue":{"value":{"entity-type":"item","numeric-id":6039405,"id":"Q6039405"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$78917496-27D3-4C1F-B182-39C66882DE65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b45eae4be6d7ffbeeaf6fa13772378783aa42ea1","datavalue":{"value":{"entity-type":"item","numeric-id":2233503,"id":"Q2233503"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$D74FA8D3-340F-42DA-AC82-09B655DB81C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"836a1d7b6bdb48a4904f72118ea93610f12fe959","datavalue":{"value":{"entity-type":"item","numeric-id":707743,"id":"Q707743"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$88A6310C-FD95-475E-927C-15B55BF053E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"516924fffc5ccd06ddf357b776bed9baac4d2e69","datavalue":{"value":{"entity-type":"item","numeric-id":2324227,"id":"Q2324227"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$93F081FD-A0FC-4D2D-A0D2-738B6F0D7050","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5d3f5b196c0df4a4076dad9269fa5296f4cdaaab","datavalue":{"value":{"entity-type":"item","numeric-id":1688537,"id":"Q1688537"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$1000F71A-539E-4143-A9A7-167AFDEEA939","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"197bd6d0b9b13f7d7d62b39ca988dbf1f2dfc0db","datavalue":{"value":{"entity-type":"item","numeric-id":4928453,"id":"Q4928453"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$8FBE386F-1AB7-4EA8-8A2D-4FBE048266DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e7cfea5fcebfb4162710425692e427cbf2157a8f","datavalue":{"value":{"entity-type":"item","numeric-id":1103602,"id":"Q1103602"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$57854135-B614-4373-B237-AF5A36147648","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"add4491e8fd66ac82b780ec4494c2c2d28510122","datavalue":{"value":{"entity-type":"item","numeric-id":677553,"id":"Q677553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957141$202D1DD4-25BE-4326-BB1C-54E4113FB53E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The QSMA algorithm for quantifiers in SMT","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_QSMA_algorithm_for_quantifiers_in_SMT"}}}}}