sources - CAVE-PNP/cave-pnp GitHub Wiki

Sources and Literature

P vs NP

Related Topics

Isabelle/HOL

Formalizations

This section lists results and resources relevant to or close to the topic of this project.

Quick Reference

Tutorials

Note: Markus Wenzel seems to be using the name Makarius Wenzel since ~2007 as can be seen in the list of his publications on his page on the website of the Technische Universität München.

Many of the sources provided here are taken from the Documentation page on the Isabelle homepage, and the homepage as well as the page Course Material of the community wiki.

  • Getting Started with Isabelle/jEdit in 2018
    • very short introduction of how to set up and work with Isabelle/jEdit
  • Thomas Genet: A Short Isabelle/HOL Tutorial for the Functional Programmer
    • very short "depth-first" look into Isabelle
    • many concepts are explained on-the-fly
    • requires an understanding of functional programming
  • concrete_semantics.pdf: Tobias Nipkow and Gerwin Klein: Concrete Semantics
  • tutorial.pdf: Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel: Isabelle/Hol: A Proof Assistant for Higher-Order Logic. Springer 2020.
    • this is an updated version of the book of the same name (published by Springer, 2002) that is available in the AAU library (see here)
    • there was a lecture based on this book with materials available here
  • jedit.pdf: Makarius Wenzel: Isabelle/jEdit. 2020.
    • more in-depth overview of the features of Isabelle/jEdit
  • Christian Urban et al.: The Isabelle Cookbook
    • Tutorial about programming on the ML level of Isabelle for users who are already familiar with Isabelle
  • Course: Thomas Genet: ACF: Software Formal Analysis and Design, 6 lectures and 10 lab sessions, WS20
    • full course materials are publicly available (including lectures in french)

    • Disclaimer: this is a course on formal software design and not on proof design. Students are given a limited set of proof tactics that is enough to prove properties defined during the lab sessions. However, resulting proofs can be long and cumbersome. As a result, it is accepted that properties are not proven but only checked using Isabelle/HOL powerful counter-example finders.

  • Course: Clemens Ballarin and Gerwin Klein: Introduction to the Isabelle Proof Assistant
    • one-day introduction to Isabelle
    • materials (slides, exercises) available
    • starts by formally introducing syntax, explaining inner workings -> not recommended for starters
  • Course: Holger Gast: Interactive Software Verification
    • materials (slides, exercises & solutions) available online
    • introduction and working with Isabelle
    • focus on software verification (small C-like language)

Resources

Coq

Formalizations

  • The Coq Package Index
    • proof repository of Coq
    • part of the OCaml Package Manager (OPAM)
    • counterpart of the Isabelle AFP
    • see also the Package Ecosystem section here
  • EasyCrypt (GitHub repo)

    EasyCrypt is a toolset for reasoning about relational properties of probabilistic computations with adversarial code. Its main application is the construction and verification of game-based cryptographic proofs.

    • CertiCrypt (GitHub repo)

      CertiCrypt is a toolset that assists the construction and verification of cryptographic proofs; it supports common patterns of reasoning in cryptography, and has been used successfully to prove the security of many constructions [...]

  • Forster et al.: A Coq Library of Undecidable Problems
  • Yannick Forster, Fabian Kunze, and Maximilian Wuttke: Verified Programming of Turing Machines in Coq. ACM 2020.
    • TMs with space and time complexity, including the universal TM
    • maintained as part of the Coq Library of Undecidable Problems (see above)
    • extends Wuttke's Bachelor's thesis of the same name
      • this is not confirmed, but definitions and content match
      • the universal TM and space complexity are not parts of the Bachelor's thesis
      • states the heavy use of dependent types, making this particular formalization of TMs rather unpleasant for proof assistants that do not support them (like Isabelle/HOL)
    • based on the Matita implementation by Asperti and Ricciotti (see below)
    • see the external Appendix for definitions that are left out in the paper
      • see also the Bachelor's thesis
    • multi-tape TMs
      • universal TM simulates single tape TM
      • compiler from multi-tape to single-tape
      • three abstraction layers from standard TM to ~register machine/pseudo code
    • custom tactics for reasoning about TMs
      • the authors state (about a certain kind of statement) that "using them by hand is almost impossible"
      • the tactic (TMSimp) simplifies goals by "destruction of complex assumptions" (i.e. conjunctions, existentials) and "exhaustively rewriting with all available equations between tapes"
  • Lennard Gäher and Fabian Kunze: Mechanising Complexity Theory: The Cook-Levin Theorem in Coq

Tutorials

The documentation section on the Coq homepage gives an overview of resources.

Resources

Other Proof Assistants

General

Matita

  • Homepage: http://matita.cs.unibo.it
  • Developed at: Computer Science Department of the University of Bologna
  • Latest release (as of 2021-04): 0.99.3 (2016-05-18)
  • sources: self-hosted git (active 2021-03)

Based on the Calculus of (Co)Inductive Constructions, like Coq.

Publications

Formalizations

  • Andrea Asperti, and Wilmer Ricciotti: Formalizing Turing Machines. Springer 2012.
    • Follow-up: A Formalization of Multi-tape Turing Machines. Springer 2015.
    • comparison to tm.pdf
      • Asperti and Ricciotti cite the complexity of the machines in tm.pdf, in contrast to the composition of very small machines
      • "In particular, the fact that the universal machine operates with a different alphabet with respect to the machines it simulates is annoying."

General Quotes

  • Manuel Herold, realizing that the solution is trivial, mere seconds after asking whether $P$ is $NP$:

    $P = NP$ genau dann, wenn $P = 0$ oder $N = 1$.

    -- Manuel Herold, Personal communications (Max), 2021-01-08.

  • The quote in the section on Relativization (Basic Idea)

  • From the preface of Concrete Semantics (cited above), on theorem proving assistants:

    • The beauty is that this includes checking the logical correctness of all proof text. No more 'proofs' that look more like LSD trips than coherent chains of logical arguments.

    • But only recently have proof assistants become mature enough for inflicting them on students without causing the students too much pain.

  • A "snarky remark" on possible reasons for why there is no sledgehammer for Coq (from Lawrence Paulson: Sledgehammer: some history, some tips)

    • One of the reasons I prefer higher-order logic to dependent type theories — apart from simple semantics, equality that works and no need to put everything in the kernel — is that dependent types seem to make automation much more difficult. Groups with access to institutional support and steady, ample resources still don’t seem to have duplicated what had been built at Cambridge on a single £250K grant. And please don’t say “dependent type checking makes other automation unnecessary”. Yes, I keep hearing this.

  • From Scott Aaronson: Death of proof greatly exaggerated (answer to John Horgan: The Death of Proof)

    • In many areas of math (including my own, theoretical computer science), proofs have continued to get longer and harder for any one person to absorb. This has led some to advocate a split approach, wherein human mathematicians would talk to each other only about the handwavy intuitions and high-level concepts, while the tedious verification of details would be left to computers. So far, though, the huge investment of time needed to write proofs in machine-checkable format — for almost no return in new insight — has prevented this approach’s wide adoption.

    • see also the wider discussion on whether automated proof assistants are the end of formal mathematics, for instance Okay, Maybe Proofs Aren't Dying After All by John Horgan

Additional reading

Comparison of proof assistants

Inspecting solver steps

Unsorted Resources

These are everything from blog posts to StackExchange questions that may be of use at some point.

Missing/Hard-to-Find Resources

  • Hartmanis1985. J Hartmanis: Solvable problems with conflicting relativizations
    • paper is frequently quoted in works on relativization but nowhere to be found
    • given an oracle $A$ such that $P^A = NP^A$, one could construct an oracle $B$ such that $P^{A,B} ≠ NP^{A,B}$, which would mean that $P^A = NP^A$ does not relativize. (see [Hartmanis1985] as cited in Allender1990)
    • some believe that "[statements that do not relativize] may fall outside the axioms of set theory" (see [Hartmanis1985] as quoted in relative.pdf)