Formal Theories for Linear Algebra
We introduce two-sorted theories in the style of [CN10] for the complexity classes \oplusL and DET, whose complete problems include determinants over Z2 and Z, respectively. We then describe interpretations of Soltys' linear algebra theory LAp over arbitrary integral domains, into each of our n...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2012-03-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/716/pdf |
| _version_ | 1827322912938393600 |
|---|---|
| author | Stephen A Cook Lila A Fontes |
| author_facet | Stephen A Cook Lila A Fontes |
| author_sort | Stephen A Cook |
| collection | DOAJ |
| description | We introduce two-sorted theories in the style of [CN10] for the complexity
classes \oplusL and DET, whose complete problems include determinants over Z2
and Z, respectively. We then describe interpretations of Soltys' linear algebra
theory LAp over arbitrary integral domains, into each of our new theories. The
result shows equivalences of standard theorems of linear algebra over Z2 and Z
can be proved in the corresponding theory, but leaves open the interesting
question of whether the theorems themselves can be proved. |
| first_indexed | 2024-04-25T01:36:22Z |
| format | Article |
| id | doaj.art-2cd5b3d221e645c68c550f1696f4a38a |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:36:22Z |
| publishDate | 2012-03-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-2cd5b3d221e645c68c550f1696f4a38a2024-03-08T09:27:54ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742012-03-01Volume 8, Issue 110.2168/LMCS-8(1:25)2012716Formal Theories for Linear AlgebraStephen A CookLila A FontesWe introduce two-sorted theories in the style of [CN10] for the complexity classes \oplusL and DET, whose complete problems include determinants over Z2 and Z, respectively. We then describe interpretations of Soltys' linear algebra theory LAp over arbitrary integral domains, into each of our new theories. The result shows equivalences of standard theorems of linear algebra over Z2 and Z can be proved in the corresponding theory, but leaves open the interesting question of whether the theorems themselves can be proved.https://lmcs.episciences.org/716/pdfcomputer science - logic in computer sciencef.4.0 |
| spellingShingle | Stephen A Cook Lila A Fontes Formal Theories for Linear Algebra Logical Methods in Computer Science computer science - logic in computer science f.4.0 |
| title | Formal Theories for Linear Algebra |
| title_full | Formal Theories for Linear Algebra |
| title_fullStr | Formal Theories for Linear Algebra |
| title_full_unstemmed | Formal Theories for Linear Algebra |
| title_short | Formal Theories for Linear Algebra |
| title_sort | formal theories for linear algebra |
| topic | computer science - logic in computer science f.4.0 |
| url | https://lmcs.episciences.org/716/pdf |
| work_keys_str_mv | AT stephenacook formaltheoriesforlinearalgebra AT lilaafontes formaltheoriesforlinearalgebra |