Skip to main content
Share Your Experience: Take the 2024 Developer Survey
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