{"entities":{"Q1886325":{"pageid":1897067,"ns":120,"title":"Item:Q1886325","lastrevid":69191625,"modified":"2026-04-13T05:22:57Z","type":"item","id":"Q1886325","labels":{"en":{"language":"en","value":"The proof complexity of linear algebra"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 2116241"}},"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":"Q1886325$00DD15FC-D5DA-4227-8D6A-C0AA2198F2F7","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d645e6754c04c84f91d7b29d59951d1e5be52e8d","datavalue":{"value":{"text":"The proof complexity of linear algebra","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1886325$A1ED83EC-B458-4D75-90F8-89FF04B097F8","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"3ea9f362c48245b4593371e875e7bda8c06a66a8","datavalue":{"value":"1059.03064","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1886325$6B55177A-7D47-4A84-8474-5056DFE79988","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"06644c28854d4134a09144ca7d53b7f0310fd152","datavalue":{"value":{"entity-type":"item","numeric-id":453197,"id":"Q453197"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1886325$149064D4-166A-4C8F-AB47-1F8DA6BDD28D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"00ef32c5864b607ccf80c983c44b8c3fc4484c5b","datavalue":{"value":{"entity-type":"item","numeric-id":1096389,"id":"Q1096389"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1886325$39D8BCA5-D191-4388-BB64-88A840FC3E58","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f91a4bcbc93435aed71775d25a4c5cd09e26f12d","datavalue":{"value":{"entity-type":"item","numeric-id":122505,"id":"Q122505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1886325$10D58C0B-ECFE-4C4D-9BA8-23514929DA1D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"037fcf95f864ae0e38f5b6894c4f594ea5ca568c","datavalue":{"value":{"time":"+2004-11-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1886325$0CF32C42-96C2-4836-BC53-A748FC5D678E","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"8ffaf84dd9dab88b4f7342c19fc391aa91af8b02","datavalue":{"value":"The authors analyze the complexity of the concepts needed to prove the basic theorems of linear algebra. One of the important results obtained in this paper is that the Cayley-Hamilton theorem enjoys a feasible proof. The analysis is carried out by making use of three formal theories, each of which is carefully designed so as to examine the basic theorems under a certain complexity, respectively.  The basic ring properties of matrices, for example, are covered by the first theory whose theorems translate into tautology families with polynomial size Frege proofs. The theory proves also the equivalence between some principles called hard matrix identities such as \\(AB = I\\) iff \\(BA = I\\) for which it is usually required to compute inverses.  The second theory, which is an extension of the first with a new function to manipulate matrix powering, proves that the C-H theorem not only implies the hard matrix identities but also is equivalent to such principles as axiomatic definition of det and cofactor expansion, respectively.  Finally the third theory is based on the second by allowing induction on formulas with bounded universal matrix quantifiers, so that the major principles of linear algebra including the C-H theorem are all provable in it.  After these observations, the authors show how the theories are translated into propositional proof systems of certain complexities, respectively, with which the complexities of the proofs of the considered principles are determined explicitly.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1886325$A47A5C63-A479-4CD0-B863-B5D62F3FC54C","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"e3f06c5cc154fad665bbd7bfe01f3fd2207302a9","datavalue":{"value":{"entity-type":"item","numeric-id":588143,"id":"Q588143"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1886325$56E11E9F-81DD-431F-A4F5-AA978100485E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1886325$72A74A7B-52AB-42D0-BDD6-274CAC5D0B20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"822dbc4c091d9d354470bf66dcd7d659b1bcc45b","datavalue":{"value":"15A99","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1886325$931A13AC-9613-4C8C-9DEC-D5311729897E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b06ff2ef9e04b42ff2c5c43e297cd9d734a55887","datavalue":{"value":"15A24","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1886325$2C0AB8A2-C37C-4773-9AB7-45763706D414","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"bdba282b6a96e2993f95c1b9dcf02ceea2f48540","datavalue":{"value":"2116241","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1886325$7765EBFD-C0E2-4DA4-96B8-7513988148C7","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"986e975208b070c5142b42b7967bb38dc4fad0f4","datavalue":{"value":"proof complexity","type":"string"},"datatype":"string"},"type":"statement","id":"Q1886325$3B0095BB-C188-4576-81A6-BB4F098D14D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"17ef7db62ea690b4e5062dfc499cec745f9bc958","datavalue":{"value":"linear algebra","type":"string"},"datatype":"string"},"type":"statement","id":"Q1886325$16BC5713-045B-4757-A8F5-A29B2E617254","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e7fa19b311be0828916e3dcda04783788c7f95e9","datavalue":{"value":"feasible proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q1886325$C360EB2A-F7D8-4022-ABA8-F9402F678744","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ccfbdce029dcd93610c89a3c36c2dd0b5ae48527","datavalue":{"value":"polynomial time reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q1886325$0E4ABE88-6B74-479A-B24B-68ECE6741F93","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4e591d31355d240ae8ac568afeb493b00a9bb82e","datavalue":{"value":"polynomial size Frege proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q1886325$8703712F-C6FE-44B6-A719-03FA7EB2C49B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7dd9515a8e8710b152d274efc4769eebd2e87ff8","datavalue":{"value":"Cayley-Hamilton theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q1886325$9B2AE3AC-CDBE-4347-B4F3-9F832D734CAC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c48483ac543fac39d7d0fe5a588d4709a18ed869","datavalue":{"value":"Berkowitz's algorithm","type":"string"},"datatype":"string"},"type":"statement","id":"Q1886325$10F414DD-3BEB-4E3D-A52E-AA40E7FC1CD3","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":"Q1886325$CF8F1A98-04CC-44AB-8F78-6C9DCEB0CC7B","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"9263737044bddd9be0729c912c95e30af13745e1","datavalue":{"value":"https://doi.org/10.1016/j.apal.2003.10.018","type":"string"},"datatype":"url"},"type":"statement","id":"Q1886325$9809C74E-F407-456B-BDFC-60054BE459F6","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e5ce629cb0510559140afe5386ec659fb031780c","datavalue":{"value":"W1967948656","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1886325$450543A4-EC70-4F8B-A010-BEE4E5CED523","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"865a580c588e979f3485b9f8d3fefd6f0a924509","datavalue":{"value":{"entity-type":"item","numeric-id":1343166,"id":"Q1343166"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1886325$9187F1FA-293B-4081-8E2F-837D4E81C39E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"33c7a78759148ce6b1abced42ef4a952f4334dd8","datavalue":{"value":{"entity-type":"item","numeric-id":794429,"id":"Q794429"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1886325$24BC8596-61F8-488C-8DBA-80774629C4D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"85cb5c2591c3b4779c32d742e1061633a99acbed","datavalue":{"value":{"entity-type":"item","numeric-id":4850545,"id":"Q4850545"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1886325$A00085CB-86EF-46AA-AB4B-43BBC79A5080","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"770839834e9b2e75c5cac9d85b4f2bbde549b6c8","datavalue":{"value":{"entity-type":"item","numeric-id":4507332,"id":"Q4507332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1886325$17BFC017-2464-4C85-82AE-C0906A952182","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"035feb3d68e7fcb8cc1f5afc2267fb8cc293e0bf","datavalue":{"value":{"entity-type":"item","numeric-id":3794177,"id":"Q3794177"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1886325$FE1DF54C-B7AF-4443-B0F0-B975B49A3710","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f31cbeafb74eb2331031a6d2305fa02411af3e7","datavalue":{"value":{"entity-type":"item","numeric-id":3775553,"id":"Q3775553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1886325$9460974E-2B11-42A4-9209-24B9F619F735","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a2ea905e0dd45e5f666435e07c5347d2d8ec010b","datavalue":{"value":{"entity-type":"item","numeric-id":4215630,"id":"Q4215630"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1886325$95C6F63F-647E-4DF5-9299-13789D8A9380","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"34a549ed1d776396be3e4308655e166de224ba89","datavalue":{"value":{"entity-type":"item","numeric-id":4133141,"id":"Q4133141"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1886325$C1FD7AEA-7A34-40F3-8F6B-2C0C578CD1CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b90df03a170fcc85d9f6d5af38c0866a51f22b3f","datavalue":{"value":{"entity-type":"item","numeric-id":3694688,"id":"Q3694688"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1886325$B71816B3-E38D-4474-BEB5-DF8CF0E5F4D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6fa34ae3e34f6a863a9f8db67c2bfb8bb6401943","datavalue":{"value":{"entity-type":"item","numeric-id":4856172,"id":"Q4856172"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1886325$49A5BDF5-CEE0-4CE5-8F3D-DAE479F102A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"453be3d9493d689c7a7a1897e9678059dadf9cda","datavalue":{"value":{"entity-type":"item","numeric-id":4438100,"id":"Q4438100"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1886325$FFDAA182-6C39-4B6A-9FDA-F96AEB5D144B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"67092c36751024c2673b5e85ec899942d13fcb67","datavalue":{"value":{"entity-type":"item","numeric-id":701728,"id":"Q701728"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1886325$FF63C222-B496-42C3-A6A3-15C6190CFF97","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":"Q1886325$7012743B-CC82-4C0F-B001-FAEAB27A5E71","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"3a647d2a947e63a06cb45d709f224e9eabc436db","datavalue":{"value":"10.1016/J.APAL.2003.10.018","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1886325$5BC02C0A-FFF2-4544-850C-2E057A7C7A0B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e015d4792a0df6f68d5215099472987a4105131a","datavalue":{"value":{"entity-type":"item","numeric-id":5394597,"id":"Q5394597"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a989f13271ac7d48c7a4f75bc86e759e81d589c5","datavalue":{"value":{"amount":"+0.8417786359786987","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":"Q1886325$B3BF3230-23FF-43FB-A3EF-709877727E1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1758853338eca872e1267172b138fd81bb1f154c","datavalue":{"value":{"entity-type":"item","numeric-id":1766923,"id":"Q1766923"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0b57f2bb7015a70727a5e968726814307f56a787","datavalue":{"value":{"amount":"+0.8381342887878418","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":"Q1886325$5F861882-C5E3-469A-BB37-7C0B5FBC88C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8b7dc5e5e540adf127a4dd9000f77502f11e4203","datavalue":{"value":{"entity-type":"item","numeric-id":5901152,"id":"Q5901152"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5ff41e6f99085ac38e3a3977c5cb96a24bff920a","datavalue":{"value":{"amount":"+0.8331559896469116","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":"Q1886325$D4FC9756-5E4B-4436-AF99-D2E31F83FCE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"73a76c54a723d94007f00f0da302e5344556a97a","datavalue":{"value":{"entity-type":"item","numeric-id":5891510,"id":"Q5891510"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"659ca9b81647b3b4097b87266f23c3508e83b0e4","datavalue":{"value":{"amount":"+0.8302890062332153","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":"Q1886325$9CFB1AF2-3B54-4E98-85A0-4C9F27EFEA38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d86317ef658b5d9b4a9b6e6091aaf22c5fa5666c","datavalue":{"value":{"entity-type":"item","numeric-id":5056443,"id":"Q5056443"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8c1e6f453c0f2fb2309f2fb78c8e7c10c8035bea","datavalue":{"value":{"amount":"+0.8251161575317383","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":"Q1886325$12F3A1AB-72A3-46CB-89C9-5AD02DC47F67","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The proof complexity of linear algebra","badges":[]}}}}}