{"entities":{"Q1430904":{"pageid":1441644,"ns":120,"title":"Item:Q1430904","lastrevid":71934396,"modified":"2026-04-14T01:32:00Z","type":"item","id":"Q1430904","labels":{"en":{"language":"en","value":"Shortest axiomatizations of implicational S4 and S5"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 2067618"}},"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":"Q1430904$2FC38D84-1646-414E-BE73-D870A139A222","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a6603d0fd843560d78df23bf7c321403c3d3313b","datavalue":{"value":{"text":"Shortest axiomatizations of implicational S4 and S5","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1430904$AA9713F7-3131-4E90-85F5-20ADFED753EA","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"3303973fd524a8764bad31ae0b85ab34d9f3cb9d","datavalue":{"value":"1045.03021","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1430904$0010FDE0-4557-4A11-B5BB-926EB94E00AB","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9060f88dc742e238cf202ad8bd5b72b7e72eac5c","datavalue":{"value":{"entity-type":"item","numeric-id":1430903,"id":"Q1430903"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1430904$3B72E339-4F50-45F5-B248-EB4032F9761B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"73184fbfb3b21357608a76d8fcbf8bd57d0ccb8f","datavalue":{"value":{"entity-type":"item","numeric-id":185562,"id":"Q185562"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1430904$B0ADEC7E-3041-40A5-81D8-B5BE73B2AD08","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ba90afe3c39216a5a167db74b8f9f42ac7df8da6","datavalue":{"value":{"entity-type":"item","numeric-id":220717,"id":"Q220717"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1430904$AE8D8C3C-E326-477E-93B0-5D629F87516D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c2308b3789038a6996f4231da48d541ec5941c9d","datavalue":{"value":{"entity-type":"item","numeric-id":1732641,"id":"Q1732641"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1430904$885A1A57-BCCF-4921-B817-6CAD75A25704","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"6325d9f59cde8ebbdb24a9f950cab3fcef3decf6","datavalue":{"value":{"entity-type":"item","numeric-id":190248,"id":"Q190248"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1430904$42271C5F-25C9-408E-9458-F1855FC64054","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4ba9d052c1c742a2c2f9206a1b4282a8f44ef61e","datavalue":{"value":{"time":"+2004-05-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":"Q1430904$FB154119-CA4E-46D7-A7C7-98BA04BDB4B3","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"cf5553a9c84d48468454604479286d5ef9db96c4","datavalue":{"value":"The paper introduces several shortest possible axiomatizations for the strict implicational fragments of the modal logics S4 and S5 (which are usually denoted C4 and C5). The paper has three clearly separated parts: the first one deals with the axiomatization of C4. After a brief historical survey of the history of its different axiomatizations, two minimal 2-bases for C4 are given together with a single axiom base, solving an open problem first stated by \\textit{A. R. Anderson} and \\textit{N. D. Belnap jun.} [Entailment. The logic of relevance and necessity. Vol. I, Princeton, N. J.: Princeton University Press (1975; Zbl 0323.02030)]. Then, a similar section is dedicated to C5, for which a minimal 2-basis is given together with several shortest single axiom bases. All the proofs reported were discovered with the assistance of the automated reasoning program Otter. The final part of the paper outlines the approach used to obtain the results and the automated reasoning strategies used.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1430904$2402405C-9B2A-47EF-85CB-4627F9A5F83A","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"d9c7994377655925beca167212c6ec3527b954b5","datavalue":{"value":{"entity-type":"item","numeric-id":587084,"id":"Q587084"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1430904$61861FEA-DC97-4FE4-B272-A137365790C6","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1430904$ABB5D5A5-0B8B-4FAE-BE9C-7BC27A25D611","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1430904$B90CA1B6-3286-44DA-843F-28DCA9D7A0C7","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"25337aaebd1b894361f5a2dd3a89a52e27c6a274","datavalue":{"value":"2067618","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1430904$9A6B0E42-8BCA-420D-91E1-5EBABA8C5895","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f1dda010537b7b36bd45151721146f720815706e","datavalue":{"value":"modal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1430904$09AB09ED-2D33-4B28-B11D-7517E3B88C92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a7b468003be556f513188e1dda9b5610aa838e5a","datavalue":{"value":"shortest axiomatization","type":"string"},"datatype":"string"},"type":"statement","id":"Q1430904$99F5BBB1-A207-4DB4-8A73-A006FC8D2E27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"637cab94c87a5b556b1043f03f56b4600824940f","datavalue":{"value":"implicational fragments","type":"string"},"datatype":"string"},"type":"statement","id":"Q1430904$860FD6C1-9D8F-4B9B-A7B5-101BD3DB6574","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"824332795652099401741a9184ca69eea2b70898","datavalue":{"value":"Otter","type":"string"},"datatype":"string"},"type":"statement","id":"Q1430904$C1F58F58-02EE-48DC-A62C-4C9522C90946","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1ca1042868ff4f694776e4b2c62ec66638c4ef91","datavalue":{"value":"automated reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q1430904$F42DFABE-7FE3-4FED-9489-CABD8AA20E78","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"10f8a293be1162767f46766ba375aedc7213fbb9","datavalue":{"value":{"entity-type":"item","numeric-id":23808,"id":"Q23808"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1430904$ED4247D1-694A-415A-B53E-A01282E91108","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1e7b4d238eeafa5b21b1ef85a0d6b8900bfdc422","datavalue":{"value":{"entity-type":"item","numeric-id":15442,"id":"Q15442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1430904$B5E006C1-66C4-4C40-972F-197D8D2AA78F","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":"Q1430904$484FAA71-2908-414C-AE2B-4B7C1BCC74EE","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"49b4b8833f3c3b0853e3cd5d728c708c04e3e682","datavalue":{"value":"https://doi.org/10.1305/ndjfl/1074290715","type":"string"},"datatype":"url"},"type":"statement","id":"Q1430904$6164E441-BB41-498B-9827-E0924614B19B","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"4bc4d2e7cd4fe6a2fdf747e34c4ac6608e28109f","datavalue":{"value":"W1982503362","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1430904$4F2C4C53-3983-49DA-B19B-707B69B7BB90","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"3bd2941e29ef96af9670f01e50a8654b5699ebd3","datavalue":{"value":"Q114254311","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1430904$DF7641B6-1237-4B71-AB0B-BA401561A672","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"babcb2136f09546a315df53e15ed48a3be9ff116","datavalue":{"value":{"entity-type":"item","numeric-id":3849883,"id":"Q3849883"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1430904$8A3E3E03-16AE-439D-A1A8-F8ACE8D537D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec09860f6f4856a0bfa1fcbed713df420a357696","datavalue":{"value":{"entity-type":"item","numeric-id":4085699,"id":"Q4085699"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1430904$55599230-5415-47BB-9C6A-200FDBD153F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5f776a9049b5d345cc4d1d41aa1d8b454cafc141","datavalue":{"value":{"entity-type":"item","numeric-id":5341748,"id":"Q5341748"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1430904$A1A2A0A9-7B58-48C5-BBC1-7C19B16E19B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"76f25313d876ab3b03b6fb725c215cdb0768fa74","datavalue":{"value":{"entity-type":"item","numeric-id":4443196,"id":"Q4443196"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1430904$79F0B858-BA66-49AF-A6DC-D8C0396A6A65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9843c8ee14c0643e458996a068684041675ad668","datavalue":{"value":{"entity-type":"item","numeric-id":1060210,"id":"Q1060210"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1430904$EDFDA142-2A07-4DC4-8724-05201B70B10A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eaaee3a935b71da0c5fd895e355092a513197bd2","datavalue":{"value":{"entity-type":"item","numeric-id":3265659,"id":"Q3265659"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1430904$27ECE7C0-F39D-44AA-AAA6-40A8633601A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e1d3666c5bbd99de8087f2e6f94b3094e911f888","datavalue":{"value":{"entity-type":"item","numeric-id":2496167,"id":"Q2496167"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1430904$45689E6B-90BC-49DA-8EE6-1FAD172119A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bedafda8a6cf5bbd75a44132bc72f5398e245db5","datavalue":{"value":{"entity-type":"item","numeric-id":5522918,"id":"Q5522918"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1430904$4AA8E430-CF5B-44B7-A999-E84ACEF4623E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7648fffa5032202159fe1c747e972ef89b013bb1","datavalue":{"value":{"entity-type":"item","numeric-id":5675344,"id":"Q5675344"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1430904$799A9B50-BB37-475A-87F9-069D767A08B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"551422936a59120f181f13e988af6ec98e343b0a","datavalue":{"value":{"entity-type":"item","numeric-id":5737076,"id":"Q5737076"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1430904$971E2BB3-6D67-4B5B-AD4E-A5AAAF1F8230","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3efb2a7a2946a44b5e87e549b3b81f72ca8b895b","datavalue":{"value":{"entity-type":"item","numeric-id":3916551,"id":"Q3916551"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1430904$F2522759-09AB-4E31-AFBB-D214C4413118","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3087f1a7eb9309c1646d3032c16c6ac9f3d28d8c","datavalue":{"value":{"entity-type":"item","numeric-id":1923820,"id":"Q1923820"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1430904$B13F221D-81C0-4879-9038-51960CADA97B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9154809d46de0469646d99042c9ccf1d8b62fa94","datavalue":{"value":{"entity-type":"item","numeric-id":1343396,"id":"Q1343396"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1430904$CD695160-BE78-4E68-934E-EE19F1107D43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2b89fc9b4fd15cbfc54fddb759b2d0fc7eb7f189","datavalue":{"value":{"entity-type":"item","numeric-id":1904397,"id":"Q1904397"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1430904$12AE0160-A09A-4087-90F9-A2842341B5DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f02927b40fa56a8999b1ccef110321a14129fb12","datavalue":{"value":{"entity-type":"item","numeric-id":1815858,"id":"Q1815858"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1430904$86CAABEF-7B5B-4BCF-BC30-DB1B4D35DE3A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2f1ecd6028bf82e657c458801db70e8788f9c69e","datavalue":{"value":{"entity-type":"item","numeric-id":1810853,"id":"Q1810853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1430904$CDE0EA6F-6F98-4B21-96CD-33BE936F04A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8cef60f49122cbdc8855980bc9949c7fcffb3541","datavalue":{"value":{"entity-type":"item","numeric-id":5444850,"id":"Q5444850"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1430904$6CCDFCF7-EDB4-430B-9730-3AB184CE64B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a4e1a291ac3cde8edb33ae306339a64d5e53ff45","datavalue":{"value":{"entity-type":"item","numeric-id":4792019,"id":"Q4792019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1430904$AC42BE4C-2115-4B5D-9737-F60F82BB8D61","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c33b50ee0a2c31a829a496bd5bb9e70958031d8d","datavalue":{"value":"10.1305/NDJFL/1074290715","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1430904$9D84D8E3-120D-42CA-BCBF-02BE74E68EBA","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f9b1519f8b03e1ccd4563eb938bc28236066b878","datavalue":{"value":{"entity-type":"item","numeric-id":1914373,"id":"Q1914373"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1b728e4df6afc1496fc02aa6c9e006c68d7d9c75","datavalue":{"value":{"amount":"+0.7479579448699951","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":"Q1430904$4F11504A-2514-44F6-9DCE-7B928F673FA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"27b4f735c9b2a4668f9812a90084bf78f5c96da9","datavalue":{"value":{"entity-type":"item","numeric-id":1383993,"id":"Q1383993"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b4802546356a1de0ca9b5ee445f1a7cb6a313a5c","datavalue":{"value":{"amount":"+0.7386808395385742","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":"Q1430904$4DE8ABD6-1F6E-4162-9EF9-F445E6616BBF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"28cab4edbc8f7d27ffd2d0e01f6038c188d600b1","datavalue":{"value":{"entity-type":"item","numeric-id":3328521,"id":"Q3328521"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0333d1063d2901b0010b2c816d9f79b89e35a9e1","datavalue":{"value":{"amount":"+0.7340898513793945","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":"Q1430904$E784A3B3-C741-4FE9-8855-2AE6F9EC96D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1b1ff08fbdda17bf7d34b5007ffedf5ffa163966","datavalue":{"value":{"entity-type":"item","numeric-id":3797157,"id":"Q3797157"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"afbc634cb4484566d8b5aa97225e4d70ff1d8a67","datavalue":{"value":{"amount":"+0.7331703901290894","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":"Q1430904$D141545E-0952-4B3F-97DC-4928F52FE6B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6faa5c285b677d687416885bc8a213e01066d271","datavalue":{"value":{"entity-type":"item","numeric-id":3698776,"id":"Q3698776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"78487d210345fd7e3db44d6c1bc9867698297549","datavalue":{"value":{"amount":"+0.7252987623214722","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":"Q1430904$8262E55F-3199-49EB-BFCC-FFB564932EC9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Shortest axiomatizations of implicational S4 and S5","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Shortest_axiomatizations_of_implicational_S4_and_S5"}}}}}