{"entities":{"Q352970":{"pageid":354737,"ns":120,"title":"Item:Q352970","lastrevid":61229226,"modified":"2026-04-10T22:00:13Z","type":"item","id":"Q352970","labels":{"en":{"language":"en","value":"Case splitting in an automatic theorem prover for real-valued special functions"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6184688"}},"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":"Q352970$5CC2C168-F80B-4A97-8D8E-F28D67FAEBC3","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"3a978aa3822841f09639fab8f7bd336c380e4791","datavalue":{"value":{"text":"Case splitting in an automatic theorem prover for real-valued special functions","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q352970$A864C2BA-F085-47A8-857B-84EE53A48C87","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"06a6fd416148844b0ea044a04741a36318b97eaa","datavalue":{"value":"1361.68187","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q352970$62E4C915-B9F4-4754-B7AE-76AD8A1E1AFD","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"1be65b849f210a7fec970f287e95842fedc2fd00","datavalue":{"value":{"entity-type":"item","numeric-id":352968,"id":"Q352968"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352970$9787E78A-1940-40AF-B8B4-A7C2B9681040","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"cb5dfbdfa6d8a2070a67ff948fb8abd387eda36e","datavalue":{"value":{"entity-type":"item","numeric-id":352969,"id":"Q352969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352970$8AE9D583-7F38-47C6-8672-775D1429CAA1","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":"Q352970$304FD100-6101-44C1-8F40-A04BEE265B35","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e553745941756c98d8238154d74f9ad7174c4d8e","datavalue":{"value":{"time":"+2013-07-05T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q352970$D8960AA5-0CBF-4E54-807D-37049962E952","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q352970$37BCF440-9213-490B-8C33-E4CBB2E2FD96","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8fc0675e2f2b88b498fa564da7317e3fe2d2a921","datavalue":{"value":"6184688","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q352970$7AAD3F25-1936-4F35-9D75-67FF3999B311","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"88fab1d7dadc9c096095fb8f4f755156daf4bb08","datavalue":{"value":"splitting","type":"string"},"datatype":"string"},"type":"statement","id":"Q352970$385950D6-5F7F-404E-9D65-78E1CF8CCBE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"03158307b01a6e2de96f5585d7a65d8e1a522aae","datavalue":{"value":"resolution theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q352970$3BB0A275-3501-4C43-BBD1-E1158E55BE2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9daa77eaa3d4f804cbf95715b13eb9fde1568b07","datavalue":{"value":"SPASS","type":"string"},"datatype":"string"},"type":"statement","id":"Q352970$7E683709-988F-4F48-A5BD-C5CEEEE6E163","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"77e035207aee986c2304b8f0359324054b2f96a9","datavalue":{"value":"MetiTarski","type":"string"},"datatype":"string"},"type":"statement","id":"Q352970$F33EDF80-CFD3-4027-B00D-620AC71A7B46","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1e7b4d238eeafa5b21b1ef85a0d6b8900bfdc422","datavalue":{"value":{"entity-type":"item","numeric-id":15442,"id":"Q15442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352970$3069BE04-1EB7-4559-ABBF-2D0D13FFDCA2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c6f90a2f4d38316e0bb5a27c4b90cf6cce495aa0","datavalue":{"value":{"entity-type":"item","numeric-id":16295,"id":"Q16295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352970$20B08AB9-EAFA-4CBE-96CA-53285B190BDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bf8fe40ec0751f683b8f31fdc6f7f38f8aa07409","datavalue":{"value":{"entity-type":"item","numeric-id":13328,"id":"Q13328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352970$8977F61B-2106-4F0D-859A-22037AF08ACD","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":"Q352970$51015422-F85F-4D4A-A171-A33E0AAF43AE","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"2208073c0cc81c7de58319f7799d631de77c4081","datavalue":{"value":"https://doi.org/10.1007/s10817-012-9245-6","type":"string"},"datatype":"url"},"type":"statement","id":"Q352970$1487581A-F5E2-4F4C-8B8A-A72E6A411628","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"120723b8882c935ff2f4a3aabbae7eb6c268b458","datavalue":{"value":"W2061644010","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q352970$218AA8E5-EA1F-481D-9D42-6EC571DC99D8","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"5253ff7f5cfb213e1ce45c278b76adb0228a1123","datavalue":{"value":"Q57382569","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q352970$BEBDB2F6-816C-4EFF-B12A-E9A52352A354","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"a602a31ec5858953936704adacfb1f5bdcaed350","datavalue":{"value":{"entity-type":"item","numeric-id":972422,"id":"Q972422"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352970$B40E4472-BDFB-4812-BDA9-38CBD1E6A538","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8b1137cf78c4cad0e217f70ec321f2a593915490","datavalue":{"value":{"entity-type":"item","numeric-id":2751353,"id":"Q2751353"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352970$CE93CFF2-AD67-4D8E-A024-194565905FF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8e7f4e131abd397423f508ff6cb02fd16c492dec","datavalue":{"value":{"entity-type":"item","numeric-id":1037396,"id":"Q1037396"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352970$967A1E06-ABA3-4B14-9D96-FC7FDF82CAB6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"741b1c2a1697c669d1b3bbdff87dd79f9f007366","datavalue":{"value":{"entity-type":"item","numeric-id":1006731,"id":"Q1006731"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352970$F9CCC7E1-5757-4A3C-BB81-53B07DCBDA3F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c6c47ba658147eed1f52d5e15acf44bb09b5d41","datavalue":{"value":{"entity-type":"item","numeric-id":5615207,"id":"Q5615207"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352970$F6E8E35C-BD7E-48DD-B5EC-9FD980079C8F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c2593297dec2eecc4260eaa6f5720cca81293d30","datavalue":{"value":{"entity-type":"item","numeric-id":2996161,"id":"Q2996161"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352970$CDCB68C9-1764-46D5-A55E-92CB99671E38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"28deebb9f03725888e2cb415bbaa29688963935e","datavalue":{"value":{"entity-type":"item","numeric-id":2751358,"id":"Q2751358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352970$A97CF7F9-D19C-4F7F-B0CA-D78B8476317D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"81507f430d90ccca44c5914f167260e0646ee88a","datavalue":{"value":{"entity-type":"item","numeric-id":2751379,"id":"Q2751379"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352970$591F9F57-E6B0-489D-8AA0-B215078CD746","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47bab4f7d1b2661e9a9ca3ddc35e5a57311ad582","datavalue":{"value":{"entity-type":"item","numeric-id":5507985,"id":"Q5507985"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q352970$ED5046CF-6D85-4CE7-A0FA-E6EDE60187DB","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"914c5a885a7a3f7dcae41d8fc3c3271ac57c5018","datavalue":{"value":"10.1007/S10817-012-9245-6","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q352970$828A2B52-F5BE-46BB-BAAA-528D79110309","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cf8124ff86b0561d7e3d91b38332044514d7d11e","datavalue":{"value":{"entity-type":"item","numeric-id":2819703,"id":"Q2819703"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"949f6def4a2547d6dec9ed33b2976812d06115c2","datavalue":{"value":{"amount":"+0.8834441","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q352970$BF12C883-B186-4FDB-852F-8A7ABF89BFFB","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":"691b512e822bbffa7ca2d0007c57b0db07476a3f","datavalue":{"value":{"amount":"+0.8661159","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q352970$73595F92-FF3D-4FDA-AB50-0DFEEFF4D3B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8e817ad8dc837ce10f68b1d24ed037d075a1da14","datavalue":{"value":{"entity-type":"item","numeric-id":1098333,"id":"Q1098333"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7a670d4ca103b809f6eed0c2d57b6364bfc1e1b1","datavalue":{"value":{"amount":"+0.8253783","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q352970$28D63EA8-4D51-4F88-9DCD-40B0D7207175","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"82d170e51fc2e631d9cc31c3155e279e1d9e0a46","datavalue":{"value":{"entity-type":"item","numeric-id":5739977,"id":"Q5739977"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fdee09f28ba57473abcd710c28ded046cfa83394","datavalue":{"value":{"amount":"+0.8245541","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q352970$6016A8EF-559D-440C-B3F9-09BE25505280","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e5d4a044d7a3a1cc0968a929ccf3f585878b3b5f","datavalue":{"value":{"entity-type":"item","numeric-id":4437963,"id":"Q4437963"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6665a26d45e8401d4762d9a36bc906f4518766e4","datavalue":{"value":{"amount":"+0.8225923","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q352970$C04E3F8A-294D-4E18-B659-47FBA5AB8F59","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"202e7d007d9f9732850f56c0fee3c656ac5401de","datavalue":{"value":{"entity-type":"item","numeric-id":4275695,"id":"Q4275695"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3ee0ee7dd35f12ef4ff92d7fd3f80cdaf304094c","datavalue":{"value":{"amount":"+0.8187045","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q352970$2866A0B6-F949-4BA5-800B-74E123869186","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1cdfe0809a67bd178c2447b57e1f89d5cd887ebb","datavalue":{"value":{"entity-type":"item","numeric-id":4848888,"id":"Q4848888"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9a5022993f03559e92c85bb4e5c4aa3a6f04a8c2","datavalue":{"value":{"amount":"+0.81478906","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q352970$7EDF9865-1741-48D6-99BD-AD83FCD7BFD6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ab414be2c6411186daf1cce36968203a94258fc7","datavalue":{"value":{"entity-type":"item","numeric-id":3805962,"id":"Q3805962"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6a23353a21ac1fad4db644546c541f70035acd93","datavalue":{"value":{"amount":"+0.8142726","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q352970$E5A58038-551C-4A92-AC7D-5D4F3A1B9D84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7c1694d6bf440cb2a8ed659587389564d3cae23a","datavalue":{"value":{"entity-type":"item","numeric-id":3454118,"id":"Q3454118"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9bd36f2ed37f021170212e83ff58c6a93b297bbd","datavalue":{"value":{"amount":"+0.8133226","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q352970$C807062E-4B8F-4128-A3C4-E4FFA0E03AB5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"24c4e1af29df48aba6865efb69804492ca54b4af","datavalue":{"value":{"entity-type":"item","numeric-id":2703760,"id":"Q2703760"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"375d608c9d8483b32ec310ec937e126b86e7a5ae","datavalue":{"value":{"amount":"+0.8109824","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q352970$72242B13-D136-4BF6-96E1-7E5D03D340D8","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Case splitting in an automatic theorem prover for real-valued special functions","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Case_splitting_in_an_automatic_theorem_prover_for_real-valued_special_functions"}}}}}