{"entities":{"Q1961453":{"pageid":1972195,"ns":120,"title":"Item:Q1961453","lastrevid":72038751,"modified":"2026-04-14T02:15:19Z","type":"item","id":"Q1961453","labels":{"en":{"language":"en","value":"The symmetry rule in propositional logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1389870"}},"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":"Q1961453$AEE3680A-9088-40E6-A602-E69F53E7A6B2","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7d9e6d324e626ae24dbcafa5ca72d04a17a6e3ca","datavalue":{"value":{"text":"The symmetry rule in propositional logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1961453$25D1AC1F-DF03-4B70-9066-DE9032969831","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9fbb69044f5fd5b69e90e0346bcdfe891ea1f94c","datavalue":{"value":"0938.03023","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1961453$44D1B3A6-FA5E-4245-8A7D-6537CFFCA1EE","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"03f543d27999bb869631789a475553314a60b8cf","datavalue":{"value":"10.1016/S0166-218X(99)00039-6","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1961453$B088B72A-1B9A-479C-82ED-D637B554F5C3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ffd6a40ad54574dfdc72407e5223fefee18b3ec7","datavalue":{"value":{"entity-type":"item","numeric-id":647404,"id":"Q647404"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1961453$3BC834AA-A012-4210-A78C-6C7693CD1F9C","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"087f55844cc920aae060b09644168bf17b022e1a","datavalue":{"value":{"entity-type":"item","numeric-id":96294,"id":"Q96294"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1961453$3F3D9D84-5BD4-4665-89A9-29F98F887BD9","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"71e784f7cfaa48fae228ecd4530139eb05d7e87c","datavalue":{"value":{"time":"+2000-02-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1961453$6CD9D228-B538-4F1A-9F9E-D18AF61C2A98","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"14e45c11c63fd2c1c9efc8c872251a3190237356","datavalue":{"value":"The addition of the symmetry rule to the resolution proof system sometimes allows considerable shortening in the length of refutations. An exponential lower bound on the size of resolution refutations using two forms of a global symmetry rule is shown. The paper also discusses the relationship of symmetry rules to the extension rule that allows the use of abbreviative definitions in proofs. Also, symmetry of random clause sets is considered.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1961453$D4882593-91D4-4929-AC05-029A748406AE","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1961453$2B35BB58-484C-4393-9881-669058556060","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"419d6f2b09c39920e34f63114ff159a2f0a01812","datavalue":{"value":"03B05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1961453$76F8DE56-83B8-4AB6-B1DC-29813AE0F8B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1961453$4AEFAC75-1042-410F-942F-1A51CB5EE700","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1961453$3F304B82-1B21-48EC-8FF3-DA2141405B65","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2460a7e57ef150aa4dc8e55ddc9b8f9aadecad70","datavalue":{"value":"1389870","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1961453$6EBC292D-1117-4070-96DD-0924C8FC692F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"480f8686db1b53b6d5e9c0946ff9fe87ca48a783","datavalue":{"value":"symmetry rule","type":"string"},"datatype":"string"},"type":"statement","id":"Q1961453$CAC42B9C-C878-41DC-B84F-BCCDE6FAD8AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c1db30a9ed17d7c25b3fe8c952d249a6bdd32a36","datavalue":{"value":"exponential lower bound on the size of resolution refutations","type":"string"},"datatype":"string"},"type":"statement","id":"Q1961453$9A409851-E2B8-4703-9782-646112DD2323","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"42c9c64d0b9070e32b1957f7e6f3c7e8f11356c9","datavalue":{"value":"extension rule","type":"string"},"datatype":"string"},"type":"statement","id":"Q1961453$CD0E1481-8EC8-40D2-AD83-3A65E9266F52","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"11a7a71816cc4d24b3c7d1d9e579c23a4764afd1","datavalue":{"value":"random clause","type":"string"},"datatype":"string"},"type":"statement","id":"Q1961453$AFE6DE46-3583-4A07-85E6-9C06CEF42421","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":"Q1961453$99B5B093-2355-4C5C-906C-8348DDF769FF","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"5035ead90ebf2e92af4cb88fdfc91c7dfa88c06a","datavalue":{"value":{"entity-type":"item","numeric-id":920967,"id":"Q920967"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1961453$78E6B29C-C392-4042-BFD0-C846093AA3B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0c6c338f74f8724c3697d5b86b62f3375f4fb35b","datavalue":{"value":{"entity-type":"item","numeric-id":1253482,"id":"Q1253482"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1961453$851B3A51-7CE7-4F4C-BBA9-C056D1E9D9D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"91c636dd583a22faf929d1cb972aae014f779c04","datavalue":{"value":{"entity-type":"item","numeric-id":3496310,"id":"Q3496310"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1961453$C3BE1343-7D89-46C7-BE58-50B71455F1EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0bea75da9fa67a5f77faa9362cd4aa6c737c792a","datavalue":{"value":{"entity-type":"item","numeric-id":4194955,"id":"Q4194955"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1961453$087A672D-7826-4B00-AFB6-91BEDFF9D532","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a8c3fb0ef3c7cbeb1b19e8a3632e3bd5fcfcda10","datavalue":{"value":{"entity-type":"item","numeric-id":1165257,"id":"Q1165257"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1961453$B6D3FA1A-D402-4116-8168-417E5ADFC66F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a35cc55e5b10a424a85f3ddcd5c540cf5328ff0d","datavalue":{"value":{"entity-type":"item","numeric-id":1249435,"id":"Q1249435"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1961453$124426A5-8C9A-4ED7-98BD-C5743924580E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec2fa04d400281f100817ce7e13bdaafd2683670","datavalue":{"value":{"entity-type":"item","numeric-id":1071750,"id":"Q1071750"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1961453$A37CE284-175F-49F4-B274-55F6A04AE11D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"70dc07534eba676d59722b415a0bd27b41786f77","datavalue":{"value":{"entity-type":"item","numeric-id":5593643,"id":"Q5593643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1961453$4361B44A-5DAB-4241-9A11-1AF9EC168CDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"25f4a86512e0f02bf82877dbb62313fcd7fe9ed1","datavalue":{"value":{"entity-type":"item","numeric-id":3472096,"id":"Q3472096"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1961453$DA7A816E-DE19-4911-B99E-0E99E7ED9C01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9039c5b03ce44bd1ae984dac18752d8859c6d482","datavalue":{"value":{"entity-type":"item","numeric-id":800909,"id":"Q800909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1961453$C2406981-203D-4F9E-A96E-34947D530A0E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"728810277830424bd131e6e77eef399df584ccea","datavalue":{"value":{"entity-type":"item","numeric-id":3780485,"id":"Q3780485"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1961453$4D3DAAC6-1C72-4FFE-A20F-FF29EE170F0A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"acddcbbc7bbb65cd6789ce6d861571f4cbd168d8","datavalue":{"value":{"entity-type":"item","numeric-id":4873893,"id":"Q4873893"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1961453$102ECE92-DD40-4AC6-823D-4CB465087E24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"635b7cf0112ffb7accdf44d274d01dea7d61443f","datavalue":{"value":{"entity-type":"item","numeric-id":2542058,"id":"Q2542058"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1961453$414B6018-CC62-4028-80FE-D41D0426511F","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"adbd802b95b2202998eefbcc5635f8e06ec285ea","datavalue":{"value":"Q126297728","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1961453$F2313376-9C94-437C-A0E4-6F15FFF04F5F","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6d2751114c00a17d679338a004e070436da1909b","datavalue":{"value":{"entity-type":"item","numeric-id":2721182,"id":"Q2721182"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f56e7059acfe1cd236eb082bf229bdf4cf596ac7","datavalue":{"value":{"amount":"+0.8907361030578613","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":"Q1961453$CEA1DAFE-3062-4307-B532-3D4CD08FA1F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"eaf6d55f21836e77cdf181a7374cf30bb6d35fa3","datavalue":{"value":{"entity-type":"item","numeric-id":1771316,"id":"Q1771316"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7d1fbace7375ecf3a58cd96a64ed8e888e0937c8","datavalue":{"value":{"amount":"+0.8517013192176819","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":"Q1961453$BD5787A9-C51F-4663-8EAB-5F6E2DF88929","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f584b6e7aaa9f9e37c6f1d0079e14e6c14d9a6bb","datavalue":{"value":{"entity-type":"item","numeric-id":4418674,"id":"Q4418674"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2d429c902dac040d74191fa441b821d8f6bd31d4","datavalue":{"value":{"amount":"+0.8506953120231628","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":"Q1961453$7A2F6875-EC2B-43B5-96CD-83396971A3F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"978aaa6bd41dd861db1c8203a087e01f8c2c05af","datavalue":{"value":{"entity-type":"item","numeric-id":4282509,"id":"Q4282509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2fe82e161196e89afdf225969d575074b7bc81bf","datavalue":{"value":{"amount":"+0.8265033960342407","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":"Q1961453$53A20467-E47A-4899-BECB-3307DB0BA30C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cc9aef774386ccbf6024985cd7c37c9123be9e4c","datavalue":{"value":{"entity-type":"item","numeric-id":4264722,"id":"Q4264722"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"72814cf58e3e9024246570017e88e36b4f53faea","datavalue":{"value":{"amount":"+0.8016265630722046","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":"Q1961453$3FD015C0-25DB-4DC3-88E9-AA748CD62173","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The symmetry rule in propositional logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_symmetry_rule_in_propositional_logic"}}}}}