c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig TableauxProp = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include PL %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder pos : o -> type. %prefix 0 pos.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder neg : o -> type. %prefix 0 neg.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder close: pos A -> neg A -> #.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder true1 : pos true -> #.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder false0 : neg false -> #.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder not1 : (neg A -> #) -> (pos not A -> #).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder not0 : (pos A -> #) -> (neg not A -> #).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder and1 : (pos A -> pos B -> #) -> (pos A and B -> #).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder and0 : (neg A -> #) -> (neg B -> #) -> (neg A and B -> #).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder or1 : (pos A -> #) -> (pos B -> #) -> (pos A or B -> #).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder or0 : (neg A -> neg B -> #) -> (neg A or B -> #).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder imp1 : (neg A -> #) -> (pos B -> #) -> (pos A imp B -> #).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder imp0 : (pos A -> neg B -> #) -> (neg A imp B -> #).