The Stack Overflow podcast is back! Listen to an interview with our new CEO.

# Questions tagged [proof-assistants]

Applications that allow to create formal proofs. They assist the user by finding partial and checking complete proofs.

61 questions
Filter by
Sorted by
Tagged with
943 views

### Euclidean Algorithm in Coq

Question How do I write more intuitive proofs of the two following results in Coq? ...
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, ...
40 views

### Recursive set - How to show a language is undecidable [duplicate]

I am currently working on the following task: A language L = {< M> | M(x) = x^2} is given. Now I need to show, that this language is not decidable. By the way, < M> is the Gödel number But ...
628 views

### The “CPS” approach has done great harm to performance in SML/NJ; reasoning desired

In a comment to Learning F#: What books using other programming languages can be translated to F# to learn functional concepts? Makarius stated: Note that the "CPS" approach has done great harm to ...
645 views

### Is there a repository for the hierarchy of proofs?

I am self-learning proof assistants and decided to start on some basic proofs and work my way up. Since proofs are based on other proofs and so form a hierarchy, is there a repository of the hierarchy ...
169 views

### Looking for a book that derives and constructs a model checking application

I am teaching myself program verification and am currently learning proof assistants. I have the book Handbook of Practical Logic and Automated Reasoning which gives the proofs necessary for the ...
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. ...
360 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,...
978 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 ...