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 ...
- 14k
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.
- 4,640
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.$$
...
- 5,598
Only top scored, non community-wiki answers of a minimum length are eligible