Lack of arguments for rules like `and` can make reconstruction hard

The rule and does not have as an argument the index of the conjunct that is concluded. This can be problematic because of the general ambiguity due to n-ary operators: (and a (and a b)) could be seen as both (and a a b) and (and a (and a b)).

I'd say then that the index could be given as an optional argument. What do you think?

I think we should also consider making it a mandatory argument. I believe both in cvc5 and veriT it would be easy to add, and for consumers it's not harder to ignore a mandatory argument than it is to ignore an optional argument.

Sounds good to me.

@hjsc will put it in the standard, @hjsc will change veriT, @hbarbosa will change cvc5. @Lachnitt will change Isabelle. @hbarbosa will change Carcara

I suggest also add the same requirement for the not_or rule, which is very similar to this one.

added todo-Carcara todo-Isabelle todo-cvc5 todo-specification todo-veriT labels

and_pos and or_neg could also profit from this. They are essentially the tautology versions of and and not_or.

Good point. I suggest to update all four at the same time.

mentioned in merge request !9 (merged)

Both cvc5 and Carcara have been update to support the argumenst for and, not_or, and_pos and or_neg.

removed todo-cvc5 label

removed todo-Carcara label

mentioned in commit 7b55835b

closed with merge request !9 (merged)

reopened

removed todo-specification label

removed todo-veriT label

This is now done in veriT

removed todo-Isabelle label

@hjsc It seems like the index is off by one in veriT. It should start at 1 and end at n:

But I get proofs with steps where the argument is 0. I don't have a good small example right now but will find one.

@hbarbosa same seems to be the case in cvc5. We can also change the Standard, if you both rather do that.

I think the standard should change. If you agree, I created a merge request: !15 (merged)