{"entities":{"Q2128808":{"pageid":2139551,"ns":120,"title":"Item:Q2128808","lastrevid":54302039,"modified":"2026-01-26T14:44:55Z","type":"item","id":"Q2128808","labels":{"en":{"language":"en","value":"A heuristic prover for elementary analysis in \\textit{Theorema}"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7511931"}},"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":"Q2128808$1F54D03A-F7D7-4D52-B48C-082620D72674","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b4381edd57ca98f2278dd5c0a9c3b74597388de5","datavalue":{"value":{"text":"A heuristic prover for elementary analysis in \\textit{Theorema}","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2128808$270B70B8-4C03-4DA3-85AC-D50F98433494","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9297a09b317d6c10c564b0a8f9b6089c50c879b5","datavalue":{"value":"1485.68284","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2128808$9EC4DD8C-3C66-40C8-B851-F90315EB93B3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"71d539a191bcf2541f55bc4ffe390ac5067e7377","datavalue":{"value":"10.1007/978-3-030-81097-9_10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2128808$6DB8DE34-D9ED-4D3C-BB52-2CE242C9A189","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"725aca679a0cd849b7123b8f0d65ff45506c8d40","datavalue":{"value":{"entity-type":"item","numeric-id":485836,"id":"Q485836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128808$441A5604-57FC-47E1-B475-2952A9511991","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6a2d220bbda83e730799716cad61153265e68ffa","datavalue":{"value":{"time":"+2022-04-22T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2128808$0C1E6E23-A260-4CE2-B4CE-6B11C077451A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2128808$F21FFA63-F5D4-47C6-B893-4744C41E2101","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fa1e8cb16271b7fcb955a4738a38222debdb9651","datavalue":{"value":"26-01","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2128808$067C5A35-C595-44AE-8D3F-D9A474B2386B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2128808$CD13981B-A0F0-4B3B-8B78-DA6025FEDCB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6be78f1bad1f2f19058dbde65eb124c0430a7d27","datavalue":{"value":"68W30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2128808$B3C1C56F-AC33-4477-A66F-D30ABA38E2C9","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8454dd1d009ad361e90824262a4cca683cf56b38","datavalue":{"value":"7511931","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2128808$FB90F91C-7A02-4D36-B0CE-B6318FA0B8B9","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2f8be496afa70f96c42c9d007ca2434d452e47a9","datavalue":{"value":"satisfiability checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q2128808$ECB71887-B2FE-469F-B9B4-C1D07914245B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cd4271c3d48c8fdcc6d52f39d7f84534e5a51082","datavalue":{"value":"natural-style proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q2128808$3605422D-62E6-4288-A378-BA595568BE5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"25a0d0a64145a26d41eb5308b1cb512dc20d7b36","datavalue":{"value":"computer algebra","type":"string"},"datatype":"string"},"type":"statement","id":"Q2128808$2D5AB1CC-046A-4195-94CA-DDF586651155","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0e36fd2915ee69146bd208b73e1714d6ba9054ec","datavalue":{"value":"symbolic computation","type":"string"},"datatype":"string"},"type":"statement","id":"Q2128808$E5D12BB8-2080-461F-A3E7-9C560003C8E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1254a7c01d2970b87da2854c1fde40c268a1f55d","datavalue":{"value":"satisfiability modulo theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q2128808$E213305D-0792-4987-847D-17E21D6E0C6A","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"261ae6dfeffd96c9ea238e124055221c78337064","datavalue":{"value":{"entity-type":"item","numeric-id":13705,"id":"Q13705"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128808$E824E588-2028-4AA1-855A-A8A0FF2C950E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"29391b19386946f3f8609d95651483db905027b9","datavalue":{"value":{"entity-type":"item","numeric-id":22439,"id":"Q22439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128808$D0DF0709-E082-4296-9C24-39D52DCA760A","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":"Q2128808$657D942B-C32D-446D-9167-F483D3A095CD","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"1bb1b0ade20c1a82e83ba37960ac0ebe339c42cc","datavalue":{"value":"https://doi.org/10.1007/978-3-030-81097-9_10","type":"string"},"datatype":"url"},"type":"statement","id":"Q2128808$5E97FC1B-A535-4F92-9EA8-4AE8DDEE9159","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ae9607b3f8006f0c1e6935f3c8cbd601570c5278","datavalue":{"value":"W3174333326","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2128808$A9043553-77C0-498B-95E1-A8451D8875B6","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"c43a14224fa5235de73a12a4a92053be887ea6ac","datavalue":{"value":{"entity-type":"item","numeric-id":1272608,"id":"Q1272608"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128808$76E8A83D-C6E3-4DE5-8E82-0CB8185879DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fbf2e2915ee525715586105eb9b7b6f7c6c8c666","datavalue":{"value":{"entity-type":"item","numeric-id":5195272,"id":"Q5195272"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128808$EAA106A1-66DF-4EBB-8426-40CCF45C9A54","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":"Q2128808$235AE861-EA9B-4C8C-817A-D9635B0E1A3B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c9883251bac30014da6efa368ef0207731c291b","datavalue":{"value":{"entity-type":"item","numeric-id":1025313,"id":"Q1025313"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128808$76BDCEA2-44C4-497D-8546-F411FAE49708","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a1fd130076346dbcdd56e42c98ce6844fd99547e","datavalue":{"value":{"entity-type":"item","numeric-id":1025313,"id":"Q1025313"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aa7daf8309464a553ec4e954ae4f3f0119cde150","datavalue":{"value":{"amount":"+0.7974970936775208","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":"Q2128808$F9A3DBFF-A776-41E5-BA04-8F93EF262B35","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f627f49c922ef0fd9cfc1d9cc57f7fea34ba48fa","datavalue":{"value":{"entity-type":"item","numeric-id":4459895,"id":"Q4459895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2ff9f28abc3e5facd770e1a220cf9c8c2cbe8d64","datavalue":{"value":{"amount":"+0.7879030108451843","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":"Q2128808$F5E36158-1E1F-484B-8001-D174A09CD166","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2bdd64fcbb948fd199cb840bfe49fd1731c1cc5c","datavalue":{"value":{"entity-type":"item","numeric-id":1272608,"id":"Q1272608"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3150400c3736851f32eba121d67debd4c77bca3e","datavalue":{"value":{"amount":"+0.773725688457489","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":"Q2128808$F7CE2B3B-F5B5-4DE9-98C2-C6AD1066789E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b360687fbb91abbd8b131ebd7a12117c200994da","datavalue":{"value":{"entity-type":"item","numeric-id":5505501,"id":"Q5505501"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b49682f877b74593f19f291779897c0cf63f0d67","datavalue":{"value":{"amount":"+0.7722315788269043","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":"Q2128808$4AE288ED-E9AB-43C6-B802-B558A1CA1D38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f9b4fb64992fb8ab53efeada2bcba4b18cfaafdb","datavalue":{"value":{"entity-type":"item","numeric-id":972422,"id":"Q972422"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"73a811f664e39ee7896cdc6a78876814aa3530e1","datavalue":{"value":{"amount":"+0.7692602872848511","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":"Q2128808$693EA80B-9E0D-4CEB-A832-8498CA126F80","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2128808","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2128808"}}}}}