Machine-checked, machine-generated or machine-verified proofs
2
votes
1answer
36 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
85 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 ...
0
votes
0answers
36 views
What are the limitations of automated deduction and theorem proving? [closed]
I do not have any background in mathematical logic, but I have studied computation and complexity theory. I have looked through some textbooks and there are distinctions between different kinds of ...
7
votes
1answer
108 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. ...
7
votes
1answer
101 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
133 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 ...
5
votes
3answers
341 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.
...
8
votes
2answers
155 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. ...
10
votes
1answer
228 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 ...
11
votes
5answers
823 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 ...
