Nick Koh will present his FPO "Consequence-Finding in Theories of Arithmeticon" on Wednesday, 7/15/26 at 3pm in CS 402. The members of his committee are as follows: Examiners: Zak Kincaid (adviser), Pravesh Kothari, David Walker Readers: Aarti Gupta and Zak Kincaid Abstract: Given a formula F in a first-order theory, what is the strongest formula of a certain form that is entailed by F? In program analysis and verification, programs are often analyzed through the lens of logic, e.g., by translating fragments of code into logical formulas, and problems like loop summarization and ranking function synthesis can be reduced to instances of consequence-finding. This thesis considers consequence-finding modulo the theory of linear integer-real arithmetic (LIRA) and the theory of linear integer-real rings (LIRR). To aid consequence-finding for these theories, we introduce an algorithmic framework of concept spaces and local abstractions. Concept spaces allow us to frame consequence-finding using representations beyond formulas, while local abstractions formalize a strategy to find consequences by generalizing sampled models of a formula. For LIRA, we consider the problem of finding the strongest conjunction of linear inequalities entailed by an existential formula. This corresponds to the problem of computing the closed convex hull of its set of models. We decompose this into a series of simpler abstraction problems, and compute the convex hull using a combination of local abstractions. For LIRR, we consider the problem of finding the set of all polynomial inequalities and integrality constraints entailed by an existential formula in polynomial integer-real arithmetic. In the standard model of integers, polynomial arithmetic is undecidable, and LIRR is a new theory of polynomial integer-real arithmetic that gives up completeness in exchange for not only decidability, but also complete consequence-finding. We introduce algebraic cones and lattices to represent sets of consequences, and solve the consequence-finding problem using a local abstraction. More broadly, these instances show that concept spaces and local abstractions are useful for consequence-finding in general.