Automatic theorem proving question

Stream: new members

[Hungry Applicative]

Hi, this is a question about Lean, but also about automatic theorem proving in general.

I am working on a project where we want to automatically prove/decide lots of theorems in first-order logic of the form

$$∀ \vec{x}_1 P_1(\vec{x}_1) , \dots , ∀ \vec{x}_n P_n(\vec{x}_n) \;\vdash\; ∀ \vec{y} Q(\vec{y})\,,$$

where the formulas $P_1(\vec{x}_1) , \dots , P_n(\vec{x}_n), Q(\vec{y})$ are quantifier-free formulas. So all formulas have a very simple structure as there is only "one layer" of quantifiers. I believe this class of problems is decidable, but I don't know what it is called. As an example of this type of problem, imagine that the formulas on the left of the turnstile are group or ring axioms like

$$∀x y z.\, (x⋅y)⋅z=x⋅(y⋅z)\,,$$

and the formula on the right is a theorem about groups or rings.

Is there any theorem prover out there that can decide these types of problems completely automatically? I've looked at SMT solvers, but they seem to have difficulties dealing with the quantifiers. Lean has some very impressive automation facilities. Do you think I can use Lean for this type of problem? Is there an other type of tool that is better suited?

[Kevin Buzzard]

The word problem for groups is undecidable, and can't you encode it in your system?

[Hungry Applicative]

Thanks for the reply, and I'm sorry, I should have investigated that. I just assumed that my problems were simple enough and most of the time I want to prove identities from identity axioms, with constraints on the interpretations of the signature. but if I understand the gist of these word problems, many of them might actually be expressed as instances of my problem.

But giving up on decidability, are there any automatic provers that are good at solving such problems? Are SMT solvers my best bet? I've had some luck with them so far, but the results are fragile—simply rearranging assertions can make the solver time out. They seem to be more geared towards theory reasoning which I don't really need, and also struggle with quantifiers. So I'm thinking, surely there must be provers that make different tradeoffs and are thereby better suited for my problem?

[Reid Barton]

My understanding is this is the domain of provers such as https://en.wikipedia.org/wiki/E_(theorem_prover) and https://en.wikipedia.org/wiki/Vampire_(theorem_prover).