Questions tagged [provers]
Use this for a more general category that includes proof assistants, automated theorem provers and interactive theorem provers.
6
questions
9
votes
1
answer
304
views
Current status of cubical inductive families
I have the impression that cubical type theory hasn't dealt with inductive families yet. But the only source on this matter I can get is this Agda issue. What I've gathered is
Agda supports defining (...
- 3,490
20
votes
1
answer
276
views
Examples of formalisation of abelian categories
The question
I would be interested to hear about examples of formalisation of the theory of abelian categories in theorem provers, and in particular formalisations of things like the zig-zag lemma and ...
- 2,099
12
votes
1
answer
218
views
Learning materials for doing analysis (calculus) in a mechanized way
Can we collect (or maybe even write) tutorials and guides on doing analysis in various Proof Assistants? Community wiki style?
I was reading Lawrence Paulson's blog (highly recommend!) the other week ...
- 441
6
votes
0
answers
75
views
Is any theorem prover able to prove quadratization relations without knowing the proof strategy that humans used?
Motivation
In discrete optimization, our goal is often to optimize a function of binary variables, such as:
$$\tag{1} {\scriptsize
5 - 3b_1 - b_2 - b_3 + 2b_1b_3 - 3b_2b_3 + 2b_1b_2b_3 - 3b_4 + ...
- 1,105
3
votes
4
answers
199
views
What provers are using quote, quotations or quasiquotations?
This is a related question to
Is there a consolidated or partial list noting the use of quasiquotation with provers?
for which it seems there is no answer. However as there might be an answer some ...
- 2,796
6
votes
0
answers
148
views
Is there a consolidated or partial list noting the use of quasiquotation with provers?
In checking to see if any provers (proof assistants, theorem provers, interactive theorem prover) make use of quasiquotation I was quickly surprised at what started showing up with a Google search.
...
- 2,796