A Unique Normal Form for Tensor Trains over Arbitrary Fields

Renaud Vilmart

A Unique Normal Form for Tensor Trains over Arbitrary Fields

T0 review · 0 major / 9 minor · reviewed 2026-07-08 · glm-5.2

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Unique normal form found for tensor trains over any field

desk verdict First unique normal form for tensor trains over arbitrary fields, built on a novel LDPU decomposition. Proofs check out. read the letter →

arxiv 2607.06271 v1 pith:JEBR3E4W submitted 2026-07-07 cs.DS

Renaud Vilmart This is my paper · ORCID

classification cs.DS

keywords tensorfieldsformnormaltrainsarbitrarycomplexfull

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper proves that every tensor train — a chain of small tensors whose product represents a large multidimensional array — can be brought to a canonical minimal form that is unique, and this form can be reached in polynomial time. The key innovation is the LDPU decomposition: a variant of LU matrix factorization that, unlike the singular value decomposition used in prior approaches, works over arbitrary fields (including finite fields like the 2-element Galois field) and is provably unique. The author defines the normal form through two structural conditions on the cores of the tensor train (row-echelon form on one axis, column-echelon form with a permutation-conditioning constraint on the other), shows that a deterministic algorithm produces it, and then proves no other tensor train with the same modes can satisfy both conditions simultaneously. A two-sweep reduction algorithm, running in time proportional to the product of the maximum rank and the tensor train size, brings any tensor train into this form without ever increasing its size. The paper also provides a direct construction algorithm that builds the normal form from a full tensor, a method to extract the leading nonzero index and value, and a tight worst-case size bound showing the normal form uses at most 8/3 times the space of naive storage.

What carries the argument

The LDPU decomposition (Definition 5): a matrix factorization A = LDPU where L is unit column-echelon and P-conditioned, D is diagonal, P is a permutation, and U is unit row-echelon. Uniqueness is proved by an inductive argument showing pivot rows, column pivots, diagonal entries, and all remaining entries of L are forced. The tensor train normal form (Definition 14) requires two conditions on each core: the block matrix of slices is in full row-rank row-echelon form, and intertwine(C_i, P_i) is in full column-rank column-echelon form and P-conditioned. The two-sweep reduction (Theorem 19) enforces these conditions sequentially.

What would settle it

A matrix over some field for which two distinct LDPU decompositions exist — i.e., two different sets of (L, D, P, U) all satisfying the P-conditioning and echelon-form constraints — which would break the uniqueness claim of Proposition 7 and cascade to destroy Theorem 16.

Watch

Extended reading notes

Core claim

The central object is the LDPU decomposition, which factors any matrix A as L·D·P·U where L is in unit column-echelon form and is P-conditioned (a constraint tying the zero-pattern of L to the permutation P), D is diagonal, P is a permutation matrix, and U is in unit row-echelon form. The author proves this decomposition exists, is unique for any matrix over any field, and is rank-revealing — the three properties needed to serve as the replacement for SVD in the tensor train setting. Uniqueness of the tensor train normal form (Theorem 16) is then established by showing that each cut between consecutive cores corresponds exactly to an LDPU decomposition of a reshaped partial tensor, so the LD

Load-bearing premise

The uniqueness of the LDPU decomposition — and hence of the entire normal form — rests on the P-conditioning constraint on the lower triangular factor L being sufficient to force every entry of L to be uniquely determined. The proof argues inductively that pivot rows and column pivots are shared between any two decompositions and that P-conditioning pins down all remaining entries, but if some edge case involving specific field characteristics or degenerate rank profiles were

Editorial extensions

If this is right

Tensor trains over finite fields can now serve as a canonical data structure with the same uniqueness guarantee that BDDs enjoy, but with provably better compactness for some function families — enabling direct substitution in model checking, satisfiability, and circuit synthesis pipelines.
Equality testing between two tensor trains reduces to subtracting one from the other (polynomial time), applying the first sweep, and checking whether the first core is null — a consequence of Proposition 17 that avoids full tensor reconstruction.
The leading nonzero index and value of a tensor train can be extracted in O(dnr) after the first sweep (Proposition 18), which is faster than the O(dr^2) needed for an arbitrary index, exploiting the echelon structure of the cores.
The worst-case size bound of 8/3 times naive storage (Proposition 21) means tensor trains in normal form are never catastrophically larger than the full tensor, matching the constant-factor overhead known for BDDs.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Desk Editor's Note

read the letter

Short version: this paper gives the first unique normal form for tensor trains over arbitrary fields, and the proofs hold up. The core construction — the LDPU decomposition — is a genuine new contribution, and the uniqueness argument is clean once you sit with it. This deserves a serious referee and likely belongs in a good venue. The reader's assessment is on target; the stress-test concern about P-conditioning is real but resolves on careful reading. The paper's main achievement is defining a rank-revealing matrix decomposition (LDPU) that is both unique and field-agnostic, then using it to build a canonical tensor train form. The P-conditioning constraint (Definition 4) is the key insight: it adds just enough structure to force uniqueness without sacrificing existence. Proposition 7's proof by inductive peeling of pivot rows is correct — the REF zero-structure before leading indices does force sigma_1(k) = sigma_2(k) and then L entry-by-entry. Theorem 16 extends this to tensor trains by cutting at each core and applying LDPU uniqueness inductively, supported by Lemmas 9–13. The two-sweep reduction algorithm (Theorem 19) is polynomial, and the size bound (Proposition 21, factor 8/3) is tight with a matching lower bound. The string-diagram notation is a real help here — it makes the reshape arguments readable rather than index-heavy. The BDD connection over F_2 is well-motivated and not oversold. Soft spots are minor. The notation in Appendix C is occasionally confusing — sigma_i denotes the inverse of the permutation from Definition 4, and there is a likely typo where U_i[sigma_i(k)] should be U_1[sigma_1(k)]. These are presentation issues, not correctness issues. The paper honestly flags that the approach suffers from numerical instability and exponential bit complexity over infinite fields — the construction is really best suited for finite fields. This is fine and appropriately scoped. One thing I'd want a referee to check: whether the LDPU can be computed in matrix-multiplication time O(n^omega), which the author leaves open. This affects practicality but not correctness. This paper is for readers in formal methods, knowledge compilation, and tensor network theory who need exact equivalence checking or canonical representations over finite fields. It bridges BDDs and tensor networks in a concrete way.

Referee Report

0 major / 9 minor

Summary. The paper introduces the LDPU decomposition—a variant of LU decomposition that is rank-revealing and, crucially, unique over arbitrary fields—and uses it to define the first unique normal form for tensor trains. The main results are: (1) the LDPU decomposition exists, is unique, and is computable in O(nm min(n,m)) time (Proposition 7); (2) a normal form for tensor trains exists and is unique (Theorem 16); (3) a two-sweep reduction algorithm reaches this normal form in O(rs) time without increasing the tensor train size (Theorem 19), implying minimality of TT-ranks and size (Corollary 20); and (4) the size of a fully reduced tensor train is at most 8/3 times the full tensor size, which is tight (Proposition 21). The paper also provides algorithms for direct construction from a full tensor (Algorithm 1), nullity testing (Proposition 17), and leading-index extraction (Proposition 18). All proofs are given in full in the appendix.

Significance. The paper addresses a genuine gap: existing SVD-based tensor train reductions (HSVD) are not unique and are restricted to R and C. The LDPU decomposition and its uniqueness proof are the core technical contributions. The extension to tensor trains via a clean inductive argument at each core cut is well-executed. The connection to BDDs over F2 provides concrete motivation, and the size bound (Proposition 21) with a matching lower bound is a nice addition. The author is appropriately candid about practical limitations (numerical instability, exponential bit complexity for infinite fields), positioning the contribution as primarily relevant to finite fields. The string-diagrammatic framework, while adding length, does make the reshaping arguments more transparent.

minor comments (9)

Appendix C, proof of Proposition 7, induction step: the text states 'we get σ₁(1) = σ₂(1)' where it should read 'σ₁(k) = σ₂(k)'. The same typo repeats for D₁[1,1] = D₂[1,1] and U₁[σ₁(1)] = U₂[σ₂(1)], which should reference index k. This is a notational error in the induction step, not a gap in the argument.
Appendix C, proof of Proposition 7: the phrase 'By taking each U₁[σ₁(j)] in order by ascending leading coefficient' should read 'ascending leading index', since all leading coefficients are 1 in unit REF. The peeling argument proceeds by ascending leading index, not coefficient.
Appendix C, proof of Proposition 7: the notation σᵢ is introduced as 'the inverse of the permutation induced by Pᵢ', which is somewhat unusual. A brief clarifying remark that σᵢ maps column-pivot indices to their positions would help readers follow the inductive argument.
Algorithm 4 (LDPU): the return statement 'return L^⊺D⁻¹, D, P, P⁻¹A' could benefit from a brief comment explaining why the transpose appears (converting the row-operation tracking matrix to column-echelon form) and why D⁻¹ normalizes L to unit form. Without this, the connection between the algorithm's internal bookkeeping and the LDPU definition (Definition 5) is not immediately obvious.
Section 3.1, Example 6: the example is helpful, but the permutation σ is described only through its inverse values. Stating σ explicitly (σ(0)=1, σ(1)=2, σ(2)=0) would make the P-conditioning verification easier to follow.
Definition 14: the two conditions reference Pᵢ-conditioning, but the definition of P-conditioning (Definition 4) is stated for column-echelon form matrices. A brief remark confirming that intertwine(Cᵢ, nᵢ, Pᵢ₋₁)Pᵢ⁻¹ is indeed in the form required by Definition 4 would improve readability.
Theorem 19: the complexity is stated as O(rs) where r is the max TT-rank and s is the size. It would help to explicitly note that this assumes naive matrix multiplication, as mentioned later in the text, since the O(rs) bound depends on the LDPU cost being O(nm min(n,m)) with naive arithmetic.
Proposition 21, proof: the derivation uses the bound nᵢ ≥ 2 to replace geometric sums with 4/3. This assumption should be stated explicitly in the proposition or its proof, since modes of dimension 0 or 1 are allowed elsewhere in the paper.
The paper would benefit from a brief discussion of how the normal form interacts with core reordering (permuting the modes of the tensor train), given that the author notes in Section 2.1 that core ordering can dramatically change size. Even a sentence acknowledging that the normal form is defined for a fixed mode ordering would suffice.

Simulated Author's Rebuttal

0 responses · 0 unresolved

The referee report is uniformly positive, recommending minor revision, with no major comments listed. We thank the referee for the careful reading and note that we will address minor typographical issues in the next version.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity found — derivation is self-contained and parameter-free

full rationale

The paper's derivation chain is self-contained. The LDPU decomposition (Proposition 7) is defined from standard Gaussian elimination (Algorithm 4), and its uniqueness is proven in Appendix C via an inductive argument on pivot rows and column pivots — no self-citation is invoked for the load-bearing uniqueness claim. The normal form (Definition 14) is defined by structural conditions (row-echelon form, column-echelon form, P-conditioning) that do not presuppose the uniqueness result. Theorem 16 (uniqueness of the normal form) derives uniqueness by showing that the normal form conditions force an LDPU decomposition at each core cut, then invoking Proposition 7 — a genuine derivation, not a renaming. Theorem 19 (reduction algorithm) is shown to reach the normal form using Lemmas 9–13, all of which are proven from first principles about row-echelon form matrices. No parameters are fitted to data and re-presented as predictions. The only external citations (Selinger [30] for string diagrams, Carrell [10] for partial LDPU, Onaka et al. [23] for BDD-TT connection) are not by the present author and are not load-bearing for the uniqueness argument. The derivation is parameter-free and self-contained against external benchmarks (e.g., the worked example in Figure 3 and Appendix B).

Assumptions & free parameters 0 free parameters · 3 assumptions · 1 invented entities

The paper introduces no free parameters or ad-hoc axioms. The LDPU decomposition is a new mathematical object, but it is defined constructively and its properties are proven from standard linear algebra.

assumptions (3)

standard math Standard properties of row-echelon form matrices and Gaussian elimination over fields.
Used throughout Section 3.2 and the appendix proofs.
standard math The isomorphism of diagrams in the strict compact-close symmetric monoidal category Mat_F (Theorem 2, citing [30]).
Invoked in Section 2.2 to justify graphical manipulation of tensor networks.
domain assumption Tensor trains over F2 generalize binary decision diagrams (citing [23, 29]).
Stated in the introduction and Section 2.1 as motivation.

invented entities (1)

LDPU decomposition independent evidence
purpose: A unique, rank-revealing matrix decomposition replacing SVD for tensor train reduction.
Defined in Definition 5, proven unique in Proposition 7, with an explicit algorithm (Algorithm 4). It makes falsifiable claims about matrix factorization that can be checked independently.

how reviews work

0 comments

Cite this review

Pith. "Pith review of A Unique Normal Form for Tensor Trains over Arbitrary Fields." pith.science (2026). https://pith.science/paper/JEBR3E4W

@misc{pith2026260706271,
  author       = {Pith},
  title        = {Pith review of: A Unique Normal Form for Tensor Trains over Arbitrary Fields},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/JEBR3E4W}},
  note         = {Machine review of arXiv:2607.06271}
}

read the original abstract

Tensor trains (or Matrix-Product States) are a data structure used in many fields of computer science and physics. They were recently shown to generalise binary decision diagrams when used over the 2-element Galois field, prompting the question of their reducibility in such a context, when the standard approach, over real or complex number, is not amenable to finite fields. We provide here a unique normal form and associated polynomial-time reduction strategy for tensor trains over arbitrary fields. We also show how to directly extract a normal form out of a full tensor, how to get the leading index and value of a normal form, and an upper bound on the size of a fully-reduced tensor train relative to a naive storage of the full tensor. On the one hand, this work strengthens the use of tensor trains as a relevant formal tool. On the other hand, from the perspective of tensor networks, it extends the formalism to more general settings than the well-studied real and complex fields, and crucially provides the first tensor train form with the uniqueness property.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

19 extracted references · 19 canonical work pages

[1]

Efficient Decomposition of Dense Matrices over GF(2)

arXiv:1006.1744 [cs.MS]. URL:https://inria.hal.science/hal-00798458. 2 Marc Baboulin, Oguz Kaya, Theo Mary, and Matthieu Robeyns. Mixed precision iterative refinement for low-rank matrix and tensor approximations.SIAM Journal on Scientific Computing, 47(5):A2906–A2935, 2025.arXiv:https://doi.org/10.1137/23M1576992, doi: 10.1137/23M1576992. 3 Erwin H. Bare...

work page Pith review arXiv doi:10.1137/23m1576992 2025
[2]

4 David Bergman and Andre A

URL:http://dx.doi.org/10.2307/ 2004533,doi:10.2307/2004533. 4 David Bergman and Andre A. Cire. Multiobjective optimization by decision diagrams. In Michel Rueher, editor,Principles and Practice of Constraint Programming, pages 86–95, Cham,

work page doi:10.2307/2004533
[3]

5 Beate Bollig and Ingo Wegener

Springer International Publishing. 5 Beate Bollig and Ingo Wegener. Improving the variable ordering of obdds is np-complete. IEEE Trans. Comput., 45(9):993–1002, September 1996.doi:10.1109/12.537122. 6 Karl S. Brace, Richard L. Rudell, and Randal E. Bryant. Efficient implementation of a bdd package. InProceedings of the 27th ACM/IEEE Design Automation Con...

work page doi:10.1109/12.537122 1996
[4]

7 Michael Brickenstein and Alexander Dreyer

Association for Computing Machinery.doi: 10.1145/123186.123222. 7 Michael Brickenstein and Alexander Dreyer. Polybori: A framework for gröbner-basis compu- tations with boolean polynomials.Journal of Symbolic Computation, 44(9):1326 – 1345,

work page doi:10.1145/123186.123222
[5]

URL:http://dx.doi.org/10.1016/j.jsc.2008

Effective Methods in Algebraic Geometry. URL:http://dx.doi.org/10.1016/j.jsc.2008. 02.017,doi:DOI:10.1016/j.jsc.2008.02.017. 8 Jacob C Bridgeman and Christopher T Chubb. Hand-waving and interpretive dance: an introductory course on tensor networks.Journal of Physics A: Mathematical and Theoretical, 50(22):223001, May

work page doi:10.1016/j.jsc.2008 2008
[6]

1088/1751-8121/aa6dc3

URL: http://dx.doi.org/10.1088/1751-8121/aa6dc3, doi:10. 1088/1751-8121/aa6dc3. 9 Randal Bryant. Graph-based algorithms for boolean function manipulation.IEEE Transactions on Computers, C-35(8):677–691, 1986.doi:10.1109/TC.1986.1676819. 10 James B. Carrell.Groups, Matrices, and Vector Spaces: A Group Theoretic Approach to Linear Algebra. Springer New York,

work page doi:10.1088/1751-8121/aa6dc3 1986
[7]

11 Edmund M

URL:http://dx.doi.org/10.1007/978-0-387-79428-0, doi:10.1007/978-0-387-79428-0. 11 Edmund M. Clarke, Kenneth L. McMillan, Sérgio Vale Aguiar Campos, and Vasiliki Hartonas- Garmhausen. Symbolic model checking. InInternational Conference on Computer Aided Verification,

work page doi:10.1007/978-0-387-79428-0
[8]

13 Gene H Golub and Charles F Van Loan.Matrix Computations

[Online; accessed 21-01-2025]. 13 Gene H Golub and Charles F Van Loan.Matrix Computations. Johns Hopkins Studies in the Mathematical Sciences. Johns Hopkins University Press, Baltimore, MD, 4 edition, February

work page 2025

Show all 19 references

[9]

URL: http://dx.doi.org/10.1007/978-3-030-35554-8, doi:10.1007/ 978-3-030-35554-8. R. Vilmart 17 15 Sebastian Holtz, Thorsten Rohwedder, and Reinhold Schneider. On manifolds of tensors of fixed tt-rank.Numerische Mathematik, 120(4):701–731, September

doi
[10]

16 Xin Hong, Xiangzhen Zhou, Sanjiang Li, Yuan Feng, and Mingsheng Ying

URL: http: //dx.doi.org/10.1007/s00211-011-0419-7,doi:10.1007/s00211-011-0419-7. 16 Xin Hong, Xiangzhen Zhou, Sanjiang Li, Yuan Feng, and Mingsheng Ying. A tensor network based decision diagram for representation of quantum circuits.ACM Trans. Des. Autom. Electron. Syst., 27(6...

2022 doi
[11]

URL:https://arxiv.org/abs/1203.0202, arXiv:1203.0202. 18 C. Y. Lee. Representation of switching circuits by binary-decision programs.The Bell System Technical Journal, 38(4):985–999, 1959.doi:10.1002/j.1538-7305.1959.tb01585.x. 19 SaundersMacLane.Categories for the Working Mat...

1959 doi arXiv
[12]

URL: http://dx.doi.org/10.1007/978-1-4757-4721-8,doi:10.1007/978-1-4757-4721-8. 20 D. M. Miller and M. A. Thornton. QMDD: A Decision Diagram Structure for Reversible and Quantum Circuits. In36th International Symposium on Multiple-Valued Logic (ISMVL’06), pages 30–30, 2006.doi...

2006 doi
[13]

Association for Computing Machinery.doi:10.1145/157485. 164890. 23 RyomaOnaka, KengoNakamura, MasaakiNishino, andNorihitoYasuda. Tensordecomposition meets knowledge compilation: a study comparing tensor trains with obdds. InProceedings of the Thirty-Ninth AAAI Conference on Ar...

2025 doi
[14]

URL:http://dx.doi.org/10.1038/s42254-019-0086-7, doi: 10.1038/s42254-019-0086-7. 25 I. V. Oseledets. Tensor-train decomposition.SIAM Journal on Scientific Computing, 33(5):2295–2317, January

doi
[15]

1137/090752286

URL: http://dx.doi.org/10.1137/090752286, doi:10. 1137/090752286. 26 Roger Penrose et al. Applications of negative dimensional tensors.Combinatorial mathematics and its applications, 1(221-244):3,

doi
[16]

Wolf, and J

27 David Pérez-García, Frank Verstraete, Michael M. Wolf, and J. Ignacio Cirac. Matrix product state representations.Quantum Inf. Comput., 7(5):401–430, 2007.doi:10.26421/QIC7.5-6-1. 28 Krzysztof Podlaski. Reversible circuit synthesis using binary decision diagrams. In2016 MIX...

2007 doi
[17]

org/abs/2605.00106,arXiv:2605.00106

URL:https://arxiv. org/abs/2605.00106,arXiv:2605.00106. 30 P. Selinger.A Survey of Graphical Languages for Monoidal Categories, page 289–355. Springer Berlin Heidelberg,

arXiv
[18]

31 PetrTichavskýandOndřejStraka

URL: http://dx.doi.org/10.1007/978-3-642-12821-9_4, doi: 10.1007/978-3-642-12821-9_4. 31 PetrTichavskýandOndřejStraka. Optimizingtheorderofmodesintensortraindecomposition. IEEE Signal Processing Letters, 32:1361–1365, 2025.doi:10.1109/LSP.2025.3552005. 18 A Unique Normal Form ...

2025 doi
[19]

147902,doi:10.1103/physrevlett.91.147902

URL:http://dx.doi.org/10.1103/PhysRevLett.91. 147902,doi:10.1103/physrevlett.91.147902. 33 Liu Yang, Rezwana Karim, Vinod Ganapathy, and Randy Smith. Improving nfa-based signature matching using ordered binary decision diagrams. InProceedings of the 13th International Conferen...

doi

Pith tools

Reviewed July 8, 2026 · model on record in the stance chip above.

[1] [1]

Efficient Decomposition of Dense Matrices over GF(2)

arXiv:1006.1744 [cs.MS]. URL:https://inria.hal.science/hal-00798458. 2 Marc Baboulin, Oguz Kaya, Theo Mary, and Matthieu Robeyns. Mixed precision iterative refinement for low-rank matrix and tensor approximations.SIAM Journal on Scientific Computing, 47(5):A2906–A2935, 2025.arXiv:https://doi.org/10.1137/23M1576992, doi: 10.1137/23M1576992. 3 Erwin H. Bare...

work page Pith review arXiv doi:10.1137/23m1576992 2025

[2] [2]

4 David Bergman and Andre A

URL:http://dx.doi.org/10.2307/ 2004533,doi:10.2307/2004533. 4 David Bergman and Andre A. Cire. Multiobjective optimization by decision diagrams. In Michel Rueher, editor,Principles and Practice of Constraint Programming, pages 86–95, Cham,

work page doi:10.2307/2004533

[3] [3]

5 Beate Bollig and Ingo Wegener

Springer International Publishing. 5 Beate Bollig and Ingo Wegener. Improving the variable ordering of obdds is np-complete. IEEE Trans. Comput., 45(9):993–1002, September 1996.doi:10.1109/12.537122. 6 Karl S. Brace, Richard L. Rudell, and Randal E. Bryant. Efficient implementation of a bdd package. InProceedings of the 27th ACM/IEEE Design Automation Con...

work page doi:10.1109/12.537122 1996

[4] [4]

7 Michael Brickenstein and Alexander Dreyer

Association for Computing Machinery.doi: 10.1145/123186.123222. 7 Michael Brickenstein and Alexander Dreyer. Polybori: A framework for gröbner-basis compu- tations with boolean polynomials.Journal of Symbolic Computation, 44(9):1326 – 1345,

work page doi:10.1145/123186.123222

[5] [5]

URL:http://dx.doi.org/10.1016/j.jsc.2008

Effective Methods in Algebraic Geometry. URL:http://dx.doi.org/10.1016/j.jsc.2008. 02.017,doi:DOI:10.1016/j.jsc.2008.02.017. 8 Jacob C Bridgeman and Christopher T Chubb. Hand-waving and interpretive dance: an introductory course on tensor networks.Journal of Physics A: Mathematical and Theoretical, 50(22):223001, May

work page doi:10.1016/j.jsc.2008 2008

[6] [6]

1088/1751-8121/aa6dc3

URL: http://dx.doi.org/10.1088/1751-8121/aa6dc3, doi:10. 1088/1751-8121/aa6dc3. 9 Randal Bryant. Graph-based algorithms for boolean function manipulation.IEEE Transactions on Computers, C-35(8):677–691, 1986.doi:10.1109/TC.1986.1676819. 10 James B. Carrell.Groups, Matrices, and Vector Spaces: A Group Theoretic Approach to Linear Algebra. Springer New York,

work page doi:10.1088/1751-8121/aa6dc3 1986

[7] [7]

11 Edmund M

URL:http://dx.doi.org/10.1007/978-0-387-79428-0, doi:10.1007/978-0-387-79428-0. 11 Edmund M. Clarke, Kenneth L. McMillan, Sérgio Vale Aguiar Campos, and Vasiliki Hartonas- Garmhausen. Symbolic model checking. InInternational Conference on Computer Aided Verification,

work page doi:10.1007/978-0-387-79428-0

[8] [8]

13 Gene H Golub and Charles F Van Loan.Matrix Computations

[Online; accessed 21-01-2025]. 13 Gene H Golub and Charles F Van Loan.Matrix Computations. Johns Hopkins Studies in the Mathematical Sciences. Johns Hopkins University Press, Baltimore, MD, 4 edition, February

work page 2025