46
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 ...
- 30k
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 ...
- 7,768
15
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 ...
- 6,958
12
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 ...
- 81.4k
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 ...
- 3,127
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
...
- 8,308
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 ...
- 8,308
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 ...
- 8,114
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 \...
- 8,114
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 (...
- 30k
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 ...
- 531
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. ...
- 176
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 ...
- 29.7k
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.♦
- 156k
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 ...
- 8,308
5
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://...
- 51
5
votes
Accepted
How can I check constraints on my state machine behaviour?
Use a model checker. This is exactly what they're good for. You might look at SPIN and NuSMV as a starting point, but there are many others as well.
D.W.♦
- 156k
4
votes
Accepted
What happens to uninterpreted predicates in Ackermann's reduction?
Essentially, you can treat uninterpreted predicates as boolean-valued functions (adding a new boolean sort if necessary) and replace them with boolean variables as you would other functions. For the ...
- 2,178
4
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 ...
- 522
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 ...
- 707
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 ...
- 2,255
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.♦
- 156k
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.♦
- 156k
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.♦
- 156k
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 ...
- 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 ...
- 30k
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 ...
- 2,713
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 ...
- 3,473
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 ...
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., ...
- 211
Only top scored, non community-wiki answers of a minimum length are eligible