Conjecture generation

[rschwiebert]

I don't doubt there have been advances at conjecture generation, but not being very familiar with the field I need to ask.

Specifically, I've been using souffle to manage a knowledge-base of facts about objects in the category of rings (https://ringtheory.herokuapp.com/). Each object either has or lacks certain conditions. There is a file of stored clauses that I run against this to deduce as much as possible.

Given some collection of conditions, I would like to do this:

1. From all the stored examples, see if one exists with those conditions, and if so, stop here.
2. If none exist, create a hypothetical object with those properties and run the body of logic against it. If there is a contradiction, stop here.
3. If no contradictions are found, then either a) an example exists for the set or b) there's a new theorem to be proven that none like that can exist. Return the conditions for further study and stop.

Obviously there is a combinatoric explosion here. I was wondering what is known about efficiently finding conjectures like this and whether or not anyone was having success doing it with souffle.

Thanks!