search

ubc-carnap-team / Rudolf

Truth Tree Widget for Carnap
2 stars 3 forks source link

Allow multiple rows to reference the same previous row (on the same branch). #86

Open McTano opened 4 years ago

McTano commented 4 years ago

This explanation will probably be hard to follow, as it relates to implementation details that are not well documented yet.

The current implementation of tableau->sequent conversion has the following constraint: A tableau which refers to an earlier row more than once on the same branch will cause the conversion to fail.

This is because, at each node, the conversion removes the cited formula from the array of formulas which is passed down to the next recursive call, and because the row cited by a node must appear as the row of one of the formulas in the current array.

Changing this probably requires changing the sequent rules on the Carnap side so that the formulas being resolved must be repeated in the sequent premise. However, this would cause a problem with the 'Lit' rule.

It may be necessary to have different conversion behaviour for the SL and QL checkers.

McTano commented 4 years ago

Since this will fall under implementing FOL #87 , I'll close this issue.

McTano commented 3 years ago

Reopening since this can be fixed prior to actually having a checker to support #87.

Having thought about this more, the way to do it is probably to keep track of all the formulas, including previously discharged ones. Then we can use 'Struct' or an explicit weakening rule to add them at the stage where we reorder the formulas.