Skip to main content

All Questions

Tagged with
3 votes
0 answers
33 views

Are questions about automated theorem provers on topic?

I asked the what is needed to move from design by contract to using a proof assistant? not realizing that proof assistant seems to imply interactivity. I now realize I meant something else - automated ...
Bruce Adams's user avatar
5 votes
1 answer
26 views

Code Reviews on topic?

There are two related questions here: Question 1: Reviewing proof scripts? I just formalized a type system in Coq (and I'm almost certain it is not "idiomatic Coq"), would it be appropriate ...
Alex Nelson's user avatar
  • 1,574
6 votes
0 answers
38 views

Are questions about categorical logic on topic?

Are questions about categorical logic and the related category theory are on topic on this website? Categorical logic is strongly connected to type theory and the semantic of (many) proof assistants, ...
Nico's user avatar
  • 722
4 votes
1 answer
68 views

Policies on answers porting code

In questions such as this, the OP asks for proofs, definitions, methodology etc. on a specific topic, but does not require a specific proof assistant*. There will imaginably be answers that are purely ...
Trebor's user avatar
  • 4,025
4 votes
2 answers
107 views

Should we allow Rosetta-Stone style questions?

This question was raised in the comments of this question about idiomatic ways to prove the associativity of append. A Rosetta Stone style question would describe some kind of task in a prover-neutral ...
Greg Nisbet's user avatar
  • 3,095
13 votes
2 answers
182 views

Is this for assistants only, excluding automated provers?

Do automated theorem provers fall under the scope of this new Stack Exchange sub-site, as well as Proof Assistants?
Reubend's user avatar
  • 519