{"entities":{"Q529166":{"pageid":530933,"ns":120,"title":"Item:Q529166","lastrevid":57074931,"modified":"2026-03-26T12:21:47Z","type":"item","id":"Q529166","labels":{"en":{"language":"en","value":"Elementary recursive quantifier elimination based on Thom encoding and sign determination"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6720142"}},"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":"Q529166$0EE1BB13-DB60-4239-9ED0-5045DE449B4E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"33b7a8bb9f8103ee491c83d370e572201d426a8e","datavalue":{"value":{"text":"Elementary recursive quantifier elimination based on Thom encoding and sign determination","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q529166$E2CD60CE-705F-49A2-8D57-228172472EF4","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"dd3ff7202a1fdde38eac07792c8579908e6a44ee","datavalue":{"value":"1373.14060","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q529166$59319334-39CD-415D-98BA-7A4A00EE77D1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"01332ef92cb78f6115eabff5fb590a35e9bc5f40","datavalue":{"value":{"entity-type":"item","numeric-id":464734,"id":"Q464734"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q529166$F22D3498-760C-4ED7-86E9-C3654876E41E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f1a067da1377e19ad699e857de7d2607dce27ca2","datavalue":{"value":{"entity-type":"item","numeric-id":171409,"id":"Q171409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q529166$A2811EF0-41BE-4253-98B3-CE4FFB6F7801","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f91a4bcbc93435aed71775d25a4c5cd09e26f12d","datavalue":{"value":{"entity-type":"item","numeric-id":122505,"id":"Q122505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q529166$38EC7D7F-45D4-4D2B-A22E-0E3000BADC2C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"46a30028c10f94c4944c801c86f2de5dd37da0f3","datavalue":{"value":{"time":"+2017-05-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q529166$B804A7FC-578D-449B-A5B7-7DC3CA337E5E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ed024ebfa770e7020f9fa828845f86e393a3ff07","datavalue":{"value":"https://arxiv.org/abs/1609.02879","type":"string"},"datatype":"url"},"type":"statement","id":"Q529166$47FFB02D-000B-4392-9BCC-729649B05BA9","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"2bf2593695dd76acb238af68c2fd480df84da8b7","datavalue":{"value":"In the paper under review, the authors describe a new quantifier elimination algorithm for real closed fields based on Thom encoding and sign determination whose complexity is elementary recursive. What is important, the proof of its correctness is entirely based on algebra and does not involve the notion of connected components of semialgebraic sets: for all previously existing elementary recursive methods, the proofs of correctness of the algorithms had been based on geometric properties of semialgebraic sets. The development of algebraic proofs is very important in the field of constructive algebra. In particular, it is important to provide an elementary recursive algorithm for quantifier elimination over real closed fields, suitable for being formally checked by a proof assistant such as Coq.","type":"string"},"datatype":"string"},"type":"statement","id":"Q529166$D686D8FC-10F4-4CB6-8FF4-D3B27BF9BF5D","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"bc0b369bc69d1f4123fe4b071275caf5e5e87dce","datavalue":{"value":{"entity-type":"item","numeric-id":448394,"id":"Q448394"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q529166$BB1C5CF2-0230-4B7F-BAD8-481ED68E2B32","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"94a258fd6e09d2d582bb6c52c7992ac55d0da749","datavalue":{"value":"14P10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q529166$F3FFBF98-991D-4C83-BAD0-823C6C9CB293","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"176e47af9f9e7cf4ebff07fc1f9e4f94a83134c1","datavalue":{"value":"03C10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q529166$AD5A6CC5-318C-4A76-BF56-968A5D2C83BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"65ef089ab6dd31e83c3611c992a3cfd8973b58bb","datavalue":{"value":"14Q20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q529166$12841099-E48E-47F9-8134-F460031C10D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"299c2ceee90a97db4ef5b7d633c2a5784e0cb3c0","datavalue":{"value":"12D15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q529166$A3B32077-C8F0-4D34-AC9F-676D70CC7F5F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f598f73236fdb47dd00c692b3f8831193abe31ba","datavalue":{"value":"6720142","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q529166$6A3CEA31-7CE3-4996-9334-C068A0E97013","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7ce94254d44045733e962d2861c33d94e3725cca","datavalue":{"value":"quantifier elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q529166$79D98E5F-2153-4F84-AAF6-DAEC0204CC62","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"992be4a4c4949a4e050131a62745614d055174a7","datavalue":{"value":"real closed fields","type":"string"},"datatype":"string"},"type":"statement","id":"Q529166$FFED909F-AF82-4E00-B85D-46BC438221B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4f5229b2164efbeea7b5dfae02a4ca9815a7a20e","datavalue":{"value":"Thom encoding","type":"string"},"datatype":"string"},"type":"statement","id":"Q529166$FBA36711-07D2-4085-B91E-D49C1C6685DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7a10c873fa78bbf88a8147ae0268c5906643f66d","datavalue":{"value":"sign determination","type":"string"},"datatype":"string"},"type":"statement","id":"Q529166$6B8E7285-977E-4ED8-A55F-D576974D4F0C","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q529166$652715FD-2120-46A3-BDD9-8AED6F9A3F78","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":"Q529166$71721196-D927-4E0A-90E2-3B882FD3C130","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"bbd712e36be2dd8652b8e6adc28f09f6e53ad458","datavalue":{"value":"W2962899356","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q529166$16535143-DDF1-46D6-9E3D-9E09D63370EB","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"c8661438afabfc55e25d2d4bf6b19e2486427094","datavalue":{"value":{"entity-type":"item","numeric-id":4371694,"id":"Q4371694"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q529166$859D4B14-378F-4512-99D9-8C4AFCA495D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7fb1e069c9e4331b31c569dc8e2183f4c63cb5ba","datavalue":{"value":{"entity-type":"item","numeric-id":5920628,"id":"Q5920628"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q529166$313C190C-2BDA-461D-9E3B-6C066B9182A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3b35afcacf487f7d4833dfa5c8ec078202260d5c","datavalue":{"value":{"entity-type":"item","numeric-id":1096620,"id":"Q1096620"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q529166$5BE8539C-8228-4FFC-A566-D1A77E192144","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"33c7a78759148ce6b1abced42ef4a952f4334dd8","datavalue":{"value":{"entity-type":"item","numeric-id":794429,"id":"Q794429"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q529166$1D44759C-7C96-4009-BD41-4125F9AD43ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c53d05caedf1a345d5e708362edf868127bfcf35","datavalue":{"value":{"entity-type":"item","numeric-id":3140551,"id":"Q3140551"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q529166$2257E0FC-118A-4B7C-8F48-0FB9D38EBBD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8f215b4be5d109fd9d816f69f638d95cc094372e","datavalue":{"value":{"entity-type":"item","numeric-id":5552751,"id":"Q5552751"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q529166$E07D729D-6249-46D5-BD7C-256D51717DE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"33edf6c60e987374ac2b92fef6c7f79da2b1b282","datavalue":{"value":{"entity-type":"item","numeric-id":2881068,"id":"Q2881068"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q529166$609C9827-2256-4F52-800B-D57405685EF5","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":"Q529166$602D7383-B777-480D-A12B-197C2BFCBD74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ccd4ac1cf38ce7adf87c1aa2fe250a0bc62e564b","datavalue":{"value":{"entity-type":"item","numeric-id":581617,"id":"Q581617"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q529166$739D1E7E-A5A1-4705-9876-D9739553F32D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"180dcdcd70e7dd722922a02e19e8df3d14ff3abb","datavalue":{"value":{"entity-type":"item","numeric-id":3413659,"id":"Q3413659"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q529166$3285138F-42D5-49CF-892D-CAB8AB90A18A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2dfdf450746c95865439cf08883bd3a1c78d6c83","datavalue":{"value":{"entity-type":"item","numeric-id":1114669,"id":"Q1114669"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q529166$982B008D-55FC-461F-9D25-8FF71E3F0EF2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"34a0e856b37ab641259d132d542c40481e9faf36","datavalue":{"value":{"entity-type":"item","numeric-id":1264143,"id":"Q1264143"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q529166$4BE99B0B-444A-4F70-8FB7-12CCDB6417AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d7d21ba7c9e01a1e4d50952aba9cb27df7aae8db","datavalue":{"value":{"entity-type":"item","numeric-id":1113939,"id":"Q1113939"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q529166$88E5FE77-02CE-4956-8CA5-6BC5019EFAA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3b47493d23b79eb82583fe61d79ce073e0da0bed","datavalue":{"value":{"entity-type":"item","numeric-id":3671563,"id":"Q3671563"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q529166$C620436D-8B60-482E-B7B2-5B0BD7D9BAD7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dd9ef86b2ad7fb68ccf2a951e8b468542d85fcab","datavalue":{"value":{"entity-type":"item","numeric-id":1185458,"id":"Q1185458"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q529166$391DD344-7183-42D8-B9A6-F97ADB31C050","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"813f00e49fcb12172c27504dfeecb9018f840f1f","datavalue":{"value":{"entity-type":"item","numeric-id":2651859,"id":"Q2651859"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q529166$796B7F05-D3E2-4B6B-821E-F3E72B81CB39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c8be9375a315209f41df1b38374a5e7e956d28bf","datavalue":{"value":{"entity-type":"item","numeric-id":5807665,"id":"Q5807665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q529166$7B7326C7-5112-46A9-84AC-8BC60FCBBFA4","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b122c49f8b3c0f4182c411136467677f93c12f00","datavalue":{"value":"10.1016/J.APAL.2017.03.001","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q529166$04DBF5A7-FE91-45A8-B567-BB44B709D725","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"14d92be5fbf609684652a1bc7590db43f6f12bb0","datavalue":{"value":{"entity-type":"item","numeric-id":3140551,"id":"Q3140551"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"52c60dab80d8996f0ad57f6d3ed87beed33f1b86","datavalue":{"value":{"amount":"+0.8253015875816345","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":"Q529166$AB35E1EF-269F-4460-8D1E-0608C1F00774","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9599fabc76c44506b389f95a6ca15a74540d2158","datavalue":{"value":{"entity-type":"item","numeric-id":677553,"id":"Q677553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"69422016421cc828c50638840824caa6779ffcd5","datavalue":{"value":{"amount":"+0.8216375708580017","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":"Q529166$D74FB7B1-BC44-42E0-A694-45FC72A93AF4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1dabcbab1e4d1e7311caff28d84ce93acc6d4ba0","datavalue":{"value":{"entity-type":"item","numeric-id":5292667,"id":"Q5292667"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2261151c9d73060c79ce098393fb7ad1a4fccc37","datavalue":{"value":{"amount":"+0.8170863389968872","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":"Q529166$7547B41B-EF6A-4175-A48A-CFB0513410F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0fd1da1462720572f75f030936eea2f5f28f7031","datavalue":{"value":{"entity-type":"item","numeric-id":4371694,"id":"Q4371694"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ecf4ae955168743de0113c8c17334e492adf1f66","datavalue":{"value":{"amount":"+0.8153003454208374","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":"Q529166$4C1EB66A-3C4B-4115-A005-3ED2C492BCB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"201f88c6add97fcb2ad85bda4aed9e3c234adc12","datavalue":{"value":{"entity-type":"item","numeric-id":4038744,"id":"Q4038744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"90e81a02df3403e7b6e939d398bf617546ff0756","datavalue":{"value":{"amount":"+0.8017382621765137","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":"Q529166$34D0B837-6AE5-425A-8408-FB58E02FBF97","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:529166","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:529166"}}}}}