What algorithm does tauto use to prove prop tautologies

Stream: general

[HWeigel]

What are the guarantees/complexity of the tauto tactic algorithm? Are there any relevant sources/literature?

Most of the existing literature on propositional logic algorithms seem to convert validity-checking into a SAT problem, but that doesn't seem to be what tauto.lean does.

[Mario Carneiro]

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mathlib.20sat.20solvers/near/265031540 and the associated conversation. The short answer is that no one knows what tauto is doing, and its completeness is questionable

[Kevin Buzzard]

If it works in my proof, who cares what it's doing!

[Patrick Massot]

Mario, that's not true, @Simon Hudon knows what tauto is doing, and users knows that it's doing it faster than its competitors. Speed is much more important than completeness because it means we can actually use it when we want to get rid of an obvious part of a proof and we don't have to come back and remove it later for speed reasons.

[Mario Carneiro]

I'm not making a value judgment on its usefulness. But it is not a "principled" SAT solver, it is a collection of heuristics. This has advantages and disadvantages: heuristic provers tend to do better than "principled" solvers on common examples, and they might come up with shorter proofs too. On the other hand they might take exceedingly long, time out, or outright fail on problems where a principled solver would succeed, because the heuristics were not good for that particular example.

Moreover, principled solvers may not always be available for a domain. There is no decision procedure for first order logic, because it is undecidable, so heuristics are the best you can do. tauto accepts this and so it can handle some problems that are not actually SAT goals; itauto is a principled solver and so outright rejects anything that is not strictly SAT, which is probably not what you want if your goal is "almost" SAT.

[Gabriel Ebner]

I agree with Patrick here. LJT is not such a great calculus for proof search in classical logic (for intuitionistic logic it's not great either, but the alternatives are not much better). And as we see, it really doesn't seem to scale well in practice on mathlib.

[Gabriel Ebner]

The question about the solved subset is completely orthogonal and imho a red herring. tauto isn't faster because it applies some non-propositional rules. itauto isn't slow because it only does SAT.

[Mario Carneiro]

I am not arguing that itauto is better for mathlib than tauto. We already did the experiment and it clearly isn't. Mathlib is classical anyway

[Gabriel Ebner]

Then I probably misunderstood your point.

[Mario Carneiro]

But I think we can still do better when it comes to mathlib sat solvers, and get something that is at least complete for SAT and preferably FOL

[Mario Carneiro]

My point is not that either is better, as I said there are advantages and disadvantages to heuristic search vs decision procedures. The best sat solvers use a mixture of both approaches, with heuristics to solve the common cases and mixing in occasional steps to ensure completeness

[Gabriel Ebner]

I think that complete for SAT is more useful than complete for FOL (in mathlib). But I am just as confident as you that we can get something great in mathlib.