### Books

- Michael Soltys.

*An introduction to the analysis of algorithms*

First Edition: 152 pages,`ISBN: 978-981-4271-40-0`, October 2009

Second Edition: 215 pages,`ISBN: 978-981-4401-15-9`, May 2012

World Scientific: [1st ed][2nd ed]

Amazon: [1st ed][2nd ed]

**3rd edition to come out in 2017!**

- Michael Soltys.

*An introduction to computational complexity*

[Click here for a sample]

Published by the Jagiellonian University Press.

143 pages,`ISBN: 978-83-233-2864-3`, 2009.

### Journal papers

- Waldemar W. Koczkodaj, Dominik Strzalka, Jean-Pierr Magnot, Jiri Mazurek, James Peters, Michael Soltys, Jacek Szybowski, Arturo Tozzi, Hojjat Rakhshani

*On normalization of inconsistency indicators in pairwise comparisons*Abstract: In this study, we provide mathematical and practice-driven justification for using [0, 1] normalization of inconsistency indicators in pairwise comparisons. The need for normalization, as well as problems with the lack of normalization, are presented. A new type of paradox of infinity is described.

Accepted for publication in the International Journal of Approximate Reasoning (*available online, to appear soon*), April 2017.

[doi][blog][arXiv]

- Joel Helling, P.J. Ryan, W.F. Smyth, Michael Soltys

*Constructing an Indeterminate String from its Associated Graph*Abstract: As discussed at length in [Christodoulakis et al.,

*Indeterminate strings, prefix arrays and undirected graphs*, Theoret. Comput. Sci. 600 4 (2015)], there is a natural one-many correspondence between simple undirected graphs G with vertex set V = {1,2,…,n} and indeterminate strings x=x[1..n] – that is, sequences of subsets of some alphabet Sigma. In this paper, given G, we consider the “reverse engineering” problem of computing a corresponding x on an alphabet Sigma_min of minimum cardinality. This turns out to be equivalent to the NP-hard problem of computing the intersection number of G, thus in turn equivalent to the clique cover problem. We describe a heuristic algorithm that computes an approximation to Sigma_min and a corresponding x. We give various properties of our algorithm, including some experimental evidence that on average it requires O(n^2log n) time. We compare it with other heuristics, and state some conjectures and open problems.

Theoretical Computer Science (*available online, to appear in print soon*), 2017.

Also presented at LSD&LAW 2017.

[doi][github][blog]

- Waldemar W. Koczkodaj, Ludmil Mikhailov, Grzegorz Redlarski, Jacek Szybowski, Gaik Tamazian, Michael Soltys, Elisa Wajch and Kevin Kam Fung Yuen

*Important Facts and Observations about Pairwise Comparisons*

Abstract: This study has been inspired by numerous requests from researchers who often confuse Saaty’s AHP with the Pairwise Comparisons (PC) method, taking AHP as the only representation of PC. Most formal results of this survey article are based on a recently published work by Koczkodaj and Szwarc. This article should be regarded as an interpretation and clarification of future theoretical investigations of PC. In addition, this article is a reflection on general PC research at a higher level of abstraction: the philosophy of science. It delves into the foundations and implications of pairwise comparisons. Finally, open problems have also been reported for future research.

Special Issue on Pairwise Comparisons in Fundamenta Informaticae, 144(3-4): 291-307, 2016

[doi]

- Barbara Sandrasagra and Michael Soltys

*Complex Ranking Procedures*Abstract: We propose a research program for developing a formal framework for ranking procedures based on the Pairwise Comparisons method. We are interested in the case where relatively few items are to be ranked with a complex procedure and according to a large number of criteria. A typical example of this scenario is a competition where several companies bid for a contract, and where the selection of the winner is done with multiple criteria according to an intricate selection procedure. Several other applications are suggested.

Special Issue on Pairwise Comparisons in Fundamenta Informaticae, 144(3-4): 223-240, 2016

[doi][blog]

- Michael Soltys

*A Formal Approach to Ranking Procedures*Abstract: A formal framework for ranking procedures is proposed. The case of interest is where relatively few items are to be ranked with a complex procedure and according to a large number of criteria. A typical example of this scenario is a competition where several companies bid for a contract, and where the selection of the winner is done with multiple criteria according to an intricate selection procedure. A case study of a bidding procedure is presented, and a logical theory for matrix algebra is proposed as the formal framework for working with Pairwise Comparisons.

International Journal of Knowledge-based and Intelligent Engineering Systems, 19(4): 225-234, 2015

[doi]

- Neerja Mhaskar and Michael Soltys

*String Shuffle: Circuits and Graphs*Abstract: We show that shuffle, the problem of determining whether a string w can be composed from an order preserving shuffle of strings x and y, is not in AC^0, but it is in AC^1. The fact that shuffle is not in AC0 is shown by a reduction of parity to shuffle and invoking the seminal result of Furst et al., while the fact that it is in AC1 is implicit in the results of Mansfield. Together, the two results provide a lower and upper bound on the complexity of this combinatorial problem. We also explore an interesting relationship between graphs and the shuffle problem, namely what types of graphs can be represented with strings exhibiting the anti-Monge condition.

Journal of Discrete Algorithms, 31:120-128, March 2015.

[doi][github][blog]

- Sam Buss and Michael Soltys

*Unshuffling a Square is NP-Hard*Abstract: A shuffle of two strings is formed by interleaving the characters into a new string, keeping the characters of each string in order. A string is a square if it is a shuffle of two identical strings. There is a known polynomial time dynamic programming algorithm to determine if a given string z is the shuffle of two given strings x,y; however, it has been an open question whether there is a polynomial time algorithm to determine if a given string z is a square. We resolve this by proving that this problem is NP-complete via a many-one reduction from 3-Partition.

Journal of Computer and System Sciences, 80(4):766-776, 2013.

[doi][arXiv][slides][github 1][github 2]

- Michael Soltys

*Proving properties of matrices over Z2*Abstract: We prove assorted properties of matrices over Z_2, and outline the complexity of the concepts required to prove these properties. The goal of this line of research is to establish the proof complexity of matrix algebra. It also presents a different approach to linear algebra: one that is formal, consisting in algebraic manipulations according to the axioms of a ring, rather than the traditional semantic approach via linear transformations. Archive for Mathematical Logic, 51(5):535-551, 2012.

[doi]

- Grzegorz Herman and Michael Soltys

*Unambiguous functions in logarithmic space*Abstract: We investigate different variants of unambiguity in the context of computing multi-valued functions. We propose a modification to the standard computation models of Turing machines and configuration graphs, which allows for unambiguity-preserving composition. We define a notion of reductions (based on function composition), which allows nondeterminism but controls its level of ambiguity. In light of this framework we establish reductions between different variants of path counting problems. We obtain improvements of results related to inductive counting. Fundamenta Informaticae, 114(2):129-147, 2012.

[doi]

- Michael Soltys

*Feasible proofs of Szpilrajn’s theorem: A proof-complexity framework for concurrent automata*Abstract: The aim of this paper is to propose a proof-complexity framework for concurrent automata. Since the behavior of concurrent processes can be described with partial orders, we start by formalizing proofs of Szpilrajn’s theorem. This theorem says that any partial order may be extended to a total order. We give two feasible proofs of the finite case of Szpilrajn’s theorem. The first proof is formalized in the logical theory LA extended to ordered rings; this yields a TC^0 Frege derivation. The second proof is formalized in the logical theory ∃LA and yields a P/poly Frege derivation. Although TC^0 is a much smaller complexity class than P/poly, the trade-off is that the P/poly proof is algebraically simpler—it requires the algebraic theory LA over the simplest of rings: Z_2.

Journal of Automata, Languages and Combinatorics, 16(1):27-38, 2011.

[journal]

- Michael Soltys and Craig Wilson

*On the complexity of computing winning strategies for finite poset games*

Abstract: This paper is concerned with the complexity of computing winning strategies for poset games. While it is reasonably clear that such strategies can be computed in PSPACE, we give a simple proof of this fact by a reduction to the game of geography. We also show how to formalize the reasoning about poset games in Skelley’s theory WW_1^1 for PSPACE reasoning. We conclude that W_1^1 can use the “strategy stealing argument” to prove that in poset games with a supremum the first player always has a winning strategy.

Theory of Computing Systems, 48(3):680-692, 2011.

[doi]

- Grzegorz Herman and Michael Soltys

*On the Ehrenfeucht-Mycielski sequence*

Abstract: We introduce the inverted prefix tries (a variation of suffix tries) as a convenient formalism for stating and proving properties of the Ehrenfeucht- Mycielski sequence. We also prove an upper bound on the position in the sequence by which all strings of a given length will have appeared; our bound is given by the Ackermann function, which, in light of experi- mental data, may be a gross over-estimate. Still, it is the best explicitly known upper bound at the moment. Finally, we show how to compute the next bit in the sequence in a constant number of operations.

Journal of Discrete Algorithms, 7(4):500-508, 2009.

[doi][github]

(*In 2008, we used*`generate.c`*available on GitHub, in order to obtain the first 30 million bits of the EM sequence in just under two minutes with 2Gb of RAM*).

- Grzegorz Herman, Tim Paterson and Michael Soltys

*A propositional proof system with quantification over permutations of variables*,

Abstract: We introduce a new propositional proof system, which we call H, that allows quantifi- cation over permutations. In H we may write (∃ab)α and (∀ab)α, which is semantically equivalent to α(a, b) ∨ α(b, a) and α(a, b) ∧ α(b, a), respectively. We show that H with cuts restricted to Σ_1 formulas (we denote this system H_1) simulates efficiently the Hajós calculus (HC) for constructing graphs which are non-3-colorable. This shows that short proofs over formulas that assert the exis- tence of permutations can capture polynomial time reasoning (as by [9], HC is equivalent in strength to EF, which in turn captures polytime reasoning). We also show that EF simulates efficiently H^*_1, which is H_1 with proofs restricted to being tree-like. In short, we show that H^∗1_1 ≤p EF ≤p H_1.

Fundamenta Informaticae, 79(1-2):71-83, 2007.

[doi]

- Michael Soltys

*The proof theoretic strength of the Steinitz Exchange Theorem*Abstract: We show that the logical theory QLA proves the Cayley-Hamilton theorem from the Steinitz Exchange theorem together with a strength- ening of the linear independence principle. Since QLA is a fairly weak theory (in the sense that its quantifier-free fragment, LA, translates into tautologies with TC^0-Frege proofs—when restricted to the field Q of the rationals), it follows that the proof complexity of matrix algebra can be distilled to the Steinitz Exchange theorem.

Discrete Applied Mathematics, 155(1):53-60, 2007.

[doi]

- Michael Soltys

*LA, Permutations, and the Hajos Calculus*

Abstract: LA is a simple and natural logical system for reasoning about matrices. We show that LA, over finite fields, proves a host of matrix identities (so called “hard matrix identities”) from the matrix form of the pigeon- hole principle. LAP is LA with matrix powering; we show that LAP extended with quantification over permutations is strong enough to prove fundamental theorems of linear algebra (such as the Cayley-Hamilton The- orem). Furthermore, we show that LA with quantification over permuta- tions expresses NP graph-theoretic properties, and proves the soundness of the Hajós Calculus. Several open problems are stated.

Theoretical Computer Science, 348(2-3):321-333, December 2005.

[doi]

- Neil Thapen and Michael Soltys

*Weak Theories of Linear Algebra*Abstract: We investigate the theories LA,LAP,∀LAP of linear algebra, which were originally defined to study the question of whether com- mutativity of matrix inverses has polysize Frege proofs. We give sen- tences separating quantified versions of these theories, and define a fragment ∃LA of ∀LAP in which we can interpret a weak theory V_1 of bounded arithmetic and carry out polynomial time reasoning about matrices – for example, we can formalize the Gaussian elimination algorithm. We show that, even if we restrict our language, ∃LA proves the commutativity of inverses.

Archive for Mathematical Logic, 44(2):195-208, 2005.

[doi]

- Michael Soltys and Stephen Cook

*The Proof Complexity of Linear Algebra*

Abstract: We introduce three formal theories of increasing strength for lin- ear algebra in order to study the complexity of the concepts needed to prove the basic theorems of the subject. We give what is apparently the first feasible proofs of the Cayley-Hamilton theorem and other properties of the determinant, and study the propositional proof complexity of matrix identities such as AB = I → BA = I.

Annals of Pure and Applied Logic, 130(1-3):207-275, December 2004.

[doi]

- Michael Soltys and Alasdair Urquhart

*Matrix Identities and the Pigeonhole Principle*

Abstract: We show that short bounded-depth Frege proofs of matrix identities, such as P Q = I ⊃ QP = I (over the field of two elements), imply short bounded-depth Frege proofs of the pigeonhole principle. Since the latter principle is known to require exponential-size bounded-depth Frege proofs, it follows that the propositional version of the matrix principle also requires bounded-depth Frege proofs of exponential size.

Archive for Mathematical Logic, 43(3):351-358, April 2004.

[doi]

- Michael Soltys

*Extended Frege and Gaussian Elimination*

Abstract: We show that the Gaussian Elimination algorithm can be proven cor- rect with uniform Extended Frege proofs of polynomial size, and hence feasibly. More precisely, we give short uniform Extended Frege proofs of the tautologies that express the following: given a matrix A, the Gaussian Elimination algorithm reduces A to row-echelon form. We also show that the consequence of this is that a large class of matrix identities can be proven with short uniform Extended Frege proofs, and hence feasibly.

Bulletin of the Section of Logic, 31(4):1-17, 2002.

- Michael Soltys

*Berkowitz’s Algorithm and Clow Sequences*,

Abstract: A combinatorial interpretation of Berkowitz’s algorithm is presented. Berkowitz’s algorithm is the fastest known parallel algorithm for computing the characteristic polynomial of a matrix. The combinatorial interpretation is based on “loop covers” introduced by Valiant, and “clow sequences”, defined by Mahajan and Vinay. Clow sequences turn out to capture very succinctly the computations performed by Berkowitz’s algorithm, which otherwise are quite difficult to analyze. The main contribution of this paper is a proof of correctness of Berkowitz’s algorithm in terms of clow sequences.

Electronic Journal of Linear Algebra, 9:42-54, 2002.

[ELA repository]

- Stephen Cook and Michael Soltys

*Boolean Programs and Quantified Propositional Proof Systems*

Abstract: We introduce the notion of Boolean programs, which provide more concise descriptions of Boolean functions than Boolean circuits. We characterize nonuniform PSPACE in terms of polynomial size families of Boolean programs. We then show how to use Boolean programs to witness quantifiers in the subsystems G1 and G∗1 of the proof system G for the quantified propositional calculus.

Bulletin of the Section of Logic, 28(3):119-129, 1999.

### Proceedings

- Ariel Fernández, Ryszard Janicki and Michael Soltys

*A permutation-based algorithm for computing covers from matchings*

Abstract: We present a matrix permutation algorithm for computing a minimal vertex cover from a maximal matching in a bipartite graph. Our algorithm is linear time and linear space, and provides an interesting perspective on a well known problem. Unlike most algorithms, it does not use the concept of alternating paths, and it is formulated entirely in terms of combinatorial operations on a binary matrix.

To appear at the 32nd International Conference on Computers and Their Applications (CATA2017), March 2017.

- Waldemar Koczkodaj and Michael Soltys

*Consistency-driven Pairwise Comparisons Approach to Abandoned Mines Hazard Rating*Abstract: The pairwise comparisons method, together with inconsistency analysis, are used to assess the hazard level for abandoned mines. Weights, reflecting the relative importance of the objectives concerned are one of the most commonly used solutions for this type of data. Subjective assessments involve inaccuracy (which is difficult to manage) and inconsistency in assessments (which can be measured and may influence the accuracy). The pairwise comparisons method allows us to define a consistency measure and use it as a validation technique. A consistency-driven knowledge acquisition, supported by a properly designed software, contributes to the improvement of quality of knowledge-based systems.

The 7th International Conference on Computational Methods (ICCM2016), August 2016.

- Neerja Mhaskar and Michael Soltys

*Forced repetitions over alphabet lists*Abstract. Thue [Thu06] showed that there exist arbitrarily long square-free strings over an alphabet of three symbols (not true for two symbols). An open problem was posed in [GKM10], which is a generalization of Thue’s original result: given an alphabet list L = L1, . . . , Ln, where |Li| = 3, is it always possible to find a square-free string, w = w1w2 . . . wn, where wi ∈ Li? In this paper we show that repetitions can be forced on square-free strings over alphabet lists iff a suffix of the square-free string conforms to a pattern which we term as an offending suffix. We also prove properties of offending suffixes. However, the problem remains tantalizingly open.

To appear in 21st Prague Stringology Conference (PSC), August 2016.

[slides]

- Neerja Mhaskar and Michael Soltys

*A formal framework for Stringology*

Abstract: A new formal framework for Stringology is proposed, which consists of a three-sorted logical theory S designed to capture the combinatorial reasoning about finite words. A witnessing theorem is proven which demonstrates how to extract algo- rithms for constructing strings from their proofs of existence. Various other applications of the theory are shown. The long term goal of this line of research is to introduce the tools of Proof Complexity to the analysis of strings.

20th Prague Stringology Conference (PSC), to appear in Lecture Notes in Computer Science, 2015.

[slides]

- Neerja Mhaskar and Michael Soltys

*Non-repetitive strings over alphabet lists*

Abstract: A word is non-repetitive if it does not contain a subword of the form vv. Given a list of alphabets L=L_1,L_2,…,L_n, we investigate the question of generating non-repetitive words w=w_1w_2 … w_n, such that the symbol w_i is a letter in the alphabet L_i. This problem has been studied by several authors (e.g., Grytczuk, Shallit, and it is a natural extension of the original problem posed and solved by A. Thue. While we do not solve the problem in its full generality, we show that such strings exist over many classes of lists. We also suggest techniques for tackling the problem, ranging from online algorithms, to combinatorics over 0-1 matrices, and to proof complexity. Finally, we show some properties of the extension of the problem to abelian squares.

WALCOM: Algorithms and Computation, volume 8973 of Lecture Notes in Computer Science, pages 270-281, February 2015.

[doi][github-1][github-2][blog]

- Michael Soltys

*Fair ranking in competitive bidding procurement: A case analysis*

Best Paper Award.

Abstract: Fair and transparent procurement procedures are a cornerstone of a well functioning free-market economy. In particular, bidding is a mechanism whereby companies compete for contracts; when functioning well, the process rewards both the quality of the proposal, and the “reasonableness” of the quote. This way, both the company and the public win. The bidding process requires a fair and transparent ranking procedure. Once the parameters of the competition are established, the company issuing the bid is required by law to abide by those parameters. Not surprisingly, opposing interests may try to “game the system.” The more complex the service, the harder it is to rank competing bids. Complex services require complex ranking, which in turn makes undue influence more difficult to uncover. In this paper we analyze the case of two companies, Reilly Security and Contemporary Security, bidding for the contract of providing security during the Pan American games in Toronto 2015: The Pan Am Games are the world’s third largest international multi-sport Games; they are only surpassed in size and scope by the Olympic Summer Games and the Asian Games. We argue that the ranking procedures did not reflect the quality of the bids, resulting in one of the companies submitting a substantially more expensive bid, and still winning the competition. The reader may gain information on this contentious matter by reading a number of newspaper articles. The author consulted for Executek International on this matter.

18th International Conference in Knowledge Based and Intelligent Information and Engineering Systems (KES), volume 35, Procedia Computer Science, pages 1138-1144, Pomorski Park Naukowo-Techniczny (PPNT), Gdynia, September 2014.

[doi][slides][blog]

- Ariel Fernández and Michael Soltys

*Feasible combinatorial matrix theory*Abstract: We give the first, as far as we know, feasible proof of König’s Min-Max Theorem (KMM), a fundamental result in combinatorial matrix theory, and we show the equivalence of KMM to various Min-Max principles, with proofs of low complexity.

38th International Symposium on Mathematical Foundations of Computer Science (MFCS), volume 8087 of Lecture Notes in Computer Science, pages 777-788, IST, Klosterneuburg, Austria, August 2013.

Click here for an expanded proof of Claim 8 in the paper.

[doi][slides]

- Michael Soltys

*Circuit complexity of shuffle*

Abstract: We show that sh(x,y,w), the problem of determining whether a string w can be composed from an order preserving shuffle of strings x and y, is not in AC^0, but it is in AC^1. The fact that shuffle is not in AC^0 is shown by a reduction of parity to shuffle and invoking the seminal result from 1984 regrind parity not in AC^0, while the fact that it is in AC^1 is implicit in the 1982 results of Mansfield. Together, the two results provide a strong complexity bound for this combinatorial problem.

International Workshop on Combinatorial Algorithms (IWOCA), volume 8288 of the Lecture Notes in Computer Science, pages 402-411, Rouen, France, July 2013.

[doi][slides]

- Katharine Blanchard and Michael Soltys

*Perceptions of foundational knowledge by computer science students*

Abstract: In this paper we are concerned with computer science students’

perceptions of foundational knowledge, understood as the mathematical

underpinnings of the field. We review recent literature on the

subject, propose an approach for teaching foundational knowledge, and

finally present a case study where we analyze the merits of our

approach. We make our observations based on experience and on a

student survey.

17th Western Canadian Conference on Computing Education (WCCCE), University of British Columbia, Vancouver, May 2012.

[doi][slides]

- Michael Soltys

*The proof theoretic strength of the Steinitz exchange theorem*Abstract: We show that the proof complexity of matrix algebra can be distilled to the Steinitz Exchange Theorem (SET): given a total set of vectors T, and a linearly independent set E, we can compute a set F such that |E|=|F| and (T-F) ∩ E is also total. We observe that the set F can be computed with NC^2 algorithms (polynomial size, depth O(log^2n) circuits), and outline a proof of the Cayley-Hamilton Theorem (a central result of matrix algebra) from SET within the logical theory QLA.

10th Meeting on Computer Algebra and Applications (EACA), pages 174-177, Seville, September 2006.

[slides]

- David L. Parnas and Michael Soltys

*Basic Science for Software Developers*

14th International Symposium on Formal Methods, pages 15-20, Canada, August 2006.

- Michael Soltys

*Feasible Proofs of Matrix Properties with Csanky’s Algorithm*Abstract: We show that Csanky’s fast parallel algorithm for computing the characteristic polynomial of a matrix can be formalized in the logical theory LAP, and can be proved correct in LAP from the principle of linear independence. LAP is a natural theory for reasoning about linear algebra introduced in Soltys & Cook. Further, we show that several principles of matrix algebra, such as linear independence or the Cayley-Hamilton Theorem, can be shown equivalent in the logical theory QLA. Applying the separation between complexity classes AC\subsetneq DET, we show that these principles are in fact not provable in QLA. In a nutshell, we show that linear independence is “all there is” to elementary linear algebra (from a proof complexity point of view), and furthermore, linear independence cannot be proved trivially (again, from a proof complexity point of view).

19th International Workshop Computer Science Logic (CSL), volume 3634 of Lecture Notes in Computer Science, pages 493-508, Oxford, August 2005.

[doi][slides][arXiv]

- Michael Soltys

*LA, Permutations, and the Hajos Calculus*Abstract: LA is a simple and natural field independent system for reasoning about matrices. We show that LA extended to contain a matrix form of the pigeonhole principle is strong enough to prove a host of matrix identities (so called “hard matrix identities” which are candidates for separating Frege and extended Frege). LAP is LA with matrix powering; we show that LAP extended with quantification over permutations is strong enough to prove theorems such as the Cayley-Hamilton Theorem. Furthermore, we show that LA extended with quantification over permutations expresses NP graph-theoretic properties, and proves the soundness of the Hajós calculus. A corollary is that a fragment of Quantified Permutation Frege (a novel propositional proof system that we introduce in this paper) is p-equivalent of extended Frege. Several open problems are stated.

31st International Colloquium on Automata, Languages and Programming (ICALP), volume 3142 of Lecture Notes in Computer Science, pages 1176-1187, Turku, July 2004.

[doi][slides]

- Michael Soltys

*Matrix algebra with quantification over permutations*Abstract: We introduce a logical system (called ∃PLAP) for reasoning about matrix algebra. ∃PLAP formalizes existential quantification over permutations, and it is strong enough to derive important results of matrix algebra such as the Cayley Hamilton Theorem. On the other hand, ∃PLAP is feasible, in the sense that it falls within polynomial time reasoning. This result elucidates further the proof complexity of linear algebra based on Berkowitz’s fast parallel algorithm for computing the characteristic polynomial.

9th Meeting on Computer Algebra and Applications (EACA), pages 301-305, Santander, July 2004.

- Michael Soltys

*Finite Fields and Propositional Proof Systems*Abstract: Propositional proof complexity is a well established area of theoretical computer science; it is an area of research intimately connected with complexity theory and automated reasoning. In this paper we introduce a proof system, which we call A (a fragment of the theory LA), for formalizing algebraic proofs over arbitrary fields, and we show how to translate formulas and proofs over A into propositional proofs, and conclude that we can formalize properties of finite fields (where the depth is small) with short Frege proofs.

The 7th World Multiconference on Systemics, Cybernetics and Informatics, pages 141-146, Orlando, Florida, July 2003.

- Michael Soltys and Stephen Cook

*The Proof Complexity of Linear Algebra*,

Abstract: We introduce three formal theories of increasing strength for linear algebra in order to study the complexity of the concepts needed to prove the basic theorems of the subject. We give what is apparently the first feasible proofs of the Cayley Hamilton theorem and other properties of the determinant, and study the propositional proof complexity of matrix identities.

17th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 335-344, Copenhagen, July 2002.

[slides]

### Presentations

- Ariel Fernández and Michael Soltys

*Feasible combinatorial matrix theory: polytime proofs for König’s Min-Max and related theorems*Abstract: We show that the well-known König’s Min-Max Theorem (KMM), a fundamental result in combinatorial matrix theory, can be proven in the first order theory LA with induction restricted to ∑_1^B formulas. This is an improvement over the standard textbook proof of KMM which requires ∏_2^B induction, and hence does not yield feasible proofs – while our new approach does. LA is a weak theory that essentially captures the ring properties of matrices; however, equipped with ∑_1^B$ induction LA is capable of proving KMM, and a host of other combinatorial properties such as Menger’s, Hall’s and Dilworth’s Theorems. Therefore, our result formalizes Min-Max type of reasoning within a feasible frame work.

Short presentation at LICS 2013.

[slides][full version]

- Michael Soltys and Greg Herman

*Unambiguous functions in logarithmic space*Abstract: We investigate different variants of unambiguity in the context of computing multi-valued functions. We propose a modification to the standard computation models of Turing Machines and configuration graphs, which allows for unambiguity-preserving composition. We define a notion of reductions (based on function composition), which allows nondeterminism but controls its level of ambiguity. In light of this framework we establish reductions between different variants of path counting problems. We obtain improvements of results related to inductive counting.

5th Conference on Computability in Europe (CiE), pages 162-175, Heidelberg, August 2009.

[slides]

- Michael Soltys and Craig Wilson

*On the complexity of computing winning strategies for finite poset games*Abstract: This paper is concerned with the complexity of computing winning strategies for poset games. While it is reasonably clear that such strategies can be computed in PSPACE, we give a simple proof of this fact by a reduction to the game of geography. We also show how to formalize the reasoning about poset games in Skelley’s theory W_1^1 for PSPACE reasoning. We conclude that W_1^1 can use the “strategy stealing argument” to prove that in poset games with a supremum the first player always has a winning strategy.

4th Conference on Computability in Europe (CiE), pages 415-424, Athens, June 2008.

[slides]

- Michael Soltys

*Feasible proofs of matrix identities with Csanky’s algorithm*Abstract: We show that Csanky’s fast parallel algorithm for computing the characteristic polynomial of a matrix can be formalized in the logical theory LAP, and can be proved correct in LAP from the principle of linear independence. LAP is a natural theory for reasoning about linear algebra introduced in Soltys & Cook. Further, we show that several principles of matrix algebra, such as linear independence or the Cayley-Hamilton Theorem, can be shown equivalent in the logical theory QLA. Applying the separation between complexity classes AC\subsetneq DET, we show that these principles are in fact not provable in QLA. In a nutshell, we show that linear independence is “all there is” to elementary linear algebra (from a proof complexity point of view), and furthermore, linear independence cannot be proved trivially (again, from a proof complexity point of view).

The 7th International Workshop on Logic and Computational Complexity, LCC, affiliated with the 20th Annual IEEE Symposium on Logic in Computer Science (LICS), Chicago, June 2005.

[slides]

### Technical reports

- Michael Soltys

*Gaussian lattice reduction algorithm terminates in polynomial time*Abstract: In this short note we show that the classical Gaussian reduction algorithm for finding the shortest vector in an R^2 lattice works in polynomial time. In other words, we show that the SVP (shortest vector problem) has a polytime solution in the case of two dimensions. This has always been known, but the author could not find an explicit proof.

McMaster Computing and Software Technical Report (CAS-11-10-MS), 2011.

- Michael Soltys

*A note on finding a rational symmetric matrix for a given separable polynomial*Abstract: Given a separable polynomial p(x)∈Q[x], which splits in R[x], is it possible to find a symmetric matrix over Q whose eigenvalues are precisely the roots of p(x)? This note investigates this questions, and provides a condition on p(x) under which it is always possible to find such a matrix—the question whether such a matrix can be found unconditionally is left open. The condition we give is that the Vandermonde matrix of the roots of p(x) be (quasi) orthogonal.

McMaster Computing and Software Technical Report (CAS-08-12-MS), 2008.

- Greg Herman and Michael Soltys

*A polytime proof of correctness of the Rabin-Miller algorithm from Fermat’s little theorem*Abstract: Although a deterministic polytime algorithm for primality testing isnow known, the Rabin-Miller randomized test of primality continues being the most efficient and widely used algorithm. We prove the correctness of the Rabin-Miller algorithm in the theory V^1 for polynomial time reasoning, from Fermat’s little theorem. This is interesting because the Rabin-Miller algorithm is a polytime randomized algorithm, which runs in the class RP (i.e., the class of polytime Monte Carlo algorithms), with a sampling space exponential in the length of the binary encoding of the input number. (The class RP contains polytime P.) However, we show how to express the correctness in the language of $\V$, and we also show that we can prove the formula expressing correctness with polytime reasoning from Fermat’s Little theorem, which is generally expected to be independent of V^1. Our proof is also conceptually very basic in the sense that we use the extended Euclid’s algorithm, for computing greatest common divisors, as the main workhorse of the proof. For example, we make do without proving the Chinese Reminder theorem, which is used in the standard proofs.

arXiv:0811.3959, 2008.

[arXiv]

- David L. Parnas and Michael Soltys

*Basic Science for Software Developers*McMaster SQRL Technical Report (7), 2002.

- Michael Soltys

*A Model-Theoretic Proof of the Completeness of LK Proofs*,

McMaster Computing and Software Technical Report (CAS-06-05-MS), 1999.

(*Originally posted on*`elogic`,*March 30, 1999*.)

### Other

- David Bremner, Antoine Deza and Michael Soltys

*Foreword: selected papers from the Franco-Canadian workshop on combinatorial algorithms*Journal of Combinatorial Optimization, 16(4):323, 2008.

[doi] - Más que difícil, complejo

Interviewed by Bruno Massare for Information Technology (Argentina), May 2008. - Michael Soltys

The complexity of derivations of matrix identities.

PhD thesis, University of Toronto, 2001.