Talk:Proof: Difference between revisions
→Satisfaction
mNo edit summary |
|||
Line 18:
:::: I don't know about Salmon, but all you can do in C, J, Tcl or whatever is [http://www.andres-loeh.de/LambdaPi/LambdaPi.pdf implement] dependently typed language or proof system, i.e. define syntax for terms and types (or terms, formulas and deduction rules) and write an unification algorithm on types and terms. — [[User:Ht|Ht]] 03:23, 1 June 2012 (UTC)
::::: For output: that was the point of asking for rejection of an invalid proof, so that there would be something to output.
::::: For J: I have restricted the vocabulary, and am rejecting all statements which go beyond that vocabulary. I am only guaranteeing that if the statement is accepted that the proof is valid, I am not guaranteeing that the statement is invalid if it is rejected. We do not need to create new syntax if we can reject syntax that would have otherwise have been valid. --[[User:Rdm|Rdm]] 05:24, 1 June 2012 (UTC)
== Huh? ==
| |||