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.

Filter by
Sorted by
Tagged with
2
votes
0answers
29 views

How does supercompilers relate to macro tree transducers?

Supercompilers can be used as a generalisation of deforestation of a functional program. Macro Tree Transducers composition can be used to the same effect, using a completely different approach. What ...
16
votes
4answers
358 views

Has Anyone Actually Created a System that Writes Computer Programs from specification?

Has anyone ever actually written a system (software or detailed explanation on paper with simple examples) that generates computer programs? I input $Prime(x) \wedge x<10$ and it creates a program ...
5
votes
1answer
943 views

Euclidean Algorithm in Coq

Question How do I write more intuitive proofs of the two following results in Coq? ...
9
votes
2answers
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, ...
0
votes
0answers
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 ...
16
votes
2answers
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,...
11
votes
1answer
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 ...
15
votes
4answers
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 ...
6
votes
1answer
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 ...
15
votes
3answers
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. ...
19
votes
1answer
979 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 ...