{"entities":{"Q5927985":{"pageid":8104787,"ns":120,"title":"Item:Q5927985","lastrevid":47588662,"modified":"2026-01-02T03:59:41Z","type":"item","id":"Q5927985","labels":{"en":{"language":"en","value":"Controlled use of clausal lemmas in connection tableau calculi"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1579157"}},"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":"Q5927985$13E01312-3CC1-4F01-BB05-2607D1A4E73A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4458ea9b6949cadafd11fdde5a283e5f54e77f1c","datavalue":{"value":{"text":"Controlled use of clausal lemmas in connection tableau calculi","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5927985$28E72B24-BB23-4283-8CF8-1DFC8B74C774","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2c1826b4008b43e0acf094850ff78ad84f2730b5","datavalue":{"value":"0969.03018","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5927985$44483F2A-8D7C-485F-9441-EF24E19E1304","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a7e6fffbecb83d3a5fffbe11935cdeae83ea4db0","datavalue":{"value":{"entity-type":"item","numeric-id":167071,"id":"Q167071"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5927985$86B06941-3615-4677-B814-B594E00BBE72","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":"Q5927985$A64EDA3C-C3C9-48CD-A568-A3E11E6B22BB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0da0ddb63369ee51f0c4f965ee150089663821f4","datavalue":{"value":{"time":"+2001-03-19T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5927985$5020EF3C-DCCC-455D-82B0-0358DDBF464D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4c434dc23286ff393e6c6048960ea50ea542cdbe","datavalue":{"value":"https://semanticscholar.org/paper/92354a3350e26fef78dcd6588213a1efefcf0e66","type":"string"},"datatype":"url"},"type":"statement","id":"Q5927985$CB1E8C12-4CDE-4F84-A0D2-25729645DEC3","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"d9c7994377655925beca167212c6ec3527b954b5","datavalue":{"value":{"entity-type":"item","numeric-id":587084,"id":"Q587084"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5927985$F9721701-FD12-40CC-965B-7DEF993B86EB","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5927985$54C23562-46FE-4132-BCC7-3C219E1B9BDD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5927985$9F5EEB7A-5A12-44FB-A974-F84D0EC66133","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"38cb7e8dc5cb52a83265e380f6a0feaf95c9257a","datavalue":{"value":"1579157","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5927985$CFDF48BC-7870-4BBC-BB95-BEB2CF628AAE","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"45ba0550e07e04a3326d1cb7dbe398ac3d7c209d","datavalue":{"value":"tableaux","type":"string"},"datatype":"string"},"type":"statement","id":"Q5927985$7FB090DB-499C-4B96-896B-D3A48F149C07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"202ab9c7203affce32741cb7fafe4c3185e25498","datavalue":{"value":"clausal lemmas","type":"string"},"datatype":"string"},"type":"statement","id":"Q5927985$1CC16BA5-CD89-4921-BD1F-C954CA6772CC","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c845b927c7c8299e3e10848fbe9373f51ae3559b","datavalue":{"value":{"entity-type":"item","numeric-id":13461,"id":"Q13461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5927985$AD384880-FA64-4309-8EA4-14CBF22BBB22","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d3ed9701b24c07e8ddeb19932e1fa77191c06e95","datavalue":{"value":{"entity-type":"item","numeric-id":16327,"id":"Q16327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5927985$AEEF5D33-0714-4562-BAA3-B86E55C2CE1C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"497739b1d588e442d5b7ba6bb4cccae512fc3231","datavalue":{"value":{"entity-type":"item","numeric-id":19196,"id":"Q19196"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5927985$304F4FF4-3022-473D-995D-DD2B68A3DD74","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":"Q5927985$3C0BF3AF-131A-4CFA-92E3-A4968458D29B","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"802eaebd63592179e2ad17d1927cba287d1c4455","datavalue":{"value":"W2018015794","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5927985$4E85273E-16E3-47B4-86AF-08610DC717DB","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"239a5725b0418b9b6339a2498e2f723fdb84abcf","datavalue":{"value":"Q124987221","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5927985$69792AC9-F6BE-46B5-96E6-2245A7052D14","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"58c3a9e4976685d7e1f5e42b0c7df8599a954d3c","datavalue":{"value":{"entity-type":"item","numeric-id":1367083,"id":"Q1367083"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5927985$7E7C788C-4C20-4167-A204-FF8DB6609D82","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4aefe5e0f2b827afb25f0a8067d25c4a893f91ca","datavalue":{"value":{"entity-type":"item","numeric-id":4304492,"id":"Q4304492"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5927985$EEA69F8C-AB59-4741-A15A-1B735021CCF3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d50f7c606a252a2bb504f7358999ab7b1ba3c57d","datavalue":{"value":{"entity-type":"item","numeric-id":1369080,"id":"Q1369080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5927985$265B928E-4C2B-4C07-913D-1CFD3F8DAD40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3227430383174e53fe133e3ddc098d739ef3ea15","datavalue":{"value":{"entity-type":"item","numeric-id":5234689,"id":"Q5234689"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5927985$7595AB71-EB4F-4B17-B15A-8F228341C108","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4448aad8e3c411d3b129c329d16917996a549120","datavalue":{"value":{"entity-type":"item","numeric-id":4524780,"id":"Q4524780"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5927985$D1A4F424-6849-4A38-98C4-EC907EB6AEED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6ad2e3e71fd34316c4d5dca241131f17edc1acca","datavalue":{"value":{"entity-type":"item","numeric-id":4863622,"id":"Q4863622"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5927985$7EA82F4E-9CE0-496B-B0D8-C68FD7B78CBF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b9b007d9692aaf24bb87f46349cd1171a8596486","datavalue":{"value":{"entity-type":"item","numeric-id":4934144,"id":"Q4934144"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5927985$BA696889-929B-47CC-8AB5-E39DEE8FB721","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"014df434e19c98aa84979531cf42f2d47588711c","datavalue":{"value":{"entity-type":"item","numeric-id":4647531,"id":"Q4647531"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5927985$4531014C-138B-4795-85CA-072DFA3D13FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1060b28c11ad81dfc8e252f1a4dc8748ef24df8b","datavalue":{"value":{"entity-type":"item","numeric-id":5234698,"id":"Q5234698"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5927985$EED62E5E-F211-47B8-A6A7-0913A2DFB253","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a1f0b5c5d1ef7da893967c1b74defc4984f71dee","datavalue":{"value":{"entity-type":"item","numeric-id":1062761,"id":"Q1062761"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5927985$AA6B7411-8696-4A36-A06A-DB2333D29FBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"158bb2233935470152d2dc667c5dec4b7a43c81a","datavalue":{"value":{"entity-type":"item","numeric-id":1344875,"id":"Q1344875"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5927985$EE197995-DF9A-4741-B47B-5A88D33227EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"07bde1b1ec996aeb071ba3c817fedaeed25122f5","datavalue":{"value":{"entity-type":"item","numeric-id":1189726,"id":"Q1189726"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5927985$63AA6E8E-3713-4275-ACEC-E3D13EEC1989","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"65f72fa731d5ef46f7c8727b7b59f2eaf22c3523","datavalue":{"value":{"entity-type":"item","numeric-id":5544307,"id":"Q5544307"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5927985$1DF26F28-3FF3-413F-AE38-1639E8712720","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8586c92c4d90a06cb521bef03111f958a597fe2e","datavalue":{"value":{"entity-type":"item","numeric-id":5574714,"id":"Q5574714"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5927985$9C8B58E4-B78E-4642-A084-C5D19CFE8F90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b1aa9e8bb4ef37ec285d6c238c3f5aa5ed5c9a38","datavalue":{"value":{"entity-type":"item","numeric-id":4139711,"id":"Q4139711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5927985$9F631CF5-1CC1-44D6-9853-6A041B46A479","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"90f433ac33b3245fd33c075feb679ff4c7546eea","datavalue":{"value":{"entity-type":"item","numeric-id":3493274,"id":"Q3493274"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5927985$B3240B09-4C14-4A94-ABD8-4CA98B6CBF94","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c5bd4f24e8eb1a084ca4ac4963d45f487b7e5bb4","datavalue":{"value":{"entity-type":"item","numeric-id":1226867,"id":"Q1226867"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5927985$F29639C2-68C7-4249-A617-42ABC0C0785D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5ab938ba3d2bb1de7d34dc0f9166735f59a48b21","datavalue":{"value":{"entity-type":"item","numeric-id":1114446,"id":"Q1114446"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5927985$2A461248-FA9F-46BE-85DE-0F12625A432B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"07441aec0715add91dbf903fea4c539fe7c16a9c","datavalue":{"value":{"entity-type":"item","numeric-id":5210777,"id":"Q5210777"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5927985$9F5E4DFA-6BEC-476C-8C2B-94BB5BD8771E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"cd171b2514e430ca4968762ad99300624c21424d","datavalue":{"value":"10.1006/JSCO.1999.0363","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5927985$6CCB3334-E91E-4BA0-B668-B91E9F1908DA","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"adca8d1d64ddb9d5edced7f21edafcfda7561f0f","datavalue":{"value":"The use of clausal lemmas is investigated in order to develop a method to reduce proof lengths and depths and to provide an appropriate reordering of the search space in connection tableau calculus. Specifically, an integration of bottom-up elements, the clausal lemmas, into the top-down oriented connection tableau calculus is provided. NEWLINENEWLINENEWLINEThis paper is based on results of \\textit{J. Schumann} [Lect. Notes Comput. Sci. 814, 774-777 (1994)] and the author [ibid. 1421, 33-37 (1998)], where, in order to refute a set of clauses with the connection tableau calculus, a set of unit lemmas is created in a preprocessing phase to be joined to the input clauses. One contribution of this paper is a method to develop an appropriate set of clausal lemmas which can provide proof length reductions in a number of refinements and extensions of the basic connection tableau calculus. NEWLINENEWLINENEWLINEA second contribution is the intelligent control of the application of these generated lemmas. In order to control the use of lemmas, in contrast to previous approaches in which the lemmas are selected without considering the given proof task and the search scheme to be used, techniques are developed for selecting relevant lemmas based on partial evaluation techniques which consider both the given clauses to be refuted as well as the search method to be employed. NEWLINENEWLINENEWLINETo evaluate the proposed method, a number of experiments with the theorem prover Setheo have been conducted using the TPTP library.","type":"string"},"datatype":"string"},"type":"statement","id":"Q5927985$851629C7-E33B-4E8A-998D-952C7A2DB0A3","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3dd2e7186fbc5fe7eb5cd827e3a95b7b9aad2f8f","datavalue":{"value":{"entity-type":"item","numeric-id":4934144,"id":"Q4934144"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eaca70f32da46046999d27a6ea0fde46564f81f5","datavalue":{"value":{"amount":"+0.8011530041694641","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":"Q5927985$2B354488-0791-4193-BC47-709F1E277071","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"efc7b29f5019a6e831cbad37caf79b29e7cc07ed","datavalue":{"value":{"entity-type":"item","numeric-id":4524783,"id":"Q4524783"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9889840278363bc9d00f5a5e3f843ae2ec9a1865","datavalue":{"value":{"amount":"+0.7793223261833191","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":"Q5927985$EF3B4960-F775-4E1B-9867-8A84F1523E31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e41eae31321cb8f4d5091ef38abb8a9ca30ef670","datavalue":{"value":{"entity-type":"item","numeric-id":3010371,"id":"Q3010371"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d168229f361b5f4a5052fcfb71bd3557d06a5a99","datavalue":{"value":{"amount":"+0.7793222069740295","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":"Q5927985$FC57CEB5-595C-4873-A4A0-64E9669225D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"db8476da4648dc0228d7d9a6f4cd404123e4ebcf","datavalue":{"value":{"entity-type":"item","numeric-id":2726303,"id":"Q2726303"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2aa269e0c46aab25f8c435e7884ebdc346ce6816","datavalue":{"value":{"amount":"+0.7684447169303894","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":"Q5927985$D938D831-2EAF-49BD-A8C6-9FDF0A5A448C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d46680a2102220f2fd452643ef7fdeb867dfdd0f","datavalue":{"value":{"entity-type":"item","numeric-id":2721202,"id":"Q2721202"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2aa269e0c46aab25f8c435e7884ebdc346ce6816","datavalue":{"value":{"amount":"+0.7684447169303894","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":"Q5927985$B6CEE1D5-B3FB-41D5-ACD9-5B4A1AFD208C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5927985","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5927985"}}}}}