{"entities":{"Q7009616":{"pageid":21560643,"ns":120,"title":"Item:Q7009616","lastrevid":81799445,"modified":"2026-05-06T19:23:02Z","type":"item","id":"Q7009616","labels":{"en":{"language":"en","value":"Satisfiability of non-linear transcendental arithmetic as a certificate search problem"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8014343"}},"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":"Q7009616$99D9764D-865A-4655-B29D-EC030F985998","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"334fe676fe04db39e25cd9b98af462444aeb844d","datavalue":{"value":{"text":"Satisfiability of non-linear transcendental arithmetic as a certificate search problem","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7009616$5A6E9F24-7E6F-4997-84DD-CD3989EF8AC4","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"763d8bdf6ee8e93fa35272bdfa36b695c4d3b491","datavalue":{"value":"1557.68279","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7009616$9726FD32-0B7C-4BD6-AA79-652A1572B726","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"79e24bc57fa3c8c1fc0402423c99e1f05aee5d75","datavalue":{"value":"10.1007/S10817-024-09716-3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7009616$2F10DAE7-BD76-4435-83CA-40B75ACD55E8","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"3a059c4a96f66f9dd4b4953d0276d1e1cfa90099","datavalue":{"value":{"entity-type":"item","numeric-id":4669553,"id":"Q4669553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$0DB0A1BF-52DE-4AF7-B451-BF277FEFAD1D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e504e5c78f160847d88d111e5ab65b0189aa771b","datavalue":{"value":{"entity-type":"item","numeric-id":389833,"id":"Q389833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$6BCE1105-0327-4FEE-ACFA-0AC2182F872B","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":"Q7009616$7D039AE5-495C-421B-964E-1C669E22145F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b6225fd2364f70e5643f17f5e8341bc2d63828c3","datavalue":{"value":{"time":"+2025-03-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7009616$5840DC2F-D459-46F3-8C33-3A557F5EFCAC","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7009616$0357F7BF-B195-4D76-AB80-7BD3D1705EF4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c15287dbb142f8dc10ab92a91b8457ac3c169cd3","datavalue":{"value":"03F30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7009616$3D135DDD-23AF-4788-822B-1589A2092D9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7083a5d146d78edf9fc7469a5d9b0c104122f1b7","datavalue":{"value":"68R07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7009616$2A9C72F9-CCAA-42E0-92D3-E8FF8DAC99D0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c56ba3da4c6d8928da922297b2dc2b89d3e34823","datavalue":{"value":"8014343","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7009616$EEDC1D98-2CC5-4953-957B-272A1DE1B866","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1254a7c01d2970b87da2854c1fde40c268a1f55d","datavalue":{"value":"satisfiability modulo theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q7009616$67F135B4-CB18-4361-B386-6C33764214AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"56c71e46e79e03ad250b01addd277681d4c615b8","datavalue":{"value":"nonlinear arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q7009616$EEDBF1E8-FAE7-41F2-AD05-7B3E09BE8AE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"819f137f9ec626acba1c8947981be8a93c7821b2","datavalue":{"value":"transcendental functions","type":"string"},"datatype":"string"},"type":"statement","id":"Q7009616$4397F499-C10D-4518-82B0-AE0727DFEF4B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dc37cf6bf1a4fd159f089028e999146e64828fa8","datavalue":{"value":"SMT","type":"string"},"datatype":"string"},"type":"statement","id":"Q7009616$AFDD6EE5-3E64-4568-A827-0F2AD8DE04A6","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":"Q7009616$D611B5A2-6FB5-4818-84E1-76EABC3C796F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"72afa48bd8e77d60f453be92d91a6c676802e66a","datavalue":{"value":{"entity-type":"item","numeric-id":4286593,"id":"Q4286593"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$192BBF9E-4376-4DC0-9390-F056598A020B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4d6bee919d9860de31a702e017a2aa9a95712c01","datavalue":{"value":{"entity-type":"item","numeric-id":2988924,"id":"Q2988924"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$D26573C8-8473-4A73-99F5-D1B309BDCC57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8bbbd10679bf2d321eb9db870479cc35412cbd39","datavalue":{"value":{"entity-type":"item","numeric-id":2104495,"id":"Q2104495"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$99A6BAEF-E01E-4760-826A-408D6DA5B138","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e3739ac44abb460105202790eedea0be872db3e8","datavalue":{"value":{"entity-type":"item","numeric-id":2055849,"id":"Q2055849"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$53D2F89A-A46A-4709-A0D0-A516349184F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c37a1c8b88708c88b02062d0ea7c0a225dd37183","datavalue":{"value":{"entity-type":"item","numeric-id":6051116,"id":"Q6051116"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$52E5BCBD-A473-41ED-AB60-923EE7ADA6A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1463fb59243822ee50e8b000f17420f0fb220a92","datavalue":{"value":{"entity-type":"item","numeric-id":6060361,"id":"Q6060361"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$4FAE9C02-BD40-4620-8AA3-21FA10B24625","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c70aad961f1be1a86a7918b2020f0d8bacb9485c","datavalue":{"value":{"entity-type":"item","numeric-id":7033563,"id":"Q7033563"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$E5B43C37-2165-4EC2-A422-0698AADC8914","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f1645d5977fcbb346c223f2e9f46edf7dc223d58","datavalue":{"value":{"entity-type":"item","numeric-id":4691738,"id":"Q4691738"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$BAAB9F4A-24CF-412C-97D6-E31085D0EA97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"21640ae8e3aa02debe92970cf2184aca918b76e5","datavalue":{"value":{"entity-type":"item","numeric-id":5326318,"id":"Q5326318"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$46712CFB-B4AF-4AC3-935C-A5BDF0446495","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a879cfa141ad3da064e20f842a679c89bd178630","datavalue":{"value":{"entity-type":"item","numeric-id":5146711,"id":"Q5146711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$C55611BC-1E3D-406B-8EB5-F4F3F3339079","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0159a4b3aa51796bf4157bb1c7d881e6f3f73b6d","datavalue":{"value":{"entity-type":"item","numeric-id":3266931,"id":"Q3266931"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$CA8AE7AC-1BD3-449B-9551-6AA861D5C5A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec87712847861422b1aef654edc4d7833b96c15e","datavalue":{"value":{"entity-type":"item","numeric-id":4838489,"id":"Q4838489"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$346A4DC2-C0FE-40AD-A2A4-3CABA114E659","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"86ebc91ea47a62722ea14f3394d1e9f0b20811f0","datavalue":{"value":{"entity-type":"item","numeric-id":1616393,"id":"Q1616393"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$E26BAA7D-6987-4AC8-A95B-34717C210DD5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6af018d397324baf161d5438de87facfdd8bd841","datavalue":{"value":{"entity-type":"item","numeric-id":5179223,"id":"Q5179223"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$BBDED808-741F-46A4-9181-572ED765AB53","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a8a8f99954904936038bef6402f3271c39799f3b","datavalue":{"value":{"entity-type":"item","numeric-id":2013319,"id":"Q2013319"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$FFC03B77-338B-4068-8A34-94B3364DCB23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"065a2d65834e8c8b57bdda41356587a32ad9b5c2","datavalue":{"value":{"entity-type":"item","numeric-id":5457277,"id":"Q5457277"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$0088824A-7D41-4A06-855C-AD95B0D0E982","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fe33bf4e1ec51f59c09f65752ea810761eb09a2a","datavalue":{"value":{"entity-type":"item","numeric-id":4928439,"id":"Q4928439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$1DD7E86D-9759-4B3D-B44C-7E274A093DDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"299c95531b5545caf6e3aadb2249a8295f13d08e","datavalue":{"value":{"entity-type":"item","numeric-id":2611401,"id":"Q2611401"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$2F8D9DBE-3BCE-4AC5-8E0F-406383B64727","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"987d5fe9e1eb7279bb9d67d0f9ef48946c41eade","datavalue":{"value":{"entity-type":"item","numeric-id":4004279,"id":"Q4004279"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$F4A5E804-D102-44ED-8E27-898E11A5F9EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"388a01e13473028a5ca30742411493f89ef8aed9","datavalue":{"value":{"entity-type":"item","numeric-id":2409014,"id":"Q2409014"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$3BB74882-C8A6-4B85-829C-B5844D2108C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8124c3a50d02ba56d5b1c0a60b8e8afe2f2a0610","datavalue":{"value":{"entity-type":"item","numeric-id":1290652,"id":"Q1290652"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$A59A9292-915C-4759-BF22-6E61747FF8EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b2135c983cdc46a7b95f3c11b796f8a79cc1e900","datavalue":{"value":{"entity-type":"item","numeric-id":2104500,"id":"Q2104500"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$6F2B95BC-FEA1-4BCA-87CA-C2CB5E8A146D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"985abca8d2ebbaf4464431b93735d1600c57c040","datavalue":{"value":{"entity-type":"item","numeric-id":4492825,"id":"Q4492825"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$FC53007B-B1F7-4A3D-92FE-AF7C67E429A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f9ac1dec4c44e7022f565fd90e837a738b783d1d","datavalue":{"value":{"entity-type":"item","numeric-id":6160909,"id":"Q6160909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$4D012F65-3C16-4CFE-B239-EB40FB3C4267","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6adce5390824587493ef5be0cdc5c1106cfdba15","datavalue":{"value":{"entity-type":"item","numeric-id":1900758,"id":"Q1900758"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$AEBA6F4E-D824-487A-8717-D4A1919C4F50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c9284012cfeaa340d0f849c5b0590734822121e5","datavalue":{"value":{"entity-type":"item","numeric-id":654031,"id":"Q654031"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$DD6486B2-79FA-4432-B486-11530C0561B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fa917cd1e9b5468ee39ca98d36ef385b02222f9c","datavalue":{"value":{"entity-type":"item","numeric-id":465678,"id":"Q465678"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$7B90D72C-2995-40DF-BC62-4436B3080F63","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c8d59b594c48e47960c7d76364d47b2464e846c1","datavalue":{"value":{"entity-type":"item","numeric-id":4413072,"id":"Q4413072"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$DFC6F35F-5C92-4F54-B3B9-64EA916ED091","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f0a544f201c6283b7933810872cf2a33339cdad9","datavalue":{"value":{"entity-type":"item","numeric-id":3605131,"id":"Q3605131"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$BD4EA51F-3838-418A-9A6F-CECAD2B11EC1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7112ada929f036ed383ba1431c227c20e5871d7f","datavalue":{"value":{"entity-type":"item","numeric-id":3997321,"id":"Q3997321"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$E40ED932-193A-4144-AF22-989A0453BBDA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"26f37a5712688624b838b1c05d00b04b70157957","datavalue":{"value":{"entity-type":"item","numeric-id":5302142,"id":"Q5302142"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$DDB8B211-3712-4E68-B036-80E5E1B9B8BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e0f2f095592fee9bccdcd39aaced175033fa5871","datavalue":{"value":{"entity-type":"item","numeric-id":5200816,"id":"Q5200816"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$E6BCE4DD-02D2-4AE4-A3C2-10BEE45554D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a976ce4c7a386a3a13ef4d5a2de7aee52bbba8a9","datavalue":{"value":{"entity-type":"item","numeric-id":6647713,"id":"Q6647713"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$88805B57-60EB-4851-A43B-2E1522907541","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"abf8d495c451508305cdb95eaf5ba926efab7bae","datavalue":{"value":{"entity-type":"item","numeric-id":5565112,"id":"Q5565112"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$FDDB863E-F80F-48E2-8DAB-A6640973D575","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"758d3724017c484fb2035201d7ba18e8ef7868f8","datavalue":{"value":{"entity-type":"item","numeric-id":2890535,"id":"Q2890535"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$6F54A6AA-892F-4BCE-8322-BE3B8ABAE811","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0c0eaf5fde452a9641bd98a14a4bcdd32f5f14c5","datavalue":{"value":{"entity-type":"item","numeric-id":2883838,"id":"Q2883838"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$24E560F1-B32B-4725-8179-41F1437BADF3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4dab43480854b8057429c5439f7df4bea88e20de","datavalue":{"value":{"entity-type":"item","numeric-id":765861,"id":"Q765861"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$3258A2F8-82DB-414A-9DAF-DB3333FA32F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b49f4f7d6b91784c37c6cc02d22520c86677ca2c","datavalue":{"value":{"entity-type":"item","numeric-id":1688535,"id":"Q1688535"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7009616$442721B9-76B4-4A2C-ADDC-F9A1F0FC68E5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Satisfiability of non-linear transcendental arithmetic as a certificate search problem","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Satisfiability_of_non-linear_transcendental_arithmetic_as_a_certificate_search_problem"}}}}}