12

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.)

New contributor
Bubbler is a new contributor to this site. Take care in asking for clarification, commenting, and answering. Check out our Code of Conduct.
3
  • 4
    While asking this question here and now is perfectly fine, now that the proposal has completed the commit phase it will soon have a Q&A site (possibly proofassistants.stackexchange.com) along with an associated meta site (possibly proofassistants.meta.stackexchange.com), I personally am waiting for the meta site to go live before asking such questions. The reason being that after some time this site (area51.meta.stackexchange.com) will be an afterthought of those using the Proof Assistants site and it will not occur to many down the road to look here for such information. :-)
    – Guy Coder
    Nov 23 at 8:17
  • 1
    @GuyCoder Yeah, I guess it's not too late to ask this again in the site's meta after we see some actual demand (i.e. actual questions posted on the site) about expanding the scope.
    – Bubbler
    Nov 24 at 7:19
  • Created chat room for various reasons, one being so that users don't have to communicate by comments.
    – Guy Coder
    Nov 24 at 11:51
16

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.

New contributor
Andrej Bauer is a new contributor to this site. Take care in asking for clarification, commenting, and answering. Check out our Code of Conduct.
2
  • I will probably repost this in the meta site once it becomes active. Would constraint programming and other forms of logic be allowed such as s(CASP) ?
    – Guy Coder
    Nov 23 at 15:34
  • 4
    Provers should not be considered off-topic, but should not be the name, as proof assistants are not provers. Nov 23 at 16:21
15

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?
New contributor
Mario Carneiro is a new contributor to this site. Take care in asking for clarification, commenting, and answering. Check out our Code of Conduct.
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.

New contributor
Couchy is a new contributor to this site. Take care in asking for clarification, commenting, and answering. Check out our Code of Conduct.
1
  • While you can probably craft a definition to exclude ITPs from being "theorem provers", most ITPs contain a nontrivial ATP component already, and the degree to which they don't already subsume what ATPs can do (usually by calling them) is mostly a historical accident. Additionally, the use of the term "prover" or "theorem prover" to refer to ITPs is not uncommon, pedantry notwithstanding. (For example, check out the title and URL of leanprover.github.io .) Nov 24 at 3:57
2

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.

New contributor
k4rtik is a new contributor to this site. Take care in asking for clarification, commenting, and answering. Check out our Code of Conduct.

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .