User Greg Nisbet

38 votes

3 answers

1k views

What is predicativity?

asked Feb 11, 2022 at 3:08

18 votes

2 answers

684 views

What is the difference between judgmental equality, definitional equality, and equality types?

asked Feb 10, 2022 at 16:32

16 votes

2 answers

204 views

Are there any proof assistants or theorem provers based on the method of analytic tableaux?

asked Feb 8, 2022 at 19:32

15 votes

4 answers

412 views

Are there any well-known Internal DSL Proof Assistants?

asked Feb 8, 2022 at 18:19

15 votes

1 answer

288 views

Are there automated theorem provers for constructive logics? What strategy do they use?

asked Feb 11, 2022 at 17:07

14 votes

2 answers

352 views

Tools for checking the consistency of a type theory

asked Feb 20, 2022 at 22:14

13 votes

3 answers

370 views

What are the possible kinds of type theories or logics with quotients?

asked Feb 13, 2022 at 17:33

12 votes

2 answers

624 views

What is a universe?

asked Feb 26, 2022 at 21:47

12 votes

1 answer

314 views

Naming conventions (letter case, underscores, &c) for Coq

asked Mar 7, 2022 at 2:34

11 votes

2 answers

122 views

Proof assistants or libraries in proof assistants for working with model theory

asked Feb 9, 2022 at 4:29

10 votes

1 answer

282 views

Is there a Mizar-like sublanguage for Coq?

asked Feb 15, 2022 at 3:25

9 votes

1 answer

545 views

What are some automated theorem generators? What background logic do they use and what heuristics do they use for theorem-goodness?

asked Feb 15, 2022 at 20:15

8 votes

2 answers

196 views

What is the closest you can get to introducing and discharging hypotheses in metamath?

asked Feb 12, 2022 at 22:32

6 votes

1 answer

180 views

Understanding the complete lattice definition of impredicativity

asked Mar 13, 2022 at 19:21

6 votes

1 answer

154 views

Architecture of Isabelle: What parts are written in SML? What parts are written in Scala? What does the boundary look like?

asked Feb 17, 2022 at 23:14

5 votes

1 answer

141 views

Libraries of formally stated theorems with proofs verified by humans

asked Feb 17, 2022 at 23:43

5 votes

1 answer

180 views

How to implement first-order relational structures in Coq?

asked Feb 19, 2022 at 16:57

5 votes

3 answers

571 views

How do you import part of the standard library in Coq?

asked Feb 13, 2022 at 22:12

5 votes

2 answers

189 views

Are there any provers based on a paraconsistent logic?

asked Feb 14, 2022 at 22:57

5 votes

1 answer

192 views

List of general purpose Coq sublanguages for defining custom tactics

asked Mar 12, 2022 at 1:22

5 votes

4 answers

3k views

Less ridiculous way to prove that an Ascii character compares equal with itself in Coq

asked Jun 27 at 3:15

4 votes

2 answers

212 views

Coq defining a hierarchy of collections of integers with infinitely many "levels"

asked Mar 7, 2022 at 1:04

4 votes

1 answer

212 views

What is an eliminator?

asked Feb 12, 2022 at 4:17

4 votes

2 answers

124 views

Proof Review: Basic theorem about ternary relations in Coq

asked Feb 17, 2022 at 1:15

3 votes

1 answer

187 views

Code Review: Proving that a simple propositional logic satisfies Aristotle's Thesis

asked Feb 26, 2022 at 1:28

3 votes

1 answer

130 views

How to use SSReflect to prove commutativity and associativity of addition idiomatically?

asked Jun 21 at 5:24

2 votes

1 answer

82 views

Strategies for representing proofs of equality

asked Jun 24 at 15:53

2 votes

3 answers

629 views

What is a positive coinductive type and why are they so bad?

asked Jun 30 at 1:44

2 votes

2 answers

132 views

Code Review: $\mathbb{Z}[\sqrt{-2}]$ is an integral domain

asked Jul 5 at 22:09

2 votes

1 answer

72 views

Checking if a goal is definitely wrong by testing it against random examples in Coq

asked Jun 17 at 23:25

Stack Exchange Network

45 Questions

What is predicativity?

What is the difference between judgmental equality, definitional equality, and equality types?

Are there any proof assistants or theorem provers based on the method of analytic tableaux?

Are there any well-known Internal DSL Proof Assistants?

Are there automated theorem provers for constructive logics? What strategy do they use?

Tools for checking the consistency of a type theory

What are the possible kinds of type theories or logics with quotients?

What is a universe?

Naming conventions (letter case, underscores, &c) for Coq

Proof assistants or libraries in proof assistants for working with model theory

Is there a Mizar-like sublanguage for Coq?

What are some automated theorem generators? What background logic do they use and what heuristics do they use for theorem-goodness?

What is the closest you can get to introducing and discharging hypotheses in metamath?

Understanding the complete lattice definition of impredicativity

Architecture of Isabelle: What parts are written in SML? What parts are written in Scala? What does the boundary look like?

Libraries of formally stated theorems with proofs verified by humans

How to implement first-order relational structures in Coq?

How do you import part of the standard library in Coq?

Are there any provers based on a paraconsistent logic?

List of general purpose Coq sublanguages for defining custom tactics

Less ridiculous way to prove that an Ascii character compares equal with itself in Coq

Coq defining a hierarchy of collections of integers with infinitely many "levels"

What is an eliminator?

Proof Review: Basic theorem about ternary relations in Coq

Code Review: Proving that a simple propositional logic satisfies Aristotle's Thesis

How to use SSReflect to prove commutativity and associativity of addition idiomatically?

Strategies for representing proofs of equality

What is a positive coinductive type and why are they so bad?

Code Review: $\mathbb{Z}[\sqrt{-2}]$ is an integral domain

Checking if a goal is definitely wrong by testing it against random examples in Coq