{"entities":{"Q1181717":{"pageid":1192466,"ns":120,"title":"Item:Q1181717","lastrevid":67050207,"modified":"2026-04-12T14:35:40Z","type":"item","id":"Q1181717","labels":{"en":{"language":"en","value":"Condensed detachment is complete for relevance logic: A computer-aided proof"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 28718"}},"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":"Q1181717$04D62A28-8FF5-462E-8A3B-9CBC554C3579","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cd7c743cb879b92794fef6f0a3698947e5178527","datavalue":{"value":{"text":"Condensed detachment is complete for relevance logic: A computer-aided proof","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1181717$960490A8-7D47-4A52-919E-22A1E24DF0C0","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d56a39df4d265030cf0fa8865731e4d61966edef","datavalue":{"value":"0751.03011","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1181717$ABBFCA34-87CE-4466-B09E-63D87305F329","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f99c6291129efc6bb3d8375bcc5027dfbee2098f","datavalue":{"value":"10.1007/BF01880330","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1181717$8E858FE8-D13D-456E-9A5A-9722F88AEF5C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"50dfba14eecf8f7e9f64ea004fb9b72dca6eb33f","datavalue":{"value":{"entity-type":"item","numeric-id":1181716,"id":"Q1181716"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1181717$846C1636-1141-4354-88D2-09A32BE54EB3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"739bb59f926e46bf270e3affee77bc2ef6969661","datavalue":{"value":{"entity-type":"item","numeric-id":454365,"id":"Q454365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1181717$7C324881-BE2E-4DD0-AF31-B9B7B48924C7","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":"Q1181717$37376169-59E5-4A5B-9E6A-ECE4E93E5AA3","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"70844ffc4666eabac4e20376c648613dbe8620f7","datavalue":{"value":{"time":"+1992-06-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1181717$699F9A3B-6C48-48FF-A562-4F5C0B77A428","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"8af2972bc5776dfeb09fa0f88cbfa95d21fdbe4b","datavalue":{"value":"The condensed detachment rule \\(D\\) is a combination of modus ponens with a minimal amount of substitution. Earlier \\(D\\) has been shown to be complete for intuitionistic and classical implicational logic but incomplete for \\(BCK\\) and \\(BCI\\) logic. We show that \\(D\\) is complete for the relevance logic. One of the main steps is the proof of the formula \\(((a\\to a)\\to a)\\to a\\) found in interaction with our resolution theorem prover. Various strategies of generating consequences of the axioms and choosing best ones for the next iteration were tried until the proof was found.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1181717$18F1D8C5-80A8-4CA0-B120-E60EE392235A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"b363e494c684597e57f0cc15c7c0d8f9f3bcf9fc","datavalue":{"value":"03B47","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1181717$360B8E69-CB76-489B-B796-3B600A432127","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1181717$5A923E19-1E0B-4C5D-A274-E05B8D672D11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1181717$23631D85-F3A6-42F7-8588-DF4F58BE8535","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d8724ac1f861fd4485a474d1844744a1ace24834","datavalue":{"value":"03-04","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1181717$5A8620E4-9ACC-4A53-A9FC-B7F0D40ED7E8","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"19686b0c1cf39ac1a47b8ca77c2e845bca1f87a9","datavalue":{"value":"28718","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1181717$9B2B70E7-176C-4C5A-878E-A28E9AF68EC1","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8372871e08a63e6423cd949e432f3da9e158d3b1","datavalue":{"value":"condensed detachment rule","type":"string"},"datatype":"string"},"type":"statement","id":"Q1181717$27FB800A-09E4-4BAD-8143-945DB805C73D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ce4feea89835b46b1433881e67cdd6f181cb49b8","datavalue":{"value":"relevance logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1181717$07B066E2-2383-4B73-934B-ACEF4335A101","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"8f432bccb81d11b6d0c5be5373ba82abf19c1967","datavalue":{"value":{"entity-type":"item","numeric-id":454365,"id":"Q454365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1181717$21916932-0839-4BB0-B6A6-6D17EEB44836","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":"Q1181717$53599740-1B0B-427E-AC59-9155970AC522","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"82c7ff17d186eeec961fee84f228f3f7d74176a9","datavalue":{"value":{"entity-type":"item","numeric-id":1106836,"id":"Q1106836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1181717$8C760BD7-BCAF-4E8B-8A11-E8AFB0FD1C5F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ae542aa49195da2f0564220c3e6d6c6c5762344","datavalue":{"value":{"entity-type":"item","numeric-id":769601,"id":"Q769601"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1181717$084CF82D-DA1A-40E9-BB99-86C656932C26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d18ca94c9b6fbb6087987abf23a68e215a4b57a","datavalue":{"value":{"entity-type":"item","numeric-id":1237066,"id":"Q1237066"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1181717$75D178BA-C2EC-48E8-9BD6-21219F5C84CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0b570dc51ad23d1e9cb47c7083a0b7b043b06071","datavalue":{"value":{"entity-type":"item","numeric-id":5592242,"id":"Q5592242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1181717$AA045FB9-8E16-455A-83EC-33D0DAD13FD5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9fe3b02d54ba595ff22780f05fff04326cc851a3","datavalue":{"value":{"entity-type":"item","numeric-id":3489979,"id":"Q3489979"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1181717$4B95C017-C5A2-4BF1-98AD-4CEA2E7B0ECB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"25313d367058edb8143ccf81859fe214d888d1ea","datavalue":{"value":{"entity-type":"item","numeric-id":5723175,"id":"Q5723175"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1181717$B89069EE-AD90-4929-8AF5-7675FD01A3AC","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":"Q1181717$82E1AA4B-1F74-4FF1-AD97-FD9FE1E89920","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"017c184c3277fb681aa54b180b0d3db5f9e6933c","datavalue":{"value":{"entity-type":"item","numeric-id":3348885,"id":"Q3348885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1181717$16B80693-4C4C-4FBD-914A-F949EE2D30CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f144c40fe3a1847d11917e0d6609f6f9818cf1d8","datavalue":{"value":{"entity-type":"item","numeric-id":583187,"id":"Q583187"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1181717$D1284DF7-CCF7-4A35-9D27-1488C99AD18E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"83112173833ccd7f5cecd703f71e4ba8bb4e3e6a","datavalue":{"value":"https://doi.org/10.1007/bf01880330","type":"string"},"datatype":"url"},"type":"statement","id":"Q1181717$3E533FA7-16F9-4801-869D-250DAA6EF0E2","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"71582aaf780f63c98652a113cb0319ac800acfd8","datavalue":{"value":"W2053760476","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1181717$CA22B4E3-FE7E-4947-85B7-C28A5E525878","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bd9184a593d566a0a980015770c52e4dbd78de80","datavalue":{"value":{"entity-type":"item","numeric-id":3466593,"id":"Q3466593"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2135c25e04aefc494fdeb2cc0923e25674d972fa","datavalue":{"value":{"amount":"+0.8045780062675476","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":"Q1181717$98EFFCCB-84D5-41D8-ABC9-9799D4A57A44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9e21d551ed4c80884fe63570495ef844d615f4c9","datavalue":{"value":{"entity-type":"item","numeric-id":1060210,"id":"Q1060210"},"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":"Q1181717$24469CF1-A3F1-497B-B89F-B816A9C9D5B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"073941fe171251f742afe8160161189f34dde366","datavalue":{"value":{"entity-type":"item","numeric-id":3489979,"id":"Q3489979"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c46345338123aaa53d53fa308831029385f124a3","datavalue":{"value":{"amount":"+0.7702889442443848","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":"Q1181717$E97C3209-E19C-40BD-B6EA-EF19C8FB9F80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dee548f2490da7e1eebb2956e490cd4a543c7c2e","datavalue":{"value":{"entity-type":"item","numeric-id":4877446,"id":"Q4877446"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"47ebf54a88a363230de6c006f45e4323f19f5338","datavalue":{"value":{"amount":"+0.7682173848152161","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":"Q1181717$6E0E5E82-1BED-4B50-B153-BA0D712238B5","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":"059a11d113a6e54e93d9c9ed823a32753b6d2772","datavalue":{"value":{"amount":"+0.76457279920578","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":"Q1181717$EB3E6768-CDB9-40EA-980B-2C18E97FF3D9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Condensed detachment is complete for relevance logic: A computer-aided proof","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Condensed_detachment_is_complete_for_relevance_logic:_A_computer-aided_proof"}}}}}