Skip to main content
11 votes
Accepted

Typo in the calculus of constructions paper?

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 ...
cody's user avatar
  • 13.9k
5 votes
Accepted

Sequent calculus for nonmonotonic/defeasible logics?

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.
Jan Johannsen's user avatar
3 votes
Accepted

Does focused proof search ever have to backtrack across the choice of focus formula?

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.$$ ...
Damiano Mazza's user avatar

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