Talk:Proof assistant
| WikiProject Computer science | (Rated Start-class, High-importance) | |||||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
|
||||||||||||||||||||||||
| WikiProject Mathematics | (Rated Start-class, Mid-priority) | ||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| |||||||||||||
 | The contents of the Automated proof checking page were merged into Proof assistant. For the contribution history and old versions of the redirected page, please see its history; for the discussion at that location, see its talk page. |
 To-do list for Proof assistant: | |
|---|---|
|
| |
See also (merge?) Computer-assisted proof Outs 10:05, 12 September 2007 (UTC)
Human help[edit]
- "a human can guide the search for proofs"
Agda[edit]
- 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)
Small Kernel[edit]
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)
Comparison table: contents and meaning?[edit]
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). — Preceding unsigned comment added by Horaceb (talk • contribs) 10:38, 5 July 2016 (UTC)
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)
Idris[edit]
Maybe someone wants to add Idris. I don't know all the fields to fill. 91.66.12.246 (talk) 19:19, 29 December 2016 (UTC)
