Questions tagged [software-request]
This tag is used for questions that ask for software with a certain property or goal, such as automated theorem provers for equational logic. If the question is not specifically for software consider using the tag by reference-request.
5
questions
2
votes
1
answer
69
views
Checking if a goal is *definitely wrong* by testing it against random examples in Coq
I'm currently poking around in a medium-sized Coq codebase that I didn't write and am not very familiar with ... and I'm trying off and on to make progress on some lemmas where the proof attempt was <...
- 3,073
4
votes
2
answers
185
views
Which proof assistants implement Church's rule?
Church's rule (CR) is one of the hallmarks of constructive mathematics, and is an admissible rule in a wide variety of constructive theories (you might consider CR to be a requirement for constructive ...
- 165
-1
votes
1
answer
106
views
Implementability of proof assistants for Infinitary logics with finite many terms
Infinitary logic is a natural consequence of extending the length of proofs of first-order logic to a infinite ordinal level.
By definition, since proof lengths are infinitely long, one should not ...
- 279
1
vote
0
answers
62
views
Embedding proof assistance in an application
Context
Perhaps this is too open-ended a question for StackExchange, in which case I apologize, but otherwise here goes:
I have a project I'm toying around with, the core of which is what I'd call &...
- 111
2
votes
0
answers
65
views
Have Hyperdoctrines been formalized?
I was thinking of formalizing them myself for a project if they haven't been already, and I looked in libraries and couldn't find anything.
I was thinking of coq in particular because it's the only ...
- 143