logitext
logitext copied to clipboard
Feature request: eliminate duplicates in sequent lists
I was exploring whether I could have my discrete structures class use this for logic puzzles like knight and knaves. I'll have to look at the code after the semester, but it would be nice to have an option to eliminate repeated literals (or expressions) in the lists of sequents.
E.g.,
A: B is a knave if and only if C is a knight
B: C is a knight or A is a knave
A <-> (~B <-> C), B <-> (C / ~A) |-
It would be cleaner if it would derive B,C |- A instead of B,C,C,B |- A and B,C,B |- A,A.