{"entities":{"Q1094149":{"pageid":1104901,"ns":120,"title":"Item:Q1094149","lastrevid":66121572,"modified":"2026-04-12T07:41:30Z","type":"item","id":"Q1094149","labels":{"en":{"language":"en","value":"On the application of Buchberger's algorithm to automated geometry theorem proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4024826"}},"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":"Q1094149$E4E35EBB-B336-4543-A438-1367BCC76D79","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"50cb769403f2b7e7ee36a3f2a01760e8ea66044c","datavalue":{"value":{"text":"On the application of Buchberger's algorithm to automated geometry theorem proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1094149$52D1674D-6E46-4350-BB30-B8E54DB35ADD","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f526197a38a7c85094ccb408a49190cd90559b60","datavalue":{"value":"0629.68086","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1094149$514F8595-01EB-407F-B805-3475DF67D138","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"cf98c93a5a82695afdcf06e1d5ff5fde2b7ffdd4","datavalue":{"value":"10.1016/S0747-7171(86)80006-2","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1094149$31FD78DD-0EF5-4B10-AA2E-A908F30FF5A2","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d3b726e3f4c29f0019c47bbcb54fb6b3433c5d05","datavalue":{"value":{"entity-type":"item","numeric-id":1094147,"id":"Q1094147"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1094149$FC8D358E-8558-4193-AE0F-3943550AD1D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ecb96e52397a23d7143c7c9df1adbf40197ed8ab","datavalue":{"value":{"entity-type":"item","numeric-id":676067,"id":"Q676067"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1094149$642324EA-11FC-49A2-B16E-F2F3CCECC73F","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"ea72303f92787da89554ee5fa15621068821a762","datavalue":{"value":{"entity-type":"item","numeric-id":99061,"id":"Q99061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1094149$6FFE1796-986D-45C9-BE13-E7DBD0CEE3EE","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"63df7153432d81fa42019fcabb076c89649b0b5b","datavalue":{"value":{"time":"+1986-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1094149$BD53AF52-D79C-4608-ADCF-C34E50EB5FC1","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"6aa2135c065bdce33199b49cb950d3ced6814f1b","datavalue":{"value":"In this paper we present a new approach to automated geometry theorem proving that is based on Buchberger's Gr\u00f6bner bases method. The goal is to automatically prove geometry theorems whose hypotheses and conjecture can be expressed algebraically, i.e. by polynomial equations. After shortly reviewing the problem considered and discussing some new aspects of confirming theorems, we present two different methods to applying Buchberger's algorithm to geometry theorem proving, each of them being more efficient than the other on a certain class of problems. The second method requires a new notion of reduction, which we call pseudoreduction. This pseudoreduction yields results on polynomials over some rational function field by computations that are done merely over the rationals and, therefore, is of general interest also. Finally, computing time statistics on 70 non-trivial examples are given, based on an implementation of the methods in the computer algebra system SAC-2 on an IBM 4341.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1094149$27D5B7F5-A795-44C3-B0C4-3B70EC2A0BB1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1094149$A3E994F0-958B-4372-B1E5-6AD64EECC38D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6be78f1bad1f2f19058dbde65eb124c0430a7d27","datavalue":{"value":"68W30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1094149$90CE7E75-8700-409B-A722-93A40CDC9C47","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"fc7b0c7bad4da553fca734df2f71be506a3c75ee","datavalue":{"value":"4024826","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1094149$3F91A4A3-10A8-4817-B206-2D4F96E662C0","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f43dc8fe8f1ab231872a9f4f599c0cc472dd10ff","datavalue":{"value":"automated geometry theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1094149$E7004530-5820-4265-AFFF-BA991EDABE4B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"99c239dc77a316f7da47f9d2d7c645993f6cd8d7","datavalue":{"value":"Gr\u00f6bner bases","type":"string"},"datatype":"string"},"type":"statement","id":"Q1094149$E895D7C2-76B6-4D2F-B935-1408FFF57AC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bb71cc518f84064881cd5cd4cf306cfce0251acb","datavalue":{"value":"polynomial equations","type":"string"},"datatype":"string"},"type":"statement","id":"Q1094149$86A7897B-1A68-4770-B005-F40948BDB4D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"698542b58ea564916b2ef53688be87fbd4e7199e","datavalue":{"value":"Buchberger's algorithm","type":"string"},"datatype":"string"},"type":"statement","id":"Q1094149$46509D11-8978-48EB-A203-1BE2B758D3FE","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":"Q1094149$3C934F68-5288-4DAD-BAB7-A022A9001856","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d0d60285ae04471993c98b6fd4f9789d850bb6c","datavalue":{"value":{"entity-type":"item","numeric-id":2902935,"id":"Q2902935"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1094149$49E7AF6D-EC81-4F10-B2DD-9FB45AD1C195","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5d87900de754ad2a3f7d55a3f915d6adeffa7325","datavalue":{"value":{"entity-type":"item","numeric-id":2544438,"id":"Q2544438"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1094149$84924647-FFD4-408C-9E55-39529AB9073A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c2ff57ef70bd9e86c9b7017e46b8cd84cb7965f4","datavalue":{"value":{"entity-type":"item","numeric-id":3714165,"id":"Q3714165"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1094149$18982973-D6E1-4383-B40A-1BA8AA9E8937","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f0684a7538caea729f6ec434d1e733a91b587e40","datavalue":{"value":{"entity-type":"item","numeric-id":3700871,"id":"Q3700871"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1094149$CB600222-D32F-441A-A2DD-28B4EB8E23AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5107dc2805878ace8909c9d9b3a5ceeaec8135f6","datavalue":{"value":{"entity-type":"item","numeric-id":1101255,"id":"Q1101255"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1094149$D232E2D3-9E3B-4261-AC66-FC47B6BEA5DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"50956a48c455c952f0787896decd201cfb6d2916","datavalue":{"value":{"entity-type":"item","numeric-id":5789115,"id":"Q5789115"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1094149$CA364533-3220-4E8B-BB24-9EAC6B4CB20B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fb88951437ccd14e6bdebc77cda052045a02f0ce","datavalue":{"value":{"entity-type":"item","numeric-id":1094150,"id":"Q1094150"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1094149$1A933060-E01E-49BD-9287-0DA6CB1FB1FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"027e018eef8810ffaaa3893bf67adf6d2ef52c6f","datavalue":{"value":{"entity-type":"item","numeric-id":1094149,"id":"Q1094149"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1094149$81EE9A61-37EB-440B-AB25-9324EB78552A","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":"Q1094149$C76767AA-C493-4261-91D4-CD1C9DF65BFA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4d57db4d3216bc53e46ae99a268680181eb65b5a","datavalue":{"value":{"entity-type":"item","numeric-id":4153620,"id":"Q4153620"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1094149$0F3E03CD-0DE1-491A-9511-9BC0DCC68998","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"21e98e5133daef166526a0f4702a2a839800a900","datavalue":{"value":{"entity-type":"item","numeric-id":3668379,"id":"Q3668379"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1094149$C7171F7F-7F0A-44DA-9ED3-106617BB5E74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"490f8cc9bba78f72f7c3ffee7fdf68d548b63e57","datavalue":{"value":{"entity-type":"item","numeric-id":3700869,"id":"Q3700869"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1094149$B6CEA4D0-3D40-45C9-8748-D00E72131FD1","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d95f1d7edfdf6257ff9ad7c232192df093ebf87f","datavalue":{"value":{"entity-type":"item","numeric-id":4011813,"id":"Q4011813"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fe7b2f49d87fac0c2a1f94cca3fd45f3092c2aac","datavalue":{"value":{"amount":"+0.8888511657714844","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":"Q1094149$E1FA2E15-F39F-4BB6-8ACD-E59B3B1E3720","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"13a3f9ea24becc94351729d985022a6f2151cb77","datavalue":{"value":{"entity-type":"item","numeric-id":5393347,"id":"Q5393347"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"317c89e240bda179192d0020560a4ef19418a0f0","datavalue":{"value":{"amount":"+0.888850748538971","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":"Q1094149$B360F926-B1DE-4D7A-9878-720003F76780","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c5de2920f592edbe5f550d8ccc7bfeeeca50aa4a","datavalue":{"value":{"entity-type":"item","numeric-id":5203713,"id":"Q5203713"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f47a4bdb5e343d548a14bc9b56ab78b8af3fd2f1","datavalue":{"value":{"amount":"+0.8429290652275085","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":"Q1094149$2170FF8C-4494-4265-902D-0089F385DDDE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"816c9a0df76b51fe8c12d3110f1fabe3069a190e","datavalue":{"value":{"entity-type":"item","numeric-id":4841300,"id":"Q4841300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2067e637f366b62bdb5f6fcd646313c70cc66ca1","datavalue":{"value":{"amount":"+0.8325472474098206","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":"Q1094149$5970AFA7-5DA4-4583-8821-E8BABDC1244A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"32a20da8aa0a8155a33ac04b818c0dc31a8db7b8","datavalue":{"value":{"entity-type":"item","numeric-id":4889407,"id":"Q4889407"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e380a4da09df528c17cdd2b1e6fc70f38c4bd3b6","datavalue":{"value":{"amount":"+0.8315223455429077","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":"Q1094149$0B0A8A0E-67D7-463E-A438-6C4F94524657","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"On the application of Buchberger's algorithm to automated geometry theorem proving","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/On_the_application_of_Buchberger%27s_algorithm_to_automated_geometry_theorem_proving"}}}}}