# Tag Info

19

The purpose of the proof checker is to minimise the trusted computing base. By having a proof checker, neither the compiler nor the theorem prover need to be correct. The paper makes this point on Page 3: Neither the compiler nor the prover need to be correct in order to be guaranteed to detect incorrect compiler output. This is a significant advantage ...

14

In general, what we usually call the logical relations argument isn't really linked to impredicativity: the main idea is simply to interpret terms in some abstract algebra $\cal A$, and to represent types as a ($n$-ary) relation $R \subseteq \cal A^n$. This works perfectly fine for all kinds of type theories, including dependently typed theories, see e.g. ...

12

Another famous example is Hales' proof of Kepler's conjecture which had a very large computer aided component. From Wikipedia: In August 1998 Hales announced that the proof was complete. At that stage it consisted of 250 pages of notes and 3 gigabytes of computer programs, data and results.

11

Assuming that the complexity of the provability problem would satisfy you, the landscape of complexities of substructural logics with and without contraction is somewhat complex. I'll try to survey here what is known for propositional linear logic and propositional logic. The short answer is that contraction sometimes helps (e.g. LLC is decidable, while LL ...

10

I don't think your question is particularly well posed. It mostly asks for opinions. Here are mine: Yes. I do not know what you mean, but the answer is probably "there is more MLTT theory to be done, although we do know a lot". You cannot do all of homotopy type theory in Coq and Agda. This is an active area of research.

10

This is more of a meta answer in that it is a list of lists. The papers of Doron Zeilberger. He is a mathematician and his computer is listed at the coauthor Shalosh B. Ekhad on all papers where the computer played a part in deriving the results. Work of Georges Gonthier. He engineered a machine-checked proof of the four colour theorem and has been recently ...

9

Short answer. Formal reasoning about binding and $\alpha$-conversion with nominal approaches is closer to intuitive reasoning than alternative approaches. Longer answer. Binders arise everywhere in mathematics and computer science. Dealing with binders has historically been done in a handwaving way (e.g. assuming Barendregt's variable convention). This ...

9

Here's an amusing approach by Brock-Nannestad and Schürmann: Truthful Monadic Abstractions The idea is to try to translate first-order sentences into monadic first-order logic, by "forgetting" some of the arguments. Certainly the translation isn't complete: there are some consistent sentences which become inconsistent after translation. However, monadic ...

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 ...

8

Principia Mathematica was a largely response to the various paradoxes discovered in mathematical logic at the turn of the 20th century. However the work itself, which has often been obliquely praised as an 'unreadable masterpiece' is somewhat clumsy and more modern foundations have been crafted. To describe most of mathematics, you have several choices: ...

8

Several points: As far as I know, Principia Mathematica uses essentially a formalization of set theory using a typed first order logic. It would therefore be tempting to use a first-order automated theorem prover like Prover 9 or possibly ACL2 to formalize your statements. However, I am seeing several set-theoretic constructions (like $\in$, $\cap, \subset$)...

6

There are numerous ways of formalizing set theory: ZFC uses first-order logic and a primitive relation $\in$ NBG uses first-order logic, a primitive relation $\in$, and a primitive predicate $S$ Church's type theory is multi-sorted and uses infintely many types Type theory is similar to set theory, but not quite the same Second-order arithmetic, through ...

6

One example is the proof of non-existence of a projective plane of order 10. See The Search for a Finite Projective Plane of Order 10 and The Non-existence of Finite Projective Planes of Order 10.

6

Short answer: no. Long answer: No, because the synthesis problem is in general undecidable once you allow for a modest amount of expressive power in the assertions (pre- and post-conditions). The specification for your synthesizer $S$ would look something like this. Its type would be $S:\mathit{Assn}^2\rightarrow\mathit{Prog}$, that is, given two ...

6

Briefly, every theorem stated in first-order logic has a first-order proof. In his book "An Introduction to Mathematical Logic and Type Theory", Peter B. Andrews develops both first-order logic and a system of higher-order logic Q0, which is generally considered to be the theory basis of modern higher-order provers. (See the introduction to the HOL logic ...

6

Pavlovic et al. view Turing machines over a binary alphabet as coalgebras for the functor $\lambda X. \, 2 \times \mathcal{P}_{\mathrm{fin}}(X \times 2 \times \{\lhd,\rhd\})^2$. The symbols $\lhd$ and $\rhd$ represent thereby the tape moves. Bart Jacobs has presented in "Coalgebraic walks, in quantum and Turing computation" an approach by using a monad. He ...

4

Yes, equality reflection and $\eta$-rule for functions together imply function extensionality. Recall that equality reflection is the rule $$\frac{\vdash p : \mathsf{Id}_A(a,b)}{\vdash a \equiv b : A}$$ Suppose $A$ is a type, $x : A \vdash B(x)$ is a type over $A$, and $f, g : \prod_{x : A} B(x)$. We claim that function extensionality $$\textstyle (\prod_{x:... 3 Heuristically: Yes, I suspect this probably works, if the system of equations is committed to in advance (well before mining works), and if the system of equations is small enough. You'll need the random oracle assumption, ERH, and maybe other heuristic assumptions. In particular, Theorem 5 of their paper upper-bounds the number of prime numbers p such ... 3 I found signs that such a decision procedure was implemented in the (general purpose) theorem prover SPASS. In particular see the thesis of Ann-Christin Knoll, On Resolution Decision Procedures for the Monadic Fragment and Guarded Negation Fragment. This implements what you want, though I couldn't find the implementation online. 3 Here is a recent one: http://link.springer.com/chapter/10.1007%2F978-3-319-09284-3_17 You can get the fulltext here: http://arxiv.org/abs/1402.2184 It uses some state-of-the-art SAT solvers (see http://fmv.jku.at/lingeling/) to solve a member of a family of problems called "Erdős Discrepancy Conjecture". They encoded the problem as SAT instances and the SAT ... 2 See this paper: On Godel’s Theorems on Lengths of Proofs II: Lower Bounds for Recognizing k Symbol Provability by Samuel R. Buss, 1995. This paper discusses a claim made by Godel in a letter to von Neumann which is closely related to the P versus NP problem. Godel’s claim is that k-symbol provability in first-order logic can not be decided in o(... 2 I guess the resource you are looking for is Adam Chlipala's Certified Programming with Dependent Types in which he builds up powerful tactics. 2 Your translation goes into Presburger arithmetic, which is decidable. You could take your translated formula, do quantifier elimination on it, and then hand it over to a proof-producing SMT solver. Since pretty much all SMT solvers are (fancy extensions of) DPLL, I would guess you can turn those proofs into resolution proofs without too much difficulty. ... 2 In a 1993 LICS paper, Bachmair, Ganzinger and Waldmann showed that set constraints are equivalent to monadic FOL, in Set Constraints are the Monadic Class. If memory serves, set constraints are equivalent to regular tree grammars, so most of the algorithms developed there should portable to monadic FOL as well. I don't know the area that well, but set ... 2 In contradiction with Gurkenglas' answer, there actually is a community of scientists who work on proving non-termination of programs in various language and formalisms. An obvious approach would be to check for looping non-termination: for a given program w, pick an input x and check to see if the same state is reached twice with the same data. Non-... 2 To add to the answer in the comments, it might help to first ask what the difference is between a model checker and an automated theorem prover for propositional logic. Given the statement$$p \wedge q we can ask whether it is true in the model $\{p=\top,q=\bot\}$ (model checking) or we can ask whether it is true in all models (theorem proving). We can ...

1

Can this formulation be trivially extended for each constructor by simply adding a Ci for an additional inductive case? Yes. I can't provide a general nor a technical answer, but a while ago I was trying to solve a similar problem and someone helped me by providing a visualization of the general procedure. This helped me a lot, so I'll reproduce it here in ...

1

Since the Halting problem is undecidable, whatever approach I use to answer the question must eventually be unhelpful in the real world. There's a sequence of sets of programs such that each set is contained in the next, their union contains all programs, and for the nth set there's a program of length in O(n) that decides haltingness in it. Proof: The nth ...

1

Computability theory in general has been somewhat under-formalized. The short answer is that most theorems of computability theory do not pass one of the three tests for formalization: A proof that is computationally intensive or untrusted for some reason (long, complex). A result that is relevant to undergraduate mathematics. A result that is useful to ...

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