We describe contributions to algorithmic proof techniques for deciding the satisfiability of boolean combinations of many-variable nonlinear polynomial equations and inequalities over the real and complex numbers. In the first half, we present an abstract theory of Grobner basis construction algorithms for algebraically closed fields of characteristic zero and use it to introduce and prove the correctness of Grobner basis methods tailored to the needs of modern satisfiability modulo theories (SMT) solvers. In the process, we use the technique of proof orders to derive a generalisation of S-polynomial superfluousness in terms of transfinite induction along an ordinal parameterised by a monomial order. We use this generalisation to prove the abstract (“strategy-independent”) admissibility of a number of superfluous S-polynomial criteria important for efficient basis construction. Finally, we consider local notions of proof minimality for weak Nullstellensatz proofs and give ideal-theoretic methods for computing complex “unsatisfiable cores” which contribute to efficient SMT solving in the context of nonlinear complex arithmetic. In the second half, we consider the problem of effectively combining a heterogeneous collection of decision techniques for fragments of the existential theory of real closed fields. We propose and investigate a number of novel combined decision methods and implement them in our proof tool RAHD (Real Algebra in High Dimensions). We build a hierarchy of increasingly powerful combined decision methods, culminating in a generalisation of partial cylindrical algebraic decomposition (CAD) which we call Abstract Partial CAD. This generalisation incorporates the use of arbitrary sound but possibly incomplete proof procedures for the existential theory of real closed fields as first-class functional parameters for “short-circuiting” expensive computations during the lifting phase of CAD. Identifying these proof procedure parameters formally with RAHD proof strategies, we implement the method in RAHD for the case of full-dimensional cell decompositions and investigate its efficacy with respect to the Brown-McCallum projection operator. We end with some wishes for the future.

Actuarial risk assessment tools have been part of the initial security classification process in Canadian prisons since the 1990s. Developed initially on a white, homogenous male prison population (Hannah-Moffat, 2015b), actuarial instruments have been championed by researchers in the field of corrections and psychology as an “objective” instrument that can standardize the classification procedure (Andrews et al., 1990; Barnum & Gobeil, 2012). However, the universal application of such tools has been met with resistance, criticized for having not been validated on an Indigenous prison population and thus culturally inappropriate for use (Martel et al., 2011; Monture-Angus, 1999; Webster & Doob, 2004). This thesis intends to examine how Correctional Service Canada (CSC) has legitimated the use of actuarial tools in its initial security classification and penitentiary placement procedure. Guided by the theoretical framework of governmentality (Foucault, 1991) and the logic of elimination (Wolfe, 1994; 2006), this study undertakes a qualitative content analysis of seven CSC research documents that evaluated the empirical validity and reliability of the Custody Rating Scale (CRS), a 12-item structured instrument that calculates a prisoner’s recommended security classification level. I put forth the argument that, in the process of legitimating actuarial instruments by appealing to justifications grounded in an actuarial rationality, CSC simultaneously facilitates the ontological erasure of Indigenous people in prison that is consistent with a logic of elimination inherent in settler colonial societies.

In this thesis we see deductive systems for classical propositional and predicate logic which use deep inference, i.e. inference rules apply arbitrarily deep inside formulas, and a certain symmetry, which provides an involution on derivations. Like sequent systems, they have a cut rule which is admissible. Unlike sequent systems, they enjoy various new interesting properties. Not only the identity axiom, but also cut, weakening and even contraction are reducible to atomic form. This leads to inference rules that are local, meaning that the effort of applying them is bounded, and finitary, meaning that, given a conclusion, there is only a finite number of premises to choose from. The systems also enjoy new normal forms for derivations and, in the propositional case, a cut elimination procedure that is drastically simpler than the ones for sequent systems.

It has been 15 years since the United Nations Declaration on the Rights of Indigenous Peoples recognized the Free, Prior and Informed consent Principle, yet it has not been able to function to its fullest potential. This Thesis aims to carry out a Qualitative Comparative Analysis of the following three countries of Australia, Canada, and the United States. With the hypothesis, that the underlying factors behind this failure can be attributed to Settler-Colonialism and Global Capitalism. To carry out this study Theoretical Frameworks based on Settler-Colonial studies and a critique of the Stakeholder theory named Critical Stakeholder Analysis (CSA) will be employed. Using the existing body of research in this area of inquiry as a point of departure, this thesis attributes the failure to implement the Free, Prior, and Informed Consent principle to its fullest potential on asymmetrical power dynamics, settler-colonial structures, and profitability.