Greg Nisbet's user avatar
Greg Nisbet's user avatar
Greg Nisbet's user avatar
Greg Nisbet
  • Member for 2 years
  • Last seen this week
  • Menlo Park, CA, United States
37 votes
3 answers
1k views

What is predicativity?

18 votes
2 answers
509 views

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

16 votes
2 answers
193 views

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

15 votes
4 answers
384 views

Are there any well-known Internal DSL Proof Assistants?

15 votes
1 answer
258 views

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

14 votes
2 answers
288 views

Tools for checking the consistency of a type theory

13 votes
3 answers
333 views

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

12 votes
1 answer
264 views

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

11 votes
2 answers
116 views

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

11 votes
2 answers
539 views

What is a universe?

10 votes
1 answer
242 views

Is there a Mizar-like sublanguage for Coq?

8 votes
1 answer
317 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
180 views

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

6 votes
1 answer
170 views

Understanding the complete lattice definition of impredicativity

5 votes
1 answer
132 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
132 views

Libraries of formally stated theorems with proofs verified by humans

5 votes
1 answer
151 views

How to implement first-order relational structures in Coq?

5 votes
3 answers
412 views

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

5 votes
2 answers
172 views

Are there any provers based on a paraconsistent logic?

4 votes
2 answers
107 views

Proof Review: Basic theorem about ternary relations in Coq

4 votes
2 answers
199 views

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

3 votes
1 answer
162 views

List of general purpose Coq sublanguages for defining custom tactics

3 votes
1 answer
155 views

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

3 votes
1 answer
186 views

What is an eliminator?

2 votes
2 answers
83 views

Coq produce instance of a type `{x : T | P x}` inside an explicit definition given an `x'` of type `T`

1 vote
1 answer
289 views

Form of intros in Coq specifically for `forall` and explicitly for `->`

0 votes
0 answers
65 views

How to check a Zenon-generated proof with Coq?