@article {988,
	title = {On the complexity of quantified linear systems},
	journal = {Theoretical Computer Science},
	volume = {518},
	year = {2014},
	pages = {128{\textendash}134},
	abstract = {In this paper, we explore the computational complexity of the conjunctive fragment of the first-order theory of linear arithmetic. Quantified propositional formulas of linear inequalities with (k-1) quantifier alternations are log-space complete in ΣkP or ΠkP depending on the initial quantifier. We show that when we restrict ourselves to quantified conjunctions of linear inequalities, i.e., quantified linear systems, the complexity classes collapse to polynomial time. In other words, the presence of universal quantifiers does not alter the complexity of the linear programming problem, which is known to be in P. Our result reinforces the importance of sentence formats from the perspective of computational complexity.},
	doi = {10.1016/j.tcs.2013.08.001},
	author = {Salvatore Ruggieri and Eirinakis, Pavlos and Subramani, K and Wojciechowski, Piotr}
}
@article {985,
	title = {On quantified linear implications},
	journal = {Annals of Mathematics and Artificial Intelligence},
	volume = {71},
	number = {4},
	year = {2014},
	pages = {301{\textendash}325},
	abstract = {A Quantified Linear Implication (QLI) is an inclusion query over two polyhedral sets, with a quantifier string that specifies which variables are existentially quantified and which are universally quantified. Equivalently, it can be viewed as a quantified implication of two systems of linear inequalities. In this paper, we provide a 2-person game semantics for the QLI problem, which allows us to explore the computational complexities of several of its classes. More specifically, we prove that the decision problem for QLIs with an arbitrary number of quantifier alternations is PSPACE-hard. Furthermore, we explore the computational complexities of several classes of 0, 1, and 2-quantifier alternation QLIs. We observed that some classes are decidable in polynomial time, some are NP-complete, some are coNP-hard and some are  ΠP2Π2P -hard. We also establish the hardness of QLIs with 2 or more quantifier alternations with respect to the first quantifier in the quantifier string and the number of quantifier alternations. All the proofs that we provide for polynomially solvable problems are constructive, i.e., polynomial-time decision algorithms are devised that utilize well-known procedures. QLIs can be utilized as powerful modelling tools for real-life applications. Such applications include reactive systems, real-time schedulers, and static program analyzers.},
	doi = {10.1007/s10472-013-9332-3},
	author = {Eirinakis, Pavlos and Salvatore Ruggieri and Subramani, K and Wojciechowski, Piotr}
}
