SMT solvers or an alternative for uninterpreted symbols + ∀

Question

I wanted to use Z3 to prove theorems from axioms with universal quantifiers, but Z3 seems to be a bad fit for my problem. It is able to solve some such problems, but it seems to get stuck every now and then. If not Z3, what other tools can I look to?

To give you an idea of the type of problem, I want to prove ∀….Pₙ from the axioms/assumptions {∀….P₁, …, ∀….Pₘ}. All symbols are uninterpreted and all formulas have only universal quantifiers.

I know about proof assistants, but I need a fully automatic decision procedure. While FOL is not decidable, is there a chance that there is a decision procedure for the fragment I'm interested in, either in some other tool, or perhaps, even in Z3?

Answer 1

Given the current formulation of your fragment, you're still in an undecidable fragment of FOL. If you could restrict what your P are allowed to talk about then you might end up in a decidable fragment (e.g. monadic, guarded, effectively propositional, there are a few).

Besides SMT solvers and proof assistants, there is a whole class of automated theorem provers that are refutationally complete for such problems (i.e. if there is a proof of inconsistency they will eventually find it), which SMT solvers are not. CASC is a good place to find out about such solvers as it's a compeittion focussing on these kinds of problems. Vampire is a very good example (note, I am a developer of Vampire).

Answer 2

These sorts of questions come up often, alas SMT solvers are just not a good match with quantifier heavy problems. The best you have is specifying patterns (See E-matching based quantifier instantiation for details). But it is quite fragile and definitely not that terribly easy to use.

Your best bet, against what you wanted, is to use proof assistants; and hope that their automated tactics (such as sledgehammer of Isabelle) can discharge the proofs without the need for much user intervention.

This is, of course, general advice without actually knowing anything about your specific problem. If you post a concrete instance of it, you might get a better answer in terms of if there might be another way to model it using z3.