Are automatic theorem provers on-topic?

Question

Proposal: Proof Assistants

One of the suggested names for Proof Assistants SE is provers, which is currently getting a lot of popularity due to being simpler than proof-assistants (with or without hyphen).

But this raises a concern: There are some things using the name "prover" other than proof assistants, namely automated theorem provers such as Z3 (aka "Z3 Theorem Prover"). Should questions about automated theorem proving, especially when it is not directly connected to proof assistants, be on-topic on this site? (I found a well-received question example regarding "intuitionistic theorem provers with SMT solvers". I guess "intuitionistic theorem provers" refers to the proof assistants, while "SMT solvers" refers to some of the automatic theorem provers.)

Answer 1

I would prefer to err on the side of inclusiveness, so yes. And the two communities really should be talking to each other more than they do.

Answer 2

Yes

Even if you put all the different branches together, formal methods is a rather niche field, and I don't think there would be so much success having separate sites for ATPs and ITPs. At the same time there is much to be gained by having a shared user base, since the combination of computer science and mathematics knowledge you need in ITPs is also useful in ATP applications, and vice versa.

I think we should be fairly liberal towards topic selection, and allow anything in formal methods, even if "proof assistants" is the title and the main draw. Here are some rough examples that I think should be on topic:

• How do I prove this theorem in Lean?
• Trouble installing Vampire prover
• Are there programming languages that use SMT solvers in the type checker?
• How can I use a SAT solver to solve a sudoku problem?

Answer 3

It's worth pointing out that ATP have been integrated in ITP with Isabelle's Sledgehammer. From what I've heard, Sledgehammer is very useful in hacking away goals and used on a daily basis by many working with Isabelle.

I feel that instead of focusing on a specific community, it might be more expedient to formulate a common goal, which I would take is proving mathematical theorems with the help of a computer. Everyone who's interested in this goal should feel welcome in this SE community, no matter their academic community.

Focusing on a goal might also provide more robust to new developments. Today, ITP and ATP are tools for doing mathematics on a computer, but in the future there might be other tools on the horizon (using machine learning or what have you).

Answer 4

While I won't argue that theorem provers should be completely off topic for this site, I think naming the site provers would really distract from the purpose of the site, namely proof assistants. I should emphazise that the term prover commonly refers to a automated theorem provers, and not proof assistants. This could also be confusing because a prover also corresponds to a class of software which is very different from a proof assistant.

Automated theorem proving deals with a (rather small) class of algorithms for proof search, whereas proof assistants are (often large and complicated) frameworks for formalizing proofs. So while automated theorem proving might be a small part of a proof assistant, it is far from representing the whole.

Answer 5

Even though I first voted on "provers", I think it's worth distinguishing between ITPs and ATPs (interactive vs automated). The original proposal for this new SE site did not say it was for formal methods in general which may make the scope too broad. So that choice of name could be misleading unless we explicitly broaden the scope.

Quoting from QED survey (omitting obvious references for clarity), which I mentioned in my proposal:

1.2 Scope: Domain and Literature

We consider proof engineering research in the context of interactive theorem provers (ITPs) or proof assistants (used interchangeably with ITPs in this survey) that satisfy the de Bruijn criterion, which requires that they produce proof objects that a small proof-checking kernel can verify; the general workflow of such tools is illustrated in Figure 1.1. That is, we consider proof assistants such as Coq, Isabelle/HOL, HOL Light, and Agda; we do not consider program verifiers, theorem provers, and constraint solvers such as Dafny, ACL2, and Z3 except when contributions carryover.

This might be a good guiding principle for our future community as well. That is, ATPs like Z3 should not be hard off-topic, but the main focus should still be on proof assistants/ITPs.

Answer 6

There are a large amount of model checking tools I took a look at when learning about formal methods for the first time. There is a variation between some like TLA+ which seem more "mathy" and some like CBMC which seem more automatic. These automatic tools are kind of specialized but they don't seem off-topic exactly. Anyhow most of the work is in writing the correct apecifications and definitions not writing proofs.