Skip to main content

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 with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
10 votes
0 answers
187 views

Is there a proof assistant (or an embedding) for the (co)end calculus?

A Higher-Order Calculus for Categories describes a system where you can conveniently perform manipulations with categories, functors, Yoneda embeddings etc. An example of the rules is: $$\frac{\Gamma ,...
Trebor's user avatar
  • 4,015
7 votes
0 answers
78 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 + ...
Nike Dattani's user avatar
  • 1,165
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 ...
Julián's user avatar
  • 143
2 votes
0 answers
68 views

Tool for typing mathematical physics, e.g. differential geometry

Many expressions in mathematical physics use a rather sloppy notation, e.g. the Lie bracket on a vector field is defined using ambiguous notation, where $X : M \rightarrow TM$ is first defined as a ...
user2361's user avatar
1 vote
0 answers
61 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 &...
Eric Anderson's user avatar