Skip to main content
Greg Nisbet's user avatar
Greg Nisbet's user avatar
Greg Nisbet's user avatar
Greg Nisbet
  • Member for 2 years, 5 months
  • Last seen this week
  • Menlo Park, CA, United States
38 votes
3 answers
1k views

What is predicativity?

18 votes
2 answers
641 views

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

16 votes
2 answers
197 views

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

15 votes
4 answers
403 views

Are there any well-known Internal DSL Proof Assistants?

15 votes
1 answer
275 views

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

14 votes
2 answers
336 views

Tools for checking the consistency of a type theory

13 votes
3 answers
359 views

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

12 votes
2 answers
589 views

What is a universe?

12 votes
1 answer
307 views

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

11 votes
2 answers
121 views

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

10 votes
1 answer
271 views

Is there a Mizar-like sublanguage for Coq?

8 votes
1 answer
470 views

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

8 votes
2 answers
192 views

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

6 votes
1 answer
179 views

Understanding the complete lattice definition of impredicativity

6 votes
1 answer
151 views

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

5 votes
1 answer
140 views

Libraries of formally stated theorems with proofs verified by humans

5 votes
1 answer
174 views

How to implement first-order relational structures in Coq?

5 votes
3 answers
537 views

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

5 votes
2 answers
184 views

Are there any provers based on a paraconsistent logic?

5 votes
1 answer
188 views

List of general purpose Coq sublanguages for defining custom tactics

5 votes
4 answers
3k views

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

4 votes
2 answers
210 views

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

4 votes
1 answer
204 views

What is an eliminator?

4 votes
2 answers
121 views

Proof Review: Basic theorem about ternary relations in Coq

3 votes
1 answer
175 views

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

3 votes
1 answer
117 views

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

2 votes
1 answer
72 views

Strategies for representing proofs of equality

2 votes
3 answers
572 views

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

2 votes
2 answers
110 views

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

2 votes
1 answer
70 views

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