Page 723 of 800
| Page 723 of 800 | Search internet |
Origin: check. Landing-place: diagnose.
Ponens-seqop used on non-inference R
The Ponens sequent operator applied to a sequent 
yields 
. Thus, the Ponens operator allows to move a hypothesis h from the conclusion to the set of premisses. Meta-modus-ponens can be implemented as a Cut sequent operator whose second argument has a Ponens sequent operator as principal operator.
The 'Ponens-seqop used on non-inference' indicates that the conclusion of the sequent did not have form 
. The error may indicate an error in the proof or a bug in a tactic.
| Page 723 of 800 | Search logiweb.eu |