First commit: almos every clausification rule, plus some contextual rules #1
Conversation
signature/alethe.eo
Outdated
| ; - conclusion Bool: Conclusion of the "subproof" step. | ||
| ; return: > | ||
| ; A boolean indicating if "conclusion" is of the form | ||
| ; @cl not assumption, premise. |
There was a problem hiding this comment.
I think for the SMT familiar reader it might be easier to read as an S-Expr: (@cl (not assumption) premise)
| ) | ||
|
|
||
| ;;;;;;;;;;;;;;;;;;;;;;; | ||
| ; Rule 4: false |
There was a problem hiding this comment.
I like this style of comment.
Maybe you could also add the state of each rule here? I.e. whether it is fully checked etc.
There is one risk: when we add a rule to the Alethe document we, don't necessarily add it to the end. So rules numbers might end up shifting around.
There was a problem hiding this comment.
I like this style of comment. Maybe you could also add the state of each rule here? I.e. whether it is fully checked etc.
Perfect. You mean adding the state within the heading? Like in
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Rule 4: false (fully checked)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
?
Or by adding a new yaml tag to the corresponding declare-rule?
There is one risk: when we add a rule to the Alethe document we, don't necessarily add it to the end. So rules numbers might end up shifting around.
With regard to the rule number, I could remove them, if they can lead to confusion in the future. Though, are they actually helpful?
There was a problem hiding this comment.
Note that you can already use the rule attribute :sorry if the rule isn't properly checked yet.
There was a problem hiding this comment.
Note that you can already use the rule attribute
:sorryif the rule isn't properly checked yet.
Awesome! I like the checker's answer better with this ":sorry" rules.
| (($last_eq_right (and (@cl (= t1 t2)))) t2) | ||
| (($last_eq_right (and (@cl (= t1 t2)) eqs)) ($last_eq_right eqs)) | ||
| ; TODO: are they always clauses? (seems that it is not the | ||
| ; case if the premises where just "assume"s) |
There was a problem hiding this comment.
So this is a general question: how should the assumes be handled?
They can't be wrapped in @cl, because otherwise reference checking failed. On the other hand that introduces ugly special cases here.
Maybe we should add a helper step that transfers every assumptions into a clause?
There was a problem hiding this comment.
So this is a general question: how should the assumes be handled? They can't be wrapped in
@cl, because otherwise reference checking failed. On the other hand that introduces ugly special cases here. Maybe we should add a helper step that transfers every assumptions into a clause?
You are totally right. That piece of code is one of my initial attempts at mechanizing something, and it shows xD I saw that you even defined a function $to_cl to that end. I will use it.
There was a problem hiding this comment.
They can't be wrapped in
@cl, because otherwise reference checking failed.
Ah!, forgot to ask: what would "reference checking" mean here?
signature/programs.eo
Outdated
| ; program: context_get_substitute | ||
| ; args: | ||
| ; - context_get_substitute nil: | ||
| ; return: |
There was a problem hiding this comment.
shouldn't there be something here
There was a problem hiding this comment.
Yes :) That is because I have an elisp function that introduces comments, but, from time to time I forgot to complete them. Thanks!
signature/programs.eo
Outdated
| ; program: context_get_var_subst_pairs | ||
| ; args: | ||
| ; - context_get_var_subst_pairs nil: | ||
| ; return: |
signature/programs.eo
Outdated
| ; args: | ||
| ; - $get_free_variables nil: | ||
| ; return: | ||
| (program $get_free_variables ((A Type) |
There was a problem hiding this comment.
As Andy said this can likely be simplified by having a parameter in head position.
Perfect. In the meantime, I will be fixing the code following your review. |
No description provided.