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.

Filter by
Sorted by
Tagged with
11 votes
0 answers
153 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 ,...
user avatar
  • 2,246
5 votes
0 answers
69 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 + ...
user avatar
  • 1,090
31 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 ...
user avatar
9 votes
1 answer
155 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 ...
user avatar
  • 489
3 votes
1 answer
91 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 (...
user avatar
  • 2,467
13 votes
2 answers
173 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 ...
user avatar
  • 2,467
5 votes
1 answer
99 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 ...
user avatar
  • 2,467
10 votes
1 answer
157 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 ...
user avatar
  • 2,467
5 votes
2 answers
136 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{...
user avatar
  • 2,467
11 votes
2 answers
127 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 ...
user avatar
12 votes
4 answers
260 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 ...
14 votes
1 answer
179 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 ...
user avatar
  • 2,467
11 votes
2 answers
204 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 ...
user avatar
11 votes
2 answers
98 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 ...
user avatar
  • 2,467
14 votes
4 answers
163 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. ...
user avatar
15 votes
2 answers
157 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 ...
user avatar
  • 2,467
16 votes
4 answers
287 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 ...
user avatar
  • 2,467