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, 3 months
  • Last seen more than a week ago
  • Menlo Park, CA, United States
0 votes
0 answers
66 views

How to check a Zenon-generated proof with Coq?

6 votes
1 answer
173 views

Understanding the complete lattice definition of impredicativity

5 votes
1 answer
180 views

List of general purpose Coq sublanguages for defining custom tactics

12 votes
1 answer
282 views

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

4 votes
2 answers
206 views

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

2 votes
2 answers
88 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
345 views

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

12 votes
2 answers
570 views

What is a universe?

3 votes
1 answer
164 views

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

14 votes
2 answers
308 views

Tools for checking the consistency of a type theory

5 votes
1 answer
167 views

How to implement first-order relational structures in Coq?

5 votes
1 answer
134 views

Libraries of formally stated theorems with proofs verified by humans

5 votes
1 answer
135 views

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

4 votes
2 answers
114 views

Proof Review: Basic theorem about ternary relations in Coq

8 votes
1 answer
423 views

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

10 votes
1 answer
253 views

Is there a Mizar-like sublanguage for Coq?

5 votes
2 answers
173 views

Are there any provers based on a paraconsistent logic?

5 votes
3 answers
499 views

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

13 votes
3 answers
348 views

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

8 votes
2 answers
186 views

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

3 votes
1 answer
192 views

What is an eliminator?

15 votes
1 answer
264 views

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

38 votes
3 answers
1k views

What is predicativity?

18 votes
2 answers
591 views

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

11 votes
2 answers
119 views

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

16 votes
2 answers
194 views

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

15 votes
4 answers
391 views

Are there any well-known Internal DSL Proof Assistants?