Machine-checked, machine-generated or machine-verified proofs

learn more… | top users | synonyms

1
vote
1answer
37 views

Automated theorem proving with SAT

If you had a polynomial time algorithm for determining boolean satisfiability how would you prove/disprove a conjecture like the Reimann-Zeta hypothesis (or the Pythagorean theorem for that matter) ...
3
votes
1answer
163 views

Euclidean Algorithm in Coq

Question How do I write more intuitive proofs of the two following results in Coq? ...
7
votes
2answers
158 views

Theorem Proofs in Coq

Background I am learning assistance, Coq, on my own. So far, I have completed reading Yves Bertot's Coq in a Hurry. Now, my goal is to prove some basic results concerning the natural numbers, ...
2
votes
1answer
83 views

What is the difference between “definition” and “inductive” in Coq?

In Coq, you can use two different kinds of keywords to do definitions--Inductive and Definition. I do not understand the difference between an inductive and a definition, or when it is appropriate to ...
3
votes
2answers
338 views

Equivalence of NFA and DFA - proof by construction

I was looking at the construction proof showing the equivalence of NFA and DFA from Sipser's text. It started by taking number of states of DFA as $\mathcal{P}(Q)$, where $\mathcal{P}(Q)$ is the set ...
7
votes
1answer
133 views

Redundancy elimination in the superposition calculus

When proving theorems with the superposition calculus, we deal with three kinds of rules: Generating rules: from pair of clauses A and B, generate new clause C while keeping the original pair, e.g. ...
9
votes
1answer
177 views

Distinct variables for different clauses

In resolution theorem proving, it is normally assumed variables in different clauses are distinct. This is not something that happens automatically; it requires significant extra code and computation ...
4
votes
1answer
223 views

Automated geometric theorem-proving using synthetic methods

This question is about geometric theorem proving and is inspired by this Math.SE post. Currently, Euclidean-geometric theorem provers, as referred to in the post, use coordinate geometry to convert ...
8
votes
3answers
687 views

Why is unification so important to inference engines?

I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here. I keep reading about the Unification Algorithm. ...
9
votes
2answers
195 views

Why do some inference engines need human assistance while others don't?

I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here. Why is it that automated theorem provers, i.e. ...
12
votes
1answer
366 views

Types of Automated Theorem Provers

I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here. Which are the relevant automated theorem provers? I ...
17
votes
5answers
2k views

Learning Automated Theorem Proving

I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here. Note that these topics are not easily digested ...