Questions tagged [proof-assistants]

Applications that allow to create formal proofs. They assist the user by finding partial and checking complete proofs. General questions about proof assistants can also be asked on the Proof Assistants Stack Exchange site.

Filter by
Sorted by
Tagged with
48 votes
6 answers
10k 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 ...
Guy Coder's user avatar
  • 5,101
18 votes
3 answers
3k 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. ...
Guy Coder's user avatar
  • 5,101
1 vote
2 answers
358 views

What to prove and how to prove it

In learning about proof theory, I am interested to know how to go about "proving properties of a program". I don't exactly see yet what needs to be proven, nor how to prove it, which leads to this ...
Lance's user avatar
  • 2,223
23 votes
2 answers
3k views

Recursive definitions over an inductive type with nested components

Consider an inductive type which has some recursive occurrences in a nested, but strictly positive location. For example, trees with finite branching with nodes using a generic list data structure to ...
Gilles 'SO- stop being evil''s user avatar
20 votes
1 answer
1k 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 ...
Guy Coder's user avatar
  • 5,101
16 votes
2 answers
462 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. ACL2,...
Guy Coder's user avatar
  • 5,101
10 votes
2 answers
2k 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, ...
user11942's user avatar
  • 161
6 votes
2 answers
348 views

Can we prove that $1 + 2 + \dots + n = \frac{n(n+1)}{2}$ using a computer program?

Chapter 7 of The Haskell Road to Logic Math and Programming discusses induction and recursion. Haskell is strongly typed and we can define the natural numbers ...
john mangual's user avatar
  • 1,951
5 votes
2 answers
497 views

What does it mean if we disable K-rule in Agda?

TL;DR: Can I say, "K-rule in Agda enables people to match $ \forall a.a \equiv a $ with $ \mathit{refl} $"? In https://agda.readthedocs.io/en/v2.5.4.1/language/without-k.html#without-k, K-...
ice1000's user avatar
  • 940
1 vote
1 answer
79 views

Time complexity of algorithms

I have some questions that I don't understand about time complexity. Given that the worst case complexity of the algorithm $A$ is $O(f(n))$ and the best case complexity of $A$ is $Ω(g(n))$. It ...
Math4me's user avatar
  • 249
1 vote
1 answer
365 views

Let M be an $\epsilon$-NFA and let $S\subseteq Q$. Prove $\epsilon (S) = \epsilon (\epsilon (S))$

Let M be an $\epsilon$-NFA and let $S\subseteq Q$. Prove $\epsilon (S)= \epsilon (\epsilon (S))$. I would like to prove this by contradiction but I don't know if my idea is correct. Definition of $...
Mandy's user avatar
  • 177