# Looking for C++ library that symbolically solves systems of set-subset equations

I'm looking for a library (preferably C++ and open source) which can solve and/or reduce systems of equations about sets and subsets. Note that I'm not asking for something which computes results of operation like set intersection, etc., but rather something which can take a system of set equations as input and output either: an optimized list of primitive operations to perform, or a simplified form of the input where sections which cannot produce a result are marked and/or removed.

In other words, I'm looking for a library which works with a system of set-subset equations without having to be given what is actually in the sets, in the same way that algebra can be performed without knowing the exact number contained in a variable.

For example, if I gave it input saying set A is a subset of B and B is a subset of C, and C is empty, then it should tell me A is empty. However if I told it set B is the union of sets B_0 and B_1 where only B_0 is a subset of C, then it should not claim that C empty implies A is empty, because A might come from B_1.

If the library were to output an optimized list of operations, the output for the latter example would include "find B_1 as a dependency of A", but would not include anything saying to find B, B_0, or C because it was proved symbolically that they don't contribute to the result.

Edit: On thinking it further, I might be leaving out an important detail. I need to be able to specify that some of the sets are pairs or tuples of elements from other sets. For example say A is pairs (x, y) and B is pairs (y, z), find all results (a, z) where A.y == B.y; I don't care what the value of "y" is but it must exist. Things the library could do with that (based on additional input) would be to produce output like "there can't exist a y such that A.y == B.y" or "A.y already equals B.y for all A,B".

I imagine that a large complete math engine like Mathematica, R, etc. might include something like this, but I am hoping to find a lighter weight version targeted to just this specific domain.

• It sounds like the problems you want to solve could be stated purely in terms of first-order logic. So, you could look into generic logic-programming tools. – Kodiologist Mar 8 '17 at 4:24
• Indeed, I am currently using a generic logic programming library, Castor, in my code. (Which, I suppose, is what got me thinking of the problem in these terms anyway.) I could write the rules of inference as logic relations... – Dennis Mar 8 '17 at 23:10