{"entities":{"Q1060210":{"pageid":1070962,"ns":120,"title":"Item:Q1060210","lastrevid":69756813,"modified":"2026-04-13T09:11:08Z","type":"item","id":"Q1060210","labels":{"en":{"language":"en","value":"Condensed detachment as a rule of inference"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3906475"}},"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":"Q1060210$C541A4BF-834C-48A4-AEC8-B17DAA5A24D4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"757c311e5bfb8a0f7b040590466f0a35d25735c0","datavalue":{"value":{"text":"Condensed detachment as a rule of inference","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1060210$8A106DFE-98DB-40E4-8248-AC55A82D6276","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5e06ff9a551f248fbf2330374c8f0d94c8fd7efe","datavalue":{"value":"0568.03010","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1060210$E5452E97-B7A8-4553-89B1-DCEEEBC0A029","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6836a89f982c14c89b4661c738e3c06700461264","datavalue":{"value":"10.1007/BF01371632","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1060210$3E35DD6E-B318-4E90-9EFC-3872B13E2205","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e34236ca73b92c6ee0bc17431d03c3537a7f0792","datavalue":{"value":{"entity-type":"item","numeric-id":195358,"id":"Q195358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1060210$9A67C892-B155-431E-BD7C-DFBA055D32C0","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0136733d5dd7d9f4d36f24c87a0b8375ae1cb2fd","datavalue":{"value":{"time":"+1983-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":"Q1060210$C202C15A-9198-40C7-AD72-E79BEFAF2ACB","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"1210e74cf6ef2ab72589be46c3312d8a3c0d6d3c","datavalue":{"value":"Condensed detachment is usually regarded as a notation, and ''defined'' by example. In this paper it is regarded as a rule of inference, and rigorously defined with the help of the unification theorem of J. A. Robinson. Historically, however, the invention of condensed detachment by C. A. Meredith preceded Robinson's studies of unification. It is argued that Meredith's ideas deserve recognition in the history of unification, and the possibility that Meredith was influenced, through \u0141ukasiewicz, by ideas of Tarski going back at least to 1939, and possibly to 1930 or earlier, is discussed. It is proved that a term is derivable by substitution and ordinary detachment from given axioms if and only if it is a substitution instance of a term which is derivable from these axioms by condensed detachment, and it is shown how this theorem enables the ideas of \u0141ukasiewicz and Tarski mentioned above to be formalized and extended. Finally, it is shown how condensed detachment may be subsumed within the resolution principle of J. A. Robinson, and several computer studies of particular Hilbert-type propositional calculi using programs based on condensed detachment or on resolution are briefly discussed.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1060210$7951BB91-AB2F-4810-98F7-28FC7F23B56B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1060210$45CD64D9-2735-4909-B8BC-2A2108219AD7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"920d53b3830654b0eb4e3a87ec3396145f924723","datavalue":{"value":"03-03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1060210$C7CD970E-5888-4178-A31F-2E341DBCC1B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"855dfff3c52593115343606bc2418a3b17e5a003","datavalue":{"value":"01A60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1060210$05707574-8A4C-4176-8B5E-F58B3BE8C1A8","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"46ac1cb5230f423ba38bc8238f34ea22c088033d","datavalue":{"value":"3906475","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1060210$237FECC9-3CE6-40B9-9F01-EA44C52731A8","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dfd68d466588eedfb479d028833ceea07a63e587","datavalue":{"value":"unification theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q1060210$C5E6FE1D-093E-44CA-94B6-8DDBEDBCFADB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c944089ebd99d6195538b901db0229fcb390018b","datavalue":{"value":"resolution principle","type":"string"},"datatype":"string"},"type":"statement","id":"Q1060210$06430490-3150-466D-A43D-2E08EAA95BDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b7b483c42dc25c21025d13069c50e0c6476284be","datavalue":{"value":"computer studies","type":"string"},"datatype":"string"},"type":"statement","id":"Q1060210$1BD10CD1-3428-4FE5-A49E-93B6A5F0A7C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"34b72e2dd6c0b91ec7e8720bbb1ea5fad58ec957","datavalue":{"value":"Hilbert-type propositional calculi","type":"string"},"datatype":"string"},"type":"statement","id":"Q1060210$3CE07591-E275-4A86-B203-E1C699A949A1","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"028d9d257050f359a2a147a0de48cf680ceb3e9c","datavalue":{"value":"Q29541784","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1060210$512CF49E-9A28-40A7-8F48-67F5AE22AA0E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"09ff7eb290cc56671cb0c745dcf7f762ebe791a1","datavalue":{"value":{"entity-type":"item","numeric-id":1242882,"id":"Q1242882"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1060210$E60ED2B8-2314-484D-9285-6B13E542C072","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":"Q1060210$29890702-9EE5-4AAC-B9A7-8553EF02B6B3","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c0e6b90c16ae5fa1eac19212a306cb84ffec72b","datavalue":{"value":{"entity-type":"item","numeric-id":5613969,"id":"Q5613969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1060210$7521B586-298A-4518-ADD7-60B22C23AEF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1716d62fb176f9fbe0816f24dd1cdfd1df8f895d","datavalue":{"value":{"entity-type":"item","numeric-id":4115125,"id":"Q4115125"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1060210$562F9537-DE2E-4F62-A9F4-4738F6064DAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ac2e1730505dc38b28b0c175adb4ff33adc97db1","datavalue":{"value":{"entity-type":"item","numeric-id":1242883,"id":"Q1242883"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1060210$D997609E-4278-4CAF-BF7F-0B286425D745","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"79bc319399a3289778f626f8d9a952e64152712e","datavalue":{"value":{"entity-type":"item","numeric-id":799664,"id":"Q799664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1060210$037980DE-0FC6-4833-B10F-AB1013038A02","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"16d1c043035191d540c37555c23f0303b7675915","datavalue":{"value":{"entity-type":"item","numeric-id":3241192,"id":"Q3241192"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1060210$17B8B5D0-7875-44A5-BCCC-D38BB45069E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"58c995625a3d6ef326eb2c5f18f7cd9368736ae0","datavalue":{"value":{"entity-type":"item","numeric-id":1237711,"id":"Q1237711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1060210$13EB2380-D8A5-4776-B90C-99942F0ECF47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1c0f6d624793f6925eb62286145797be3cb2786a","datavalue":{"value":{"entity-type":"item","numeric-id":5555705,"id":"Q5555705"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1060210$0D4DC1B8-FBC2-4BA0-B9BF-A2D277779C03","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9c0f5d8160663dcf3896a10288f16c979160b94d","datavalue":{"value":{"entity-type":"item","numeric-id":4095908,"id":"Q4095908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1060210$8A69BBE5-F571-4CD4-BCFC-2A4C15417FA3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"871eeb072064268812d71252bf2535d5e9ad8d8c","datavalue":{"value":{"entity-type":"item","numeric-id":1242700,"id":"Q1242700"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1060210$6005A36A-BEC6-4D83-A13D-E9134AFD39C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62e82257b416db4246a715182cdefecc0570e41d","datavalue":{"value":{"entity-type":"item","numeric-id":3279281,"id":"Q3279281"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1060210$D4936A4B-4A49-4322-B297-DCDC222B03AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f62ebef9379ad97d2bdc3c2e7f5717f221d056cb","datavalue":{"value":{"entity-type":"item","numeric-id":5514129,"id":"Q5514129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1060210$CCAAAC37-8063-4631-BDD3-ABE4291DBCD6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dd7f4ac2c4d2314fae83403dbcb7eab5f78434cd","datavalue":{"value":{"entity-type":"item","numeric-id":3864488,"id":"Q3864488"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1060210$C6AC5949-3AD0-4182-A6B8-8BE20B537971","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5c2691d858e4397db5d79d5923363d0a30db8142","datavalue":{"value":{"entity-type":"item","numeric-id":3853703,"id":"Q3853703"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1060210$6EE7B49D-6B81-4FB5-B4A3-8D31A1311BDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5700cb31135742c28553eda28989b80f165cc32d","datavalue":{"value":{"entity-type":"item","numeric-id":1165832,"id":"Q1165832"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1060210$D1E1EBCC-81C7-4D19-BD39-7DB5D0A460D3","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"32337f4f9983526df9e0468f6b8bff805af0954d","datavalue":{"value":{"entity-type":"item","numeric-id":799664,"id":"Q799664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b9f6d6b67eb5b2d56a2111c226e126e56a2106dd","datavalue":{"value":{"amount":"+0.8130882382392883","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":"Q1060210$DF99E28C-3339-46D6-8BCD-31A77C764494","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4166e17fbdeeddb801569cb7c71ca9bef0cc5872","datavalue":{"value":{"entity-type":"item","numeric-id":1181717,"id":"Q1181717"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a06d6f4ac72e0175a417984ce2a1e53821dc5427","datavalue":{"value":{"amount":"+0.7883210778236389","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":"Q1060210$3FA973DF-395C-4254-B415-E48FFB5AE603","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"17fb10eef86dcfda8132d6736057f7094945ee18","datavalue":{"value":{"entity-type":"item","numeric-id":1903086,"id":"Q1903086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0b32d5b1ae0f53d0a5fe028b251ffd7cdea4d32c","datavalue":{"value":{"amount":"+0.7857391238212585","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":"Q1060210$955E2218-9F43-4527-9711-D106A81D71AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"85a02bafe836cd0b9491400fe4965a117bf50b68","datavalue":{"value":{"entity-type":"item","numeric-id":4218026,"id":"Q4218026"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2a897fd9b4b127d1e3c1854257323ff244463088","datavalue":{"value":{"amount":"+0.7609297037124634","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":"Q1060210$0A136CD6-0E49-4AF1-8B12-57E17087C8EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9bb0d0ae59343cb96fca8d4fd6b3a0b5b6181400","datavalue":{"value":{"entity-type":"item","numeric-id":3682462,"id":"Q3682462"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fb9c3f6f5f90de7b0bc5e42f7a7a4c5b59801c7f","datavalue":{"value":{"amount":"+0.7566357851028442","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":"Q1060210$147F7AEE-F9F3-430C-94CA-B2BC8D767051","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Condensed detachment as a rule of inference","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Condensed_detachment_as_a_rule_of_inference"}}}}}