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.
26
questions
5
votes
0
answers
57
views
Open source implementations of euclidean geometery automated theorem provers
I plan to work on extending a theorem prover which is specialised in generating proofs for questions based in euclidean geometry which is taught to high school students to introduce them to the ideas ...
- 51
2
votes
1
answer
72
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,105
4
votes
2
answers
189
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
112
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
66
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
2
votes
0
answers
71
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 ...
- 21
5
votes
1
answer
187
views
Is there an easy-to-learn GUI of proof assistants for teenagers in maths education?
I'm a high school sophomore and I have been interested in Interactive Theorem Proving for a year or two. I found it extremely hard for my peers (lack of knowledge in mathematical logic, type theories ...
- 51
2
votes
1
answer
159
views
Does there exists a logical format so that my app can export in that format, and the existing popular proof assistants can take it as input?
I'm creating a "CAS for category theory / homological algebra" in C++ that "supports proofs". Although it is feature creep, I was wondering if there exists a format that my app ...
- 303
10
votes
0
answers
188
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 ,...
- 4,087
7
votes
0
answers
79
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,175
32
votes
2
answers
2k
views
What work has been done on computationally intensive proofs?
Fifty years ago, few would have imagined that the process of verifying the correctness of a known proof of a mathematical theorem might be so costly that the mathematical community would hesitate to ...
- 505
9
votes
1
answer
183
views
Generating valid statements without a proof goal
Given some initial list of assumptions, I'd like to generate some true statements which follow from them without seeking a specific proof goal. I only need a small number of consequences from those ...
- 519
5
votes
1
answer
192
views
List of general purpose Coq sublanguages for defining custom tactics
I've been tweaking the Coq plugin template recently to try to get a feel for writing custom Coq tactics in OCaml.
It's tricky. You need to define an .mlg file (...
- 3,105
14
votes
2
answers
352
views
Tools for checking the consistency of a type theory
My question is twofold:
How do you define consistency (analogously to the concept in first-order logic) in the context of a type theory?
Are there any tools that can check consistency?
I have seen a ...
- 3,105
5
votes
1
answer
141
views
Libraries of formally stated theorems with proofs verified by humans
This answer by Kevin Buzzard talks, among other things, about incremental progress made in Lean's mathlib vs Isabelle.
There's a lot in that answer that I don't understand, but one thing that seems ...
- 3,105
10
votes
1
answer
282
views
Is there a Mizar-like sublanguage for Coq?
Isabelle has the frontend Isar which mimics some features of the Mizar system.
I'm curious if Coq has anything similar, i.e. an alternative to tactic scripts that's designed to be readable or similar ...
- 3,105
5
votes
2
answers
189
views
Are there any provers based on a paraconsistent logic?
This question talks about controlled usage of a self-containing top type satisfying $\text{type}\! : \text{type}$.
I'm wondering if there are any provers that deliberately give $\text{type}\!: \text{...
- 3,105
13
votes
2
answers
210
views
verifying combinatorial constructions - choice of a proof assistant
The choice of the proof assistant to use for formalisation depends on the area quite a bit; e.g. they say that algebraic topology comes easy in HoTT assistants.
What would be the most natural choices ...
- 480
15
votes
4
answers
505
views
What games are there?
A game is a fun interactive tutorial/puzzle/challenge that provides the user with a DAG of definitions, theorem statements, examples, etc. and asks the user to prove all the theorems in this DAG. For ...
15
votes
1
answer
288
views
Are there automated theorem provers for constructive logics? What strategy do they use?
I know of a handful of automated theorem provers for classical first-order logic such as Vampire (source code).
Internally, I think most of these provers work by translating premises and the negated ...
- 3,105
10
votes
2
answers
242
views
Are there any non-English based proof assistants?
There is a Wikipedia article about non-English based programming languages, but what about for proof assistants?
I recall seeing one which was a translation of Lean tactics to French, by Patrick ...
- 410
11
votes
2
answers
122
views
Proof assistants or libraries in proof assistants for working with model theory
The basics of model theory contain, as far as I understand, some theorems that are difficult to prove in their full generality.
For example, the compactness theorem in FOL for languages with ...
- 3,105
14
votes
4
answers
288
views
Proof Assistants with support for creating executable software artifacts
I am looking for proof assistants with which I can write sound proofs about my functions and values, as well as compile actions of type IO () into executable code. ...
- 1,502
16
votes
2
answers
204
views
Are there any proof assistants or theorem provers based on the method of analytic tableaux?
Are there any proof assistants or theorem provers based on the method of analytic tableaux?
A closed tableau makes the branching structure of a proof using case analysis very obvious.
I like tableau ...
- 3,105
15
votes
4
answers
413
views
Are there any well-known Internal DSL Proof Assistants?
Proof assistants like Coq have their own extensible syntax that's rather different from a general purpose language.
I'm curious whether there are any well-known proof assistants that are implemented ...
- 3,105