Talk:Proof assistant

Computer science Start‑class High‑importance

This article is within the scope of WikiProject Computer science, a collaborative effort to improve the coverage of Computer science related articles on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.Computer scienceWikipedia:WikiProject Computer scienceTemplate:WikiProject Computer scienceComputer science articles

Start

This article has been rated as Start-class on Wikipedia's content assessment scale.

High

This article has been rated as High-importance on the project's importance scale.

Things you can help WikiProject Computer science with:

Here are some tasks awaiting attention:

Article requests :
- Requested articles/Applied arts and sciences/Computer science, computing, and Internet
Cleanup :
- Computer science articles needing attention
- Computer science articles needing expert attention
Copyedit :
- Computing
Expand :
- Computer science
Infobox :
- Computer science articles without infoboxes
Maintain :
- Timeline of computing 2020–present
Photo :
- Find pictures for the biographies of computer scientists (see List of computer scientists)
- Computing articles needing images
Stubs :
- Computer science stubs
Unreferenced :
- WikiProject Computer science/Unreferenced BLPs
Project-related :
- Tag all relevant articles in Category:Computer science and sub-categories with {{WikiProject Computer science}}

Mathematics Start‑class Mid‑priority

	Mathematics portal This article is within the scope of WikiProject Mathematics, a collaborative effort to improve the coverage of mathematics on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.MathematicsWikipedia:WikiProject MathematicsTemplate:WikiProject Mathematicsmathematics articles
Start	This article has been rated as Start-class on Wikipedia's content assessment scale.
Mid	This article has been rated as Mid-priority on the project's priority scale.

Human help

"a human can guide the search for proofs"
- Can someone give an example where there is a practical need for a human to guide the search for a proof? What kind of proof steps are better done by humans? --Abdull (talk) 08:54, 11 September 2010 (UTC)[reply]

Agda

I'm not quite sure where to put it in this list, but Agda probably belong here, too. KLuwak (talk) 14:20, 2 April 2011 (UTC)[reply]

Small Kernel

I have experience of using Agda and Coq, and as far as I know their source code neither of them has a small kernel. --Konstantin.Solomatov (talk) 05:15, 20 July 2014 (UTC)[reply]

Comparison table: contents and meaning?

It would be great to add the logic language and rules used by the system (even if some PA like Isabel can deal with more than one set of rules).

I edited the table where I thought some of the feature evaluations were unclear. What are "partial" dependent types, for instance? There either are or aren't some types dependent on specific values. So far as I know, that's the definition of dependent types. If someone wants to put "partial" back, could they please explain what it means? Similarly for proof automation, ACL2 and PVS---which do not have small trusted computing bases---were listed as having "partial" automation because the automation is unverified; i.e., it is in the TCB. That seems already addressed in the Small Kernel section, to me.

This is a minor improvement, but I think overall it's not clear why the specific set of features in the table were chosen, or what exactly constitutes "partial" or N/A. Nothing in the table has a citation, for instance, to show that some reputable source both considers these criteria significant and agrees with the results presented here.

MisterCarl (talk) 22:23, 20 September 2012 (UTC)[reply]