11

You are correct, there is an error in that paper, and the rule should indeed read: $$\frac{\Gamma\vdash M:\Delta}{\Gamma\vdash M\cong M} $$ the use of jugements of this style for equality (sometimes called "typed equality") originates already in Martin-Löf, I think (see here for example). It's often replaced with an untyped operational definition in modern ...


5

There is a paper by Beyersdorff and Chew on the proof complexity of calculi for non-monotonic logic. In the references of this paper you will find links to the papers where these calculi are defined.


3

Yes, backtracking in focused proof search may be necessary due to a wrong choice of focus formula. Consider the provable sequent $$\vdash p\otimes q, (p^\bot\mathrel{\wp} q^\bot)\otimes r, r^\bot.$$ Choosing to focus on $p\otimes q$ leads to a dead end, because however you "split" the context you end up with an atom ($p$ or $q$) without matching ...


Only top voted, non community-wiki answers of a minimum length are eligible