{"entities":{"Q928656":{"pageid":930504,"ns":120,"title":"Item:Q928656","lastrevid":65442753,"modified":"2026-04-12T02:37:58Z","type":"item","id":"Q928656","labels":{"en":{"language":"en","value":"Connection tableaux with lazy paramodulation"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5287716"}},"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":"Q928656$59C6C6B6-525E-4327-8DC8-9EC6F054188D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6009554a22367615588d061c225f8fa425224bfa","datavalue":{"value":{"text":"Connection tableaux with lazy paramodulation","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q928656$99005B30-48CE-45E2-9FC8-41A4EA44F22A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0e007883fd57fa038186ae5e644d48795c67486d","datavalue":{"value":"1144.03008","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q928656$0155FF3F-C576-415B-8299-08D9E02C15BA","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ec54547b4f5c25170660bf9ec332f673814ae34c","datavalue":{"value":{"entity-type":"item","numeric-id":287383,"id":"Q287383"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928656$B9E322F3-E678-4CED-A1AD-B5024ACF2309","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":"Q928656$2CC48FE4-EB95-424D-B469-A9EA0019F44D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9f1c0b93a352a714c61ccd46766a52600d36f8c2","datavalue":{"value":{"time":"+2008-06-11T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q928656$66569337-2DBE-4ECF-B27C-ADB69730148E","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"1ffd6754f8b46902155c528409c1ba97e5fb4d1c","datavalue":{"value":"Up to now, no competitive theorem prover for first-order logic with equality is known which is based on the tableau calculus. The present paper presents such a calculus. It starts with connection tableaux and transforms the equality symbol into an uninterpreted predicate symbol and constraints, similar to [\\textit{L. Bachmair, H. Ganzinger} and \\textit{A. Voronkov}, Lect. Notes Comput. Sci. 1421, 175--190 (1998; Zbl 0926.03006)]. As a refinement, paramodulation is restricted to be lazy and basic, as in [\\textit{L. Bachmair, H. Ganzinger, C. Lynch} and \\textit{W. Snyder}, Inf. Comput. 121, No. 2, 172--192 (1995; Zbl 0833.68115)]. The calculus is proved to be sound and complete. Unfortunately, no implementation is available and so no comparison with saturation-based provers is possible.","type":"string"},"datatype":"string"},"type":"statement","id":"Q928656$047E93B9-49A1-45A5-9712-8F1D201D64EA","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"1024eb68be5ead5b1a13571c300dc7d3374934dc","datavalue":{"value":{"entity-type":"item","numeric-id":174769,"id":"Q174769"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928656$15E4E0E0-2E48-4163-AF5F-2995CD8B2D31","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q928656$8A17F5E0-9613-4A1B-A70D-E60479B2DEA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q928656$531C73EC-97D8-47C7-BE4E-D3B169A984AC","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c88aa4fe17d6433503f56b59b7465c2f88889ddd","datavalue":{"value":"5287716","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q928656$FD10BD22-0236-4A0E-8082-0562F10B45DB","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"098925cca13caec604ae9347f1b8673ec619b16e","datavalue":{"value":"connection tableaux","type":"string"},"datatype":"string"},"type":"statement","id":"Q928656$9BD9A735-4C60-460E-9925-563AD2ED7A7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"83abf26cae7fdb9fcff130a3454efd3f336b5419","datavalue":{"value":"lazy paramodulation","type":"string"},"datatype":"string"},"type":"statement","id":"Q928656$40769F5E-B27D-4D70-A906-12B1D4676D22","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cf59c453cdcf995751dc5089749fcf7811fe9170","datavalue":{"value":"basic ordered paramodulation","type":"string"},"datatype":"string"},"type":"statement","id":"Q928656$DCAB725A-BD96-4751-BDB1-1F96D6D2F810","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c9f81fd79d9a404edbf19c987163b4693c5a6aa6","datavalue":{"value":"first-order logic with equality","type":"string"},"datatype":"string"},"type":"statement","id":"Q928656$E951B088-6ED1-4E7E-B8DD-7E42CC138E92","rank":"normal"}],"P1463":[{"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":"Q928656$D2E7B298-2408-4E2C-84C6-C7320AC62898","rank":"normal"},{"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":"Q928656$C635AD9A-5E8C-4E24-AA78-07A1D82A88AC","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":"Q928656$AFF20D55-C8EE-4103-B5E3-59009AC61A08","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"732a40c16ecad65df24cd8524686ac317cb73923","datavalue":{"value":"https://doi.org/10.1007/s10817-007-9089-7","type":"string"},"datatype":"url"},"type":"statement","id":"Q928656$0B3E809A-9822-43A8-87FE-6D6313D4BE39","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"da28059503e1f051b4471c646942ffa5b99b2be0","datavalue":{"value":"W2045057655","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q928656$7477F9CD-8DEF-4605-9757-9C3C34FC888E","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"8ad7c23e8d7895495a33ef0a244c1d5f7a7d7e16","datavalue":{"value":{"entity-type":"item","numeric-id":1899908,"id":"Q1899908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928656$8FCDBBA4-A877-4466-B4A3-7E904A39C120","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"92b24916f8a190902c9f51557c21e619c4626fe3","datavalue":{"value":{"entity-type":"item","numeric-id":4249897,"id":"Q4249897"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928656$6B6097F8-7D11-4B86-A16D-D9A83F19BE62","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c4fb53dc30cdc46111c93a6e7de143f2e9b39160","datavalue":{"value":{"entity-type":"item","numeric-id":4099229,"id":"Q4099229"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928656$C1CDBCAE-51C5-44E5-8AE2-A93C9A2C1489","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7eb04700ed5e4dc9ae265f641db7ca870734b6df","datavalue":{"value":{"entity-type":"item","numeric-id":1382154,"id":"Q1382154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928656$4CFBAE4D-EC7F-4F1C-9A72-ABE8F646B2B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eafad2279bcd1a1ddbebd2da7446bcd66e04d511","datavalue":{"value":{"entity-type":"item","numeric-id":1262754,"id":"Q1262754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928656$DAD5ADAE-7E1A-4109-9119-05867119563D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"04843464a3369615eab52a529e2b30351bdf49e4","datavalue":{"value":{"entity-type":"item","numeric-id":4412856,"id":"Q4412856"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928656$07AFD7BD-33CF-4D0B-91BE-07A7556729FD","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":"Q928656$785A6446-5914-4CDD-959D-9E8BBF3C6854","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cd41301b78a03236dc27ccdfce83b246065d0cdc","datavalue":{"value":{"entity-type":"item","numeric-id":2751380,"id":"Q2751380"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928656$E57DE859-141D-49F5-BAB8-C3EFF34E087E","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":"Q928656$3B16A6A7-E86F-4DA2-899B-08125CCEABB1","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":"Q928656$119E4992-6862-40B3-9F1A-084711D7B064","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f14878b4342799995051ac9bc54cd21c98efc98","datavalue":{"value":{"entity-type":"item","numeric-id":2751359,"id":"Q2751359"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928656$18AF9CA9-19CF-414D-89FD-4B5C34004AA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fb29642056d3477aeaf6c3c32644b5d38b09eeac","datavalue":{"value":{"entity-type":"item","numeric-id":3613404,"id":"Q3613404"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928656$B7AF1803-A7EE-4952-B9EA-19AB34C4F075","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"2fdd3cf52fbf8294de127219362d1db48a7e3e1b","datavalue":{"value":"10.1007/S10817-007-9089-7","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q928656$039378F5-1CA0-4E62-BAA3-A8E6EC885378","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8182d19625309e7d46cdf95dbe9574e24d5d7503","datavalue":{"value":{"entity-type":"item","numeric-id":3613404,"id":"Q3613404"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dae78ed70c3a37a92d95847aa932566837cc31ee","datavalue":{"value":{"amount":"+0.9225788712501526","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":"Q928656$4E418F26-D239-4A14-8984-C134E781F5CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c86f80878e3d6987e2d89acaf5e00e9e68411b0e","datavalue":{"value":{"entity-type":"item","numeric-id":5698235,"id":"Q5698235"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b51ab3eb05a9ae90cac20adc3525135e554c6c4b","datavalue":{"value":{"amount":"+0.7929174900054932","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":"Q928656$4387C738-693F-4A3D-B933-53BDBD93B265","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"574c234d136db95e089adaee97950623853f74a9","datavalue":{"value":{"entity-type":"item","numeric-id":877889,"id":"Q877889"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a2a4b2ad703c1cdf8cd6c944c9e91f1e95c8a6d8","datavalue":{"value":{"amount":"+0.7769571542739868","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":"Q928656$839905C2-748D-4593-A2EE-AC3113C4D2A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fc81a6f30bea8e28f0da30a991f272eca7dabe41","datavalue":{"value":{"entity-type":"item","numeric-id":3608795,"id":"Q3608795"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3d5b258cc89c801bf3e0c7cd86b3dd71a15f75d2","datavalue":{"value":{"amount":"+0.7755571603775024","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":"Q928656$C45D553D-4AE0-4928-95B6-ECE858F99C69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fed39a206a07c7b5b7dfb40c30153123a625560d","datavalue":{"value":{"entity-type":"item","numeric-id":3406685,"id":"Q3406685"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"07e8e108fc7f006da3b1aeecae0694213c714863","datavalue":{"value":{"amount":"+0.7750567197799683","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":"Q928656$23B1BD3B-227A-460F-858A-98D8DE08F641","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Connection tableaux with lazy paramodulation","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Connection_tableaux_with_lazy_paramodulation"}}}}}