22

As for question 2, there are at least two examples of $NP$-completeness proofs that involve computer-assistant. Erickson and Ruskey provided a computer-aided proof that Domino Tatami Covering is NP-complete. They gave a polynomial time reduction from planar 3-SAT to tatami domino covering. A SAT-solver (Minisat) was used to automate gadgets discovery in ...


21

That's a good question! It asks what we expect from types in a typed language. First note that we can type any programing language with the unitype: just pick a letter, say U, and say that every program has type U. This isn't terribly useful, but it makes a point. There are many ways to understand types, but from a programmer's point of view the following ...


20

Here is a small, incomplete, and inconsistent formalization of HoTT in Idris. It shows that you can derive a contradiction in Idris just by postulating univalence. There are two barriers to formalizing HoTT in Idris at the moment. Barrier 1: Idris has heterogeneous equality and heterogeneous equality rewriting. From the HoTT perspective this means we have ...


17

LCF is indeed the grand-father of all these system: Coq, Isabelle, HOLs, including the ML programming language (which we see today as OCaml, SML, also F#). Yes, I am including Coq as a member of the greater LCF family. Compared to the US-American proof assistants (notably ACL2), or the totally unrelated Mizar, Coq is culturally quite close to Isabelle and ...


15

A general rule of thumb is that the more abstract/exotic the mathematics you want to mechanise, the easier it gets. Conversely, the more concrete/familiar the mathematics is, the harder it will be. So (for instance) rare animals like predicative point-free topology are vastly easier to mechanize than ordinary metric topology. This might initially seem a ...


15

In this paper, I showed that if for some $k\geq 3$ there is a graph with maximum degree $k$ and chromatic edge strength strictly greater than $k$, then it is $\Theta_2^p$-complete to decide if chromatic edge strength is at most $k$. Such graphs were known for $k>3$ and I did a computer search to find a suitable $12$-vertex graph for $k=3$. The complexity ...


14

It is important to understand that there is a spectrum from deep to shallow. You model the parts of your language deeply that should somehow participate in some inductive argument about the construction of it, the remainder is better left in the shallow see of direct semantics of the substrate of the logic. For example, when you want to reason about Hoare ...


13

You are probably thinking of Gower's work with Ganesalingam, based on the latter's MSc dissertation (1). Gowers blogged about this in (2) and other places, and they've written a paper on the subject (3). There is other work in that direction, for example from the interactive proof assistant community. The most well-known example here might be the Isar ...


13

From the comment above: I used the Choco Java library for Constraint programming to check the correct behaviour of the gadgets used to prove the NP-completeness of the following puzzles: Binary Puzzle, Tents, Rolling cube puzzle without free cells, Net. I didn't have the time to publish them, yet, but the draft papers are available on my blog. The ...


11

In the following paper my colleague Uli Schöpp presents a formal verification (in Coq) of a nontrivial result by Cook and Rackoff on the computational power of graph automata. https://scholar.google.at/scholar?oi=bibs&cluster=4944920843669159892&btnI=1&hl=de (Schöpp, U. (2008). A formalised lower bound on undirected graph reachability. In Logic ...


11

I did this very thing — computer-assisted NP-completeness proof — in my bachelor thesis! The bad part - it's in Russian and wasn't translated to English. http://is.ifmo.ru/diploma-theses/_dvorkin_bachelor.pdf I worked with logical gates in 2D problems. The plan is: Manually design what a "wire" looks like in your problem. Use very smart and optimized ...


11

To my knowledge, no machine checked proof of a complex mathematical development has ever been retracted. As Andrej points out though, it occasionally happens that soundness-breaking bugs do crop up in these systems (though usually not silently, as Andrej suggests), and the fix to that bug involves some changes to existing proofs, or, more likely, of the ...


10

(Turning a comment into an answer, and expanding on it) From talking to someone who worked on this: no. He invented all sorts of clever refinements to many proofs, and restructured many theory developments, both of which are extremely valuable, but the algorithms involved are not interesting -- in fact, many of them are dumb brute force, the very opposite ...


10

The question can be interpreted in two ways: Whether the implementation does implement a given typing system $T$? Whether the typing system $T$ does prevent the errors you think it should? The former is really a question in program verification and has little to do with typing. Just needs showing that your implementation meets its specification, see Andrej'...


8

I'm not sure this answers your question, but the first (?) paper on the subject of tactics appears to have been Milner's The Use of Machines to Assist in Rigorous Proof.


8

Obviously there is an operational semantics of Ltac by Jedynak et al.


8

For Buchberger, it depends what you want it for, but generally speaking the answer is no. First, as pointed out on the Wikipedia article, the complexity upper bound given by Tarski-Seidenberg is horrendous, whereas Buchberger's algorithm is exponential space, which is optimal (since ideal membership is EXPSPACE-complete). Second, Tarski-Seidenberg is for ...


7

As usual, (a) the high-level conceptual approach is basically the same as it is on paper, but (b) mechanization makes new things reasonable to attempt. The way you do things is to define a cost semantics for a programming language, where you assign a cost for each of the operations in the language. Next, you define a machine model, with its own cost ...


7

I am not aware that J or K exists for heterogeneous equality. It does not need an elimination principle, because it can be simply defined as a sigma type: coe : ∀{i}{A B : Set i} → A ≡ B → A → B HEq : ∀ {i}{A B : Set i} → A → B → Set _ HEq {_}{A} {B} x y = Σ (A ≡ B) λ p → coe p x ≡ y To do anything with HEq, it is enough to consider J and K for ...


6

One very prominent example is of course Gonthiers Coq formalization of the 4 color theorem in Coq which uses a lot of combinatorics. My colleague Uli Schöpp used the ssreflect library developed by Gonthier for this purpose in order to verify (and slightly extend) also in Coq a result by Cook and Rackoff on graph automata. https://scholar.google.at/scholar?...


6

It is true that Agda currently has a much shakier foundation than say Coq or Lean. It does have an internal term syntax that could be seen as a core language (https://github.com/agda/agda/blob/master/src/full/Agda/Syntax/Internal.hs). It even has an independent typechecker for internal syntax (https://github.com/agda/agda/blob/master/src/full/Agda/...


5

There are a few different things you could mean by "prove that my typechecker works". Which, I suppose, is part of what your question is asking ;) One half of this question is proving that your type theory is good enough to prove whatever properties about the language. Andrej's answer tackles this area very well imo. The other half of the question is —...


5

He doesn't cite any references for it and Google doesn't return any results so I don't think he is really quoting from anywhere. The idea that a proof is a "construction" (a term in intuitionistic/constructive mathematics with a very close meaning to what we call algorithm nowadays) goes back to at least Luitzen Egbertus Jan Brouwer. Note that Brouwer ...


5

Compactness for FOL was done in HOL by John Harrison, and reported at TPHOLs 1998. See Formalizing basic first order model theory.


5

The obvious resource for planar graphs in Coq would be the (modern port of) the four color theorem in Coq/SSReflect, by Georges Gonthier (and others) which obviously does need to define planar graphs. It's not immediately obvious to me how planar graphs are characterized, though the relevant file is here and it seems to involve a combination of Euler ...


5

DEDUCT_ANTISYM_RULE only applies to propositions, while REFL applies to all terms of all types. Your suggestion only shows that every propositions is equal (equivalent) to itself, but it could not be used to show that ever number equals itself.


4

The current Software Foundations book does explain all this later on: https://softwarefoundations.cis.upenn.edu/lf-current/ProofObjects.html So if you're following the book, just read on :)


4

For verified complexity analysis in other theorem proving systems, see e.g. Tobias Nipkow's paper on this subject using the Isabelle theorem prover ("Amortised Complexity Verified" at ITP 2015) which presented a framework for deriving amortised cost bounds of functional data structures and applied it to a number of well known data structures. The code is ...


4

As Neel answered, you can (theoretically) prove anything in a proof assistant that you can prove on paper, including idealized run-times or resource usage for a program modeled using a deep embedding (see Shallow versus Deep Embeddings). How closely your idealized representation of the run-time corresponds to the actual run-time (in milliseconds, say) of a ...


4

I just wanted to make some additional comments not already covered by Cody's nice answer, and also address question (2). First, Gonthier goes into detail about the representation of planar maps used for the formalization of 4CT in his technical report A computer-checked proof of the Four Colour Theorem. This representation is based on the classical (and ...


Only top voted, non community-wiki answers of a minimum length are eligible