{"entities":{"Q2333858":{"pageid":2344601,"ns":120,"title":"Item:Q2333858","lastrevid":78964145,"modified":"2026-05-06T12:50:21Z","type":"item","id":"Q2333858","labels":{"en":{"language":"en","value":"Set-blocked clause and extended set-blocked clause in first-order logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7129531"}},"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":"Q2333858$694A112B-3C91-4083-AA44-74E62FD8294B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ccaf9c1d58f2af901a9668ce552eef675c2fcfc4","datavalue":{"value":{"text":"Set-blocked clause and extended set-blocked clause in first-order logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2333858$8E7F7052-6DED-446F-ABD3-4C5A5B32A91D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"fc72214714eee684901e1bcb1836cbcaefbffae3","datavalue":{"value":"1437.03118","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333858$ECA6623E-6D85-4F0A-8A12-B79BF9AB2F4F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"172732add4916bf3bf41fe85b7b2008cb9769c94","datavalue":{"value":{"entity-type":"item","numeric-id":2333856,"id":"Q2333856"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333858$0FF57C53-C9AD-4E74-BD79-AAFC8E288E03","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ee6429993c4b83380d2aa1a3eca2b98f393effbe","datavalue":{"value":{"entity-type":"item","numeric-id":209286,"id":"Q209286"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333858$C6D17F5D-8912-4921-B7EB-49DF4F3AC53C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d356adca328e50aa4488b6ecdb1b28ac263ee6b2","datavalue":{"value":{"entity-type":"item","numeric-id":2333857,"id":"Q2333857"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333858$AB172B2C-1555-45E4-9B5E-53D8B0F5C81B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1a0e95573879f5e8bd8c492340f9e6aafcee02b1","datavalue":{"value":{"entity-type":"item","numeric-id":682720,"id":"Q682720"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333858$61DE7DC2-7A4E-4F0B-8CE5-AFE7C0A6903A","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"536de48637c235d08fe3e176612e997aba7a2c18","datavalue":{"value":{"entity-type":"item","numeric-id":83462,"id":"Q83462"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333858$E416359A-4549-4E29-9E3A-366F4A38BA23","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"cce5560f694216ba99b4e4d50a7d9bab949bc76c","datavalue":{"value":{"time":"+2019-11-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2333858$61898E64-FA52-4CD7-BF81-DED6751F4538","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"6660ed5149656e0dbdc28270ee8f28ab9fdf8c97","datavalue":{"value":"Summary: Due to scale and complexity of first-order formulas, simplifications play a very important role in first-order theorem proving, in which removal of clauses and literals identified as redundant is a significant component. In this paper, four types of clauses with the local redundancy property were proposed, separately called a set-blocked clause (SBC), extended set-blocked clause (E-SBC), equality-set-blocked clause (ESBC) and extended equality-set-blocked clause (E-ESBC). The former two are redundant clauses in first-order formulas without equality while the latter two are redundant clauses in first-order formulas with equality. In addition, to prove the correctness of the four proposals, the redundancy of the four kinds of clauses were proved. It was guaranteed eliminating clauses with the four forms has no effect on the satisfiability or the unsatisfiability of original formulas. In the end, effectiveness and confluence properties of corresponding clause elimination methods were analyzed and compared.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2333858$0B6802BF-858E-42CC-BED8-60C0809BD562","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333858$5260172A-472B-48C0-A0EC-478D3E7E31FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"62ae2f4e9717dc72a20d2c4f17bdde30d85a417c","datavalue":{"value":"68T27","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333858$C555B538-E29E-4DA9-AFD5-0F13D7809A79","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333858$5DC589E0-1B90-4CA4-893A-49739365B04C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1ec2133de22b9154bfae76b0b88648af96d31561","datavalue":{"value":"7129531","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333858$8A6EFC06-09F6-4121-B824-DC94ADDC3263","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7a5eb6b1bc035b0acc88a184598dd6e3ce517044","datavalue":{"value":"set-blocked clause","type":"string"},"datatype":"string"},"type":"statement","id":"Q2333858$68AE577E-C44A-4079-8184-33ADE463289F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b0885305429d6a27b443acbf4f477ccc1c97c102","datavalue":{"value":"extended set-blocked clause","type":"string"},"datatype":"string"},"type":"statement","id":"Q2333858$E86AD335-5F80-4BE6-A3CC-5AB5C406B305","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e2e80a7123e4ea6d0418cb24d37b1837f13e3514","datavalue":{"value":"first-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2333858$247B2F23-D019-4EEE-9635-E784299ACA91","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b443b776731e3bc75eb79b752e7ef8c4cee2d97a","datavalue":{"value":{"entity-type":"item","numeric-id":15455,"id":"Q15455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333858$3923A8A4-B2A9-49EB-BC05-78713D31CD68","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bbe2b9a97ce0ea3098b4e4971345da27fad3d33e","datavalue":{"value":{"entity-type":"item","numeric-id":39735,"id":"Q39735"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333858$F4ED552F-8C67-4BCB-A408-40AB60BC1E6C","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":"Q2333858$F9F3D2EE-29E6-4B64-A487-98CE584DD7A4","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"1a8d91054f24fda592949b6d74d5541ce24c7357","datavalue":{"value":"https://doi.org/10.3390/sym10110553","type":"string"},"datatype":"url"},"type":"statement","id":"Q2333858$3FE5E72F-CC76-4BB0-AEEE-88C44A03FFB7","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"11c20f82440966d5eb213380e4a91828db7fda1b","datavalue":{"value":"W2898993032","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333858$9A0C1621-D999-4836-93D7-828CF7713CD7","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"4bcb0e71d083cf8486de0b4db45626afe5608e21","datavalue":{"value":{"entity-type":"item","numeric-id":3557074,"id":"Q3557074"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333858$994722A5-3E12-4364-BFB2-155E2A599407","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4140c1175bddc4c685fd37c0a5c7adcd0a184434","datavalue":{"value":{"entity-type":"item","numeric-id":4933317,"id":"Q4933317"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333858$BB0FA86F-9AF1-429C-8551-FE8E2BFEC804","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"87be12daaa9049d37eba12568fd639bb8a1c86c9","datavalue":{"value":{"entity-type":"item","numeric-id":2908507,"id":"Q2908507"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333858$D24CC533-6587-417C-9A8C-3A80CF300191","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f0895a6a6467bd1c6c67d2e7e17631989b0b2fd","datavalue":{"value":{"entity-type":"item","numeric-id":2870145,"id":"Q2870145"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333858$927C3619-4D66-4D3B-ACEB-EFD20B9A306C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ab7e8358f58e1397be654c43936d21c1d809ce15","datavalue":{"value":{"entity-type":"item","numeric-id":2817910,"id":"Q2817910"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333858$A0BCC5BB-0CFC-400F-8451-B8DC7FF97BBC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a92b8c20a31b5a186e0b862f25a0fd9399274371","datavalue":{"value":{"entity-type":"item","numeric-id":4645725,"id":"Q4645725"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333858$293EFDB0-7321-4857-AAAF-BC54FB3AFB11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"33ec6a38e62b229158ba6796c81864271d359e34","datavalue":{"value":{"entity-type":"item","numeric-id":2405255,"id":"Q2405255"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333858$89945DCE-946F-451E-B90E-0659F1EFADC3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f829d586193236a297f70521b500446992eec7c3","datavalue":{"value":{"entity-type":"item","numeric-id":2818027,"id":"Q2818027"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333858$129C27A6-8B88-47FB-82A7-631EB16195C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"819a2535befb2a67f49ee5e43432525215be36de","datavalue":{"value":{"entity-type":"item","numeric-id":4702972,"id":"Q4702972"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333858$269E1BF7-B7DD-4C2D-94A2-76C7FC8B4340","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"a09ac4fd98c2241a82102745712e76e5ebe51930","datavalue":{"value":"Q129076056","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333858$B58BEA66-F7F9-4FF7-8F95-DC36D32BC0E2","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d460f53a1e78fcb380b5abd6dbf19306b78e8536","datavalue":{"value":"10.3390/SYM10110553","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333858$DA4FBB3A-A910-4211-A926-4D346BA08AE4","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bc9474be161f6187e0cec91908d618efacc7f26b","datavalue":{"value":{"entity-type":"item","numeric-id":4645725,"id":"Q4645725"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ccb346097af1dd64e29232f35bb6b74e94ebc91b","datavalue":{"value":{"amount":"+0.8341818451881409","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":"Q2333858$2124496A-1F99-4868-A3B2-46E426C477B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"549b9e28b5019c300f5c4b14bd9068fe844a6300","datavalue":{"value":{"entity-type":"item","numeric-id":5128050,"id":"Q5128050"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"146820a630aec08a667aa005b456d2fdf2b55901","datavalue":{"value":{"amount":"+0.820309579372406","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":"Q2333858$4798F053-9061-479E-8838-A3DF56EAD71E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"689877375047fe87a7bcddf1d00855207cca824e","datavalue":{"value":{"entity-type":"item","numeric-id":4553279,"id":"Q4553279"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1ded945a9f1f45b9bbe6e1d9d243bda4a3891440","datavalue":{"value":{"amount":"+0.7899906039237976","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":"Q2333858$D2C55234-6F24-492D-9BCD-F502679928E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"af71dab54da42201412a717e4afe28e633bb38f7","datavalue":{"value":{"entity-type":"item","numeric-id":2817910,"id":"Q2817910"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"df6a5322eb3e3b050c84d6d5848bab8a5e84ea96","datavalue":{"value":{"amount":"+0.7749691605567932","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":"Q2333858$67D7625A-675B-4140-A4D0-86085ED6F65D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0d9ee3fedb306e15b25ac18e1c056a5542779645","datavalue":{"value":{"entity-type":"item","numeric-id":2405255,"id":"Q2405255"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ce30f67c6a66102df2920e4f950408f3d2a89a68","datavalue":{"value":{"amount":"+0.7681788206100464","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":"Q2333858$AC12ECB6-0069-465C-A1CA-AC4834EB2F64","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333858$2C2CD9EA-D6D7-47D4-B1EB-422B43199BC3","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Set-blocked clause and extended set-blocked clause in first-order logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Set-blocked_clause_and_extended_set-blocked_clause_in_first-order_logic"}}}}}