# Tag Info

Accepted

### Do theorem provers demonstrate their own correctness?

I recommend reading Pollack's How to believe a machine-checked proof. It explains how proof assistants are designed to minimize the amount of critical code. There are many levels of formal ...
• 30.9k
Accepted

### What kind of math problems can be solved by automated theorem provers?

Most of your statements are elementary algebra, so these can be proved automatically by a computer algebra system (CAS), such as Maple or Mathematica. (In case you're interested in the mathematics ...
• 8,303
Accepted

### What is the complexity of theorem proving?

In general, the complexity of theorem proving in a particular logical system (such as ZFC) is recursively enumerable (RE), and is complete for this class -- that is, equally as hard as solving the ...
• 7,088
Accepted

### Monadic Second Order Logic for Dummies

What is second order logic in contrast to first order logic? What is monadic vs non monadic logic? Monadic second-order logic is first-order logic plus quantification over sets. So, as well as ...
• 81.9k

### Do theorem provers demonstrate their own correctness?

What you need is the idea of "the trusted core". Quoting "A verified runtime for a verified theorem prover": In many theorem provers, the trusted core—the code that must be right to ensure ...
• 3,192
Accepted

### What was the major breakthrough between Hoare-Floyd logic and Scott–Strachey semantics?

I don't know why people didn't develop Hoare logics for lambda-calculi earlier. The first work to get this right was Honda et al's A Compositional Program Logic for Polymorphic Higher-Order Functions ...
• 8,328
Accepted

### Framework or tools to generate theorem prover/solver/reasoner for new logic

There are many related ways you can mechanise your logic. Deep embedding into one of the well-developed provers such as Isabelle/HOL, Coq or Agda. This is (almost) always possible, but makes using ...
• 8,328
Accepted

### How did 'Isabelle' (the theorem prover) get its name?

A little google-fu (and my own memory) tells me it was apparently named by Larry Paulson after Gerard Huet's daughter. Gerard Huet happens to be one of the people behind the less poetically named Coq ...
• 8,233

### Why do presenttations of proof systems in logic and automated reasoning not include the algorithm that finds proofs?

To simplify a bit, a system of inference rules generally defines a set of sequents, which are simply pairs of a list (or set) of propositions $\Gamma$ and a proposition $\phi$ written  \Gamma \...
• 8,233

### How to get an element from an existential proposition in Type theory proof assistant (Lean prover)

The existential form of the axioms of set theory is convenient for the meta-theoretic explorations of set theory, such as forcing etc., where it is important to have a minimal language to worry about (...
• 30.9k

### Do theorem provers demonstrate their own correctness?

While this may trend close to self-advertisement, this is essentially the topic of my recent paper Metamath Zero: The Cartesian Theorem Prover (video), and the analogy with bootstrapping compilers is ...

### What is the difference between superposition and paramodulation?

This is late for you, but probably might be of help to others. I myself had asked this question and I wrote the summary of my findings to the acl2-help mailing list on 8 and 9 September 2013: https://...
• 61
Accepted

### Building non-classical logics in Agda & Coq

You can define many non-classical logics in Coq (and I assume Agda too), even if they are incompatible with the logic of your proof assistant, but you need to define the concept of inference yourself. ...
• 176
Accepted

### Why Church-encoded types aren't sufficient to express inductive proofs?

How would you prove inside the pure CoC that the induction principle holds of the Church numerals? See Thomas Streicher's, Independence of the induction principle and the axiom of choice in the pure ...
• 8,328
Accepted

### Is it possible to build short proofs of arbitrary folds over a huge list?

Yes, there is a generalization of the construction you mentioned. However, it's utility depends on the function F. The guarantees you get are meaningful only if <...
• 161k
Accepted

### Theorem Prover for complexity theoretic reductions

This is certainly possible, and the language of higher order functions makes this quite nice. If you're doing a Turing/Cook reduction, you can basically just write a function that takes an oracle as a ...
• 29.8k

My goal is to be able to judge what parts of formal verification I could apply to my job as a software/network engineer. If you plan to use formal verification as black boxes, then I would suggest ...
• 532

### Do theorem provers demonstrate their own correctness?

In case you are not aware, there is a possibility that a theorem prover is implemented 100% correctly and run on a faultless machine and proves itself arithmetically inconsistent, even though it is ...
• 727
Accepted

### Finding libraries of formalized mathematics

Metamath has a HUGE chapter-organized archive of formal theorems: http://us.metamath.org/mpeuni/mmtheorems.html Besides that, Freek Wiedijk's QED manifesto is always a good starter for future ...
• 2,275
Accepted

### Has the concept of using a hand checked simple theorem prover to validate more complex theorem provers been explored before?

Not that I know of. A more typical architecture is to decompose the theorem prover into a prover plus a proof checker. Then only the proof checker needs to be validated. If proofs are expressed in ...
• 161k

### Why do TPTP Performance plots look like this?

I can speculate/hypothesize. Each solver has many heuristics and proof tactics. Imagine that corresponding to each heuristic is a class of instances that are easy to solve if you use that heuristic, ...
• 161k
Accepted

### Procedure to automatically solve field theorems in a SMT solver

All of the theorems you want to prove (except uniqueAddNeutral) are of the form $\forall x . \phi(x)$ where $\phi(x)$ is quantifier-free. Herbrandization is typically the first step towards proving ...
• 161k

### Proof Carrying LLVM?

This is a project I've been thinking of venturing into for a few years now, and I was fortunate to have a very useful discussion about it at the time I started planning it with Chris Lattner (at the ...
• 201
Accepted

### on coq: Why is the proof complete after proving only for one induction when we have more than one variable?

You do not have to prove things by induction. For example, you can prove $\forall n : \mathbb{N} \,.\, n = n$ without induction by applying reflexivity. In your proof, we use induction on $a$, but ...
• 30.9k
Accepted

### Halting problem vs. automated theorem proving?

The notion of automating mathematics is a vague one, and that's accounting for the discrepancy here. One interpretation would be: to automate mathematics would be to produce a machine $M$ which could ...
• 2,783

### Halting problem vs. automated theorem proving?

You are conflating two possible meanings of the phrase "mathematics can be automated": "any theorem can be proved true or false by an algorithm" "the practical activity of proving theorems, as ...
• 3,543

### Prove simple theorems in Haskell in automated way

Look at Agda [1][2] I think that it's exactly what you are looking for. I recommend using its emacs mode for autocompletion and hole/interactive programming. [2]/quick-guide.html A very good ...
Accepted

### Prove simple theorems in Haskell in automated way

SMT (satisfiablity-modulo-theories) solvers can provide an (almost-) push-button solution for at least a subset of such problems, especially for those that use machine-arithmetic, IEEE-floats, etc., ...
• 211
In your case, the simplest solution may be to use SAT. Your first clause includes $x \le 0.25$ and $x > 0.91$. This means that there are five regions of interest for the variable $x$, which we ...
I've recently came to these Coq tutorials from $\lambda$conf2017 so I've figured out it's worth sharing here for whoever visits this question later. Gabriel Claramunt - Introduction to Coq - Part 1 ...