Skip to main content
45 votes
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 ...
Andrej Bauer's user avatar
  • 30.9k
20 votes
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 ...
Discrete lizard's user avatar
  • 8,303
16 votes
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 ...
Caleb Stanford's user avatar
13 votes
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 ...
David Richerby's user avatar
10 votes

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 ...
Alexey Romanov's user avatar
10 votes
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 ...
Martin Berger's user avatar
10 votes
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 ...
Martin Berger's user avatar
10 votes
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 ...
cody's user avatar
  • 8,233
8 votes

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 \...
cody's user avatar
  • 8,233
8 votes

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 (...
Andrej Bauer's user avatar
  • 30.9k
6 votes

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 ...
Mario Carneiro's user avatar
6 votes

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://...
harshrc's user avatar
  • 61
6 votes
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. ...
Ana Borges's user avatar
5 votes
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 ...
Martin Berger's user avatar
5 votes
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 <...
D.W.'s user avatar
  • 161k
5 votes
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 ...
Joey Eremondi's user avatar
5 votes

Roadmap to formal verification

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 ...
sean's user avatar
  • 532
3 votes

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 ...
user21820's user avatar
  • 727
3 votes
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 ...
Thinh D. Nguyen's user avatar
3 votes
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 ...
D.W.'s user avatar
  • 161k
3 votes

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, ...
D.W.'s user avatar
  • 161k
3 votes
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 ...
D.W.'s user avatar
  • 161k
3 votes

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 ...
Jules's user avatar
  • 201
3 votes
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 ...
Andrej Bauer's user avatar
  • 30.9k
3 votes
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 ...
Noah Schweber's user avatar
3 votes

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 ...
Aaron Rotenberg's user avatar
3 votes

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 ...
seriousquestions's user avatar
3 votes
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., ...
alias's user avatar
  • 211
3 votes

Automated reasoning with real numbers

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 ...
Pseudonym's user avatar
  • 22.2k
2 votes

Learning Automated Theorem Proving

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 ...
Aristu's user avatar
  • 1,483

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