Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

A proof assistant is an application program that helps humans construct machine-checked proofs.

5
votes
0answers
143 views

Is Agda sound as a proof system? [closed]

I've asked the same question on CSSE but with no luck (https://cs.stackexchange.com/questions/89611/is-agda-sound-as-a-proof-system). Therefore I ask it again here in cstheory and hope that more ...
18
votes
1answer
464 views

Formally Verified Complexity Theory

Is there any ongoing project to formally verify the theorems and proofs of complexity theory using a proof assistant like Coq? Are there any boundaries to doing this?
0
votes
1answer
142 views

Is Buchberger's algorithm or Wu's method valuable theoretically when we have the Tarski–Seidenberg theorem?

Is Buchberger's algorithm or Wu's method valuable theoretically when we have the Tarski–Seidenberg theorem? In other words, could the Tarski–Seidenberg theorem subsume Buchberger's algorithm and Wu's ...
5
votes
1answer
101 views

Using ϵ -unification and Knuth-Bendix completion to automatically proof theorems about groups

This is a follow-up question. In my previous question, I presented Welder proof assistant and I stated that I want to automate proofs about basic field theory. The only answer to this post states that ...
6
votes
3answers
195 views

Proving running time upper bounds for algorithms in dependent type theory

Proof assistants are a valuable tool for verifying the correctness of proofs of mathematical theorems. When dealing with proofs of correctness of algorithms, one is not only interested on showing ...
8
votes
3answers
654 views

What should a proof of correctness for a typechecker actually be proving?

I've been programming for several years, but am very unfamiliar with theoretical CS. I've recently been trying to study programming languages, and as part of that, type checking and inference. My ...
14
votes
2answers
365 views

Proof assistant usage in complexity theory research?

Considering the topics covered at a conference like STOC, are any algorithm or complexity researchers actively using COQ or Isabelle? If so, how are they using it in their research? I assume most ...
9
votes
0answers
168 views

Is there a known automatic proof of the independence of the continuum hypothesis?

In 2002, L.C. Paulson gave a mechanized proof of the consistency of the axiom of choice by formalizing $V=L$ and its consistency. We could ask whether there is a formalized proof of the independence ...
30
votes
1answer
924 views

Has a proof checker bug ever invalidated a major proof?

Most (all?) proof assistants have soundness bugs fixed on occasion. However, from those I've seen these bugs are usually difficult to come across unintentionally, and results proved before the bug is ...
4
votes
1answer
233 views

Where is the quote “Informal proofs are algorithms, formal proofs are code” from?

Does anyone know the origin of the quote, Informal proofs are algorithms; formal proofs are code. Its made in Benjamin C. Pierce et al.'s Software Foundations.
7
votes
1answer
163 views

Is there a theory of overloading types?

There is a sound theory of overloading operators and functions realized by type classes in Haskell, and to rougher extent by traits in Rust, etc. In mathematics however, there are many situations ...
2
votes
1answer
79 views

Proof software for Primitive Recursive Arithmetic

Primitive Recursive Arithmetic is a critical foundational system in mathematics at large, and all the more so in areas studying constructive reasoning and/or computability such as Theoretical Computer ...
8
votes
1answer
573 views

Humanifying computer-generated or computer assisted proofs

I remember reading a blog post displaying two versions of the same proof, one written by a human and the other by a machine, and asked the readers to tell which is which. Trying to google the post ...
7
votes
1answer
168 views

Formalized priority argument

A priority argument, an important proof technique in recursion theory, was introduced by Friedberg and Muchnik, to solve Post's Problem, i.e., the existence of two r.e. sets that do not Turing reduce ...
23
votes
5answers
791 views

Curious about computer-assisted NP-completeness proofs

In the paper "THE COMPLEXITY OF SATISFIABILITY PROBLEMS" by Thomas J. Schaefer, the author has mentioned that ...
16
votes
1answer
1k views

Formalizing Homotopy Type theory in Idris

Looking at the homotopy type theory blog one can easily find a lot of library formalizing most of Homotopy Type Theory in Agda and Coq. Is there anyone aware if there is any similar attempt to ...
1
vote
0answers
113 views

looking for notable applications of ASP (Answer Set Programming) in TCS

a recent difficult question of interest to the group[1] by GB has possibly led to verification of a new graph property by dspyz, by use of Answer Set Programming/ASP. via sophisticated logic ...
26
votes
1answer
505 views

Interesting algorithms in the formalization of the Feit-Thompson theorem?

It looks like George Gonthier and his collaborators have finished formalizing the Odd Order Theorem. In his earlier work on the Four Color Theorem, Gonthier invented a bunch of new algorithms (...
-2
votes
1answer
527 views

Coq definition with unusual syntax (Definition … Defined.)

While examining the package Library ZFC.Sets, I found the following definition: ...
14
votes
0answers
286 views

Proof assistant formalizations of Finite Model Theory

I'm wondering if anyone knows of a formalization (even limited) of any part of finite model theory in any of the major proof assistants. (I'm most familiar with Coq, but Isabelle, Agda, etc. would ...
16
votes
3answers
1k views

What is the role of predicativity in inductive definitions in type theory?

We often want to define an object $A \in U$ according to some inference rules. Those rules denote a generating function $F$ which, when it is monotonic, yields a least fixed point $\mu F$. We take $A :...
39
votes
4answers
3k views

How would I go about learning the underlying theory of the Coq proof assistant?

I'm going over the course notes at CIS 500: Software Foundations and the exercises are a lot of fun. I'm only at the third exercise set but I would like to know more about what's happening when I use ...
42
votes
3answers
3k views

How do 'tactics' work in proof assistants?

Question: How do 'tactics' work in proof assistants? They seem to be ways of specifying how to rewrite a term into an equivalent term (for some definition of 'equivalent'). Presumably there are formal ...
17
votes
1answer
2k views

Prove proof irrelevance in Coq?

Is there a way to prove the following theorem in Coq? Theorem bool_pirrel : forall (b : bool) (p1 p2 : b = true), p1 = p2. EDIT: An attempt to give a brief ...
12
votes
6answers
2k views

Proof assistant for writing mathematics

I'd like to write mathematical proofs using some proof assistant. Everything will be written using first order logic (with equality) and natural deduction. The background is set theory (ZF). For ...
28
votes
1answer
806 views

Is there a reasonable automated proof system for TCS theorems?

Suppose I wanted to formalize Turing's proof regarding the halting problem so that a machine could check it. Some of the well-known automated theorem proving systems include Mizar, Coq, and HOL4. I ...
13
votes
1answer
4k views

How to define a function inductively on two arguments in Coq?

How can I convince Coq that the recursive function given below terminates? The function takes two inductive arguments. Intuitively, the recursion terminates because either argument is decomposed. ...
45
votes
3answers
4k views

Shallow versus Deep Embeddings

When encoding a logic into a proof assistant such as Coq or Isabelle, a choice needs to be made between using a shallow and a deep embedding. In a shallow embedding logical formulas are written ...
15
votes
2answers
933 views

Eliminating cofix in Coq proof

While trying to prove some basic properties using coinductive types in Coq, I keep running into the following problem and I cannot get around it. I've distilled the problem into a simple Coq script as ...