{"entities":{"Q1114445":{"pageid":1125194,"ns":120,"title":"Item:Q1114445","lastrevid":66157785,"modified":"2026-04-12T07:56:25Z","type":"item","id":"Q1114445","labels":{"en":{"language":"en","value":"A new reduction rule for the connection graph proof procedure"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4083032"}},"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":"Q1114445$97E6F94D-BA40-4949-BD55-649C041C3070","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"976fbd83f66bf034b8a1b8018343e8ac169b953d","datavalue":{"value":{"text":"A new reduction rule for the connection graph proof procedure","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1114445$E95A10C0-633E-42BB-B5FD-98FD0E3293D8","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4dfde9fd59ec5e32a53ea2f83ee425dd935bbb70","datavalue":{"value":"0662.68103","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1114445$59B4CC93-CC73-4004-B57C-9B992390B6F1","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6f64084c86f40ca8b5a9a3a9f039bfc28c7655d3","datavalue":{"value":"10.1007/BF00297248","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1114445$DEDF2222-86DF-42FA-9DB7-E0F63173876C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"fb4c12377d7bffe72b62b0c64be315dfb7289453","datavalue":{"value":{"entity-type":"item","numeric-id":1114444,"id":"Q1114444"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1114445$F823E462-8A08-4D58-8A31-05B9BD79C259","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":"Q1114445$C780D7DC-4B97-4498-85EF-1B4E9B4D353A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"31a1937240ca4a323604b4728c31d242b5596d7c","datavalue":{"value":{"time":"+1988-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":"Q1114445$14ACA179-DB49-4686-9620-CE6B6E8CDF90","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"c53f0adaa89049e439f61776fa29b8ab706235ff","datavalue":{"value":"The connection graph proof procedure (CGPP) is extended from one-valued variables to set-valued variables. Finding the set of values for clause variables, and checking which links can be removed, is performed during the extended unification procedure. In this context a new reduction rule is introduced (called v-rule), leading to refined link removals in CGPP. The author argues that the introduced v-rule preserves the refutation confluence property of the resulted CGPP. A proof system containing the v-rule has been implemented by the author in PROLOG, and successfully compared with other priviously existing proof systems on the Schubert's steamroller problem. The relation of this approach to order-sorted logic is pointed out. We suggest the (not only) formal connection with the (linguistic) feature structure unification algorithms (and grammars).    Despite the extra-cost involved by the v-rule administration of clause variable values, the system proves to be prominent considering execution time, while generating the fewest number of derived clauses.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1114445$CC58D06F-065C-4CB1-BA5B-57C4DD3A024E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1114445$4EA0CA52-D66A-4AC6-B4FF-977479C5DBB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1114445$FE29BE07-31CC-4FCA-B0D6-B9B1791F5BC4","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e350800e7c952bf044acfab2ebec161662d48ccb","datavalue":{"value":"4083032","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1114445$C79976AC-5365-4FD9-B247-C94966CCDCD8","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e97175fd5d747e7d34cbcc625e3abab53d84653d","datavalue":{"value":"automated theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1114445$F3D8BFFE-EE7C-4826-ABC8-7853EE5C264D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1aa5f484a838b484febc3b4ebe1a6ca190c8ce19","datavalue":{"value":"connection graphs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1114445$2B180D88-BF67-45DB-9D3D-EEC5A5828A22","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cfac5eb6431ec88e2a6e9bafbfcf7b49dda794fc","datavalue":{"value":"resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q1114445$7E4FCFA4-E95B-458A-B401-983C67284841","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c17c6c5f1f39281a7c608e75e90e4767b3d32e0a","datavalue":{"value":"order-sorted logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1114445$2EA69B56-D0FD-4BFE-8B28-8125C3CE2773","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"ddfe26001cac27b44f73ee317c958b41c5d4e225","datavalue":{"value":{"entity-type":"item","numeric-id":585901,"id":"Q585901"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1114445$1C2A8F97-5029-4CD7-8015-E0C196B69A72","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":"Q1114445$515B7157-BD91-466D-BF57-7F78A66DBAE4","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"82285947ecd1d65d80e17696025cdf5ddb799be6","datavalue":{"value":{"entity-type":"item","numeric-id":3922205,"id":"Q3922205"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1114445$72DBF69F-E58D-434B-964D-6F97C09AB163","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3a4735154d50c08d584a8e28202802fa9d661654","datavalue":{"value":{"entity-type":"item","numeric-id":5679729,"id":"Q5679729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1114445$190C6B7B-79BC-4B9A-8EF0-3AFD4FBD11D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"088de41fe6d8646ce7f075a0c90a5bcc32089f07","datavalue":{"value":{"entity-type":"item","numeric-id":3783625,"id":"Q3783625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1114445$3B946DE4-FE65-49D5-ACC6-7E9D6F32A90A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a45ed88c84c30a799c478233e266ce605894b324","datavalue":{"value":{"entity-type":"item","numeric-id":4133168,"id":"Q4133168"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1114445$CE4723B9-EFBB-454F-9243-0AE6776F3F63","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d9a872690aae65aa8cbfced9522c07629e0a8e21","datavalue":{"value":{"entity-type":"item","numeric-id":3862380,"id":"Q3862380"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1114445$97C70167-4FCA-4FF6-8837-4C7A699B3656","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"27ee3b057142576093bd9e66364057980fafc0e4","datavalue":{"value":{"entity-type":"item","numeric-id":1821564,"id":"Q1821564"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1114445$B5FD1EFE-5D71-47A5-BC41-42FDE87E942F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8aefcbbb48c9809b0ea99532e8c981cd3b1e3ae5","datavalue":{"value":{"entity-type":"item","numeric-id":1101259,"id":"Q1101259"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1114445$F8E4FA39-518C-4416-A224-C629E4C092A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"09289f6833573b3dfe785ef27b87fe1f0ccbfbc3","datavalue":{"value":{"entity-type":"item","numeric-id":1060859,"id":"Q1060859"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1114445$77A53C52-9DDF-425C-8115-FC403F3A4100","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b291019264cf5e54c2864208bdfb95c1a1e44d28","datavalue":{"value":{"entity-type":"item","numeric-id":4095917,"id":"Q4095917"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1114445$292FB219-3BBD-43F9-B4FB-2A6E7525248C","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4bfdc062c9d934ee4c497de2e8ca97f56c8e32f8","datavalue":{"value":{"entity-type":"item","numeric-id":1199542,"id":"Q1199542"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ac6e4780f5bb1d46cf8c50cad39c75d1e558af59","datavalue":{"value":{"amount":"+0.9136137","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":"Q1114445$328F2AFC-797A-4FC8-9D3F-5B8A7C73C4DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"46944bb8da42e8da4a7af99ea3d9b322c9f22d85","datavalue":{"value":{"entity-type":"item","numeric-id":4037299,"id":"Q4037299"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"66fe1d6a2cef8aac6770f5c987c53dee3b7f0a78","datavalue":{"value":{"amount":"+0.86244047","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":"Q1114445$1DE6F776-CB3E-483D-B060-35CE958B9F6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"36c07be3a81a593d5fd87aaa23a4edcc6c764e2c","datavalue":{"value":{"entity-type":"item","numeric-id":4285634,"id":"Q4285634"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"66fe1d6a2cef8aac6770f5c987c53dee3b7f0a78","datavalue":{"value":{"amount":"+0.86244047","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":"Q1114445$0238CFB4-F492-4D0F-995B-80CA23AD4037","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"040ec92cc214599ecdf38d6bd02ff3927f501733","datavalue":{"value":{"entity-type":"item","numeric-id":1669583,"id":"Q1669583"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c59c9be139b7c49742c345c09b64cab8128fdbc9","datavalue":{"value":{"amount":"+0.8622754","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":"Q1114445$D0B49D13-B5A6-4C40-B494-E76005DBFEFF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"461d9141354035a34b52c82d900f972033218370","datavalue":{"value":{"entity-type":"item","numeric-id":3032302,"id":"Q3032302"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a50a67c5ac977261bdb2e03e9ea584d0230d6064","datavalue":{"value":{"amount":"+0.8620271","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":"Q1114445$8F52B0AB-9633-433E-8B95-ABB72E864C46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cb541ea4ab00798066a9ea18e5fd9c688517a683","datavalue":{"value":{"entity-type":"item","numeric-id":3638039,"id":"Q3638039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"636fe99ec7f5007a82a9c1d8118944ab0188d656","datavalue":{"value":{"amount":"+0.85981995","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":"Q1114445$0FD1DF72-5C33-4AE2-8804-43DB50DAD850","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4b5d94eac23b34bee4cebd91c0adbe4274e61aed","datavalue":{"value":{"entity-type":"item","numeric-id":4964705,"id":"Q4964705"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aa40ffbadf93cad1afe7524f8da40e1f5c48255e","datavalue":{"value":{"amount":"+0.84949696","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":"Q1114445$612DF666-F046-4379-8FDB-F257B5AF514A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d82055788cb8862532211c629cf4f414dce739c9","datavalue":{"value":{"entity-type":"item","numeric-id":2509541,"id":"Q2509541"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"140e29da41949c7dc958d1f2f85626c5cfafe523","datavalue":{"value":{"amount":"+0.8489866","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":"Q1114445$665150B6-B1F2-42EF-84FB-50D3455F62E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a8cd0ea8c677ccb5e707eba3ce592df495f7e48a","datavalue":{"value":{"entity-type":"item","numeric-id":1657766,"id":"Q1657766"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"72870ac34ee38e190f99b7bb89e451b2a5d5d6e3","datavalue":{"value":{"amount":"+0.8484098","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":"Q1114445$B45BE16A-4569-40A5-8029-89D87B3CE527","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A new reduction rule for the connection graph proof procedure","badges":[]}}}}}