How do computer algebra systems like Sage perform operations on infinite structures

Question

Allow me to preface this question with a little bit of background:

I am not a computer scientist. I have coded some small programs in Python and Java to do very basic things like generate fractals and analyze fractal dimension. However, this does not leave me particularly well-equipped to understand the inner workings of data structures or anything of the sort.

Onto the question at hand:

I am a graduate student working in model theory and set theory. For my thesis, I am interested in the use of computer algebra systems to solve model theoretic problems. Primarily, I'm interested in something capable of performing the following type of computation:

function equivCheck(A,B):
    if isElementarilyEquivalent(A,B):
        return true
    else: return false

Here are my questions:

1. First, does a CAS capable of performing such types of computations exist? Sources would be greatly appreciated here.
2. If not: Where would you start?

With regards to the second question, I am aware that CASs like Sage are able to perform computations on "infinite" objects. For example, given an infinite group $G$, Sage can tell me whether or not $G$ is Abelian. My question is how? How is this type of "infinite" structure being stored in memory that such a function can run and produce an output?

It seems like the model theoretic problem could be approached from a similar angle. I did try going through the official documentation for Sage, but there wasn't too much as far as I could tell on how these objects are being represented in memory.

(I am honestly not sure if I am in the right place to be asking such a question. I thought I should post here instead of CS.SE since I imagine that elementary equivalence of structures is not really within the scope of CS. We also did have a CAS tag, so I figured I would try here first. Please let me know if the question is off-topic here.)

Answer 1

Elementary equivalence of infinite structures is not computer-checkable in any good sense. For example:

There is a uniformly computable sequence of structures $(\mathcal{A}_i)_{i\in\mathbb{N}}$ such that $$\{(u,v):\mathcal{A}_u\equiv\mathcal{A}_v\}$$ is incomputable.

This is actually quite simple: letting $\mathcal{A}_i$ be the expansion of $(\mathbb{N}; 0,1,+)$ by a unary predicate $U_i$ with $U_i^{\mathcal{A}_i}=\{k: \Phi_i(i)[k]\downarrow\}$, we have $\mathcal{A}_i\equiv(\mathbb{N};0,1,+,\emptyset)$ iff $i$ is not in the Halting Problem.

---

In general, you'll only have a hope of doing this if the structures you're looking at are known ahead of time to have their theories determined by very finitary data. And even then you'll need to argue that the appropriate data can be "read off" the descriptions of the structures you're feeding the computer in an appropriate way.