Logics

Added
- Alternative natural deduction system for classical logic (with solver), see docs.

Changed
- Tableaux `is_correct_tree` errors are sorted by LevelOrder.

Added
- `child_index` property to `TableauxNode`.
- More extensive tests for `TableauxSystem`'s `is_correct_tree` method.

Changed
- Error messages on `logics.classes.propositional.proof_theories.tableaux`.
`TableauxSystem`'s `is_correct_tree` method now returns a list of tuples
as `error_list`, where the first member is the tuple of indexes (`int`) leading to the
node from the root and the second is an `str` with the error, instead of a list of `str`.

Fixed
- Various bugs with TableauxSystem's `is_correct_tree` (no missing premises -avoids
marking tableaux that only contain one premise as correct-; all premises must come at
the beginning of the tableaux, before branching and before applying any other rule)

Changed
- TableauxSystem's `is_correct_tree` method now takes an extra `parser` optional parameter
for nicer error displaying.

Added
- Option to `exit_on_first_error` in natural deduction `is_correct_derivation`

Changed
- Natural deduction `is_correct_derivation` accepts rule justifications like `E∧` for
rules that have multiple versions (e.g. `E∧1`, `E∧2`)

Fixed
- Bug fix in natural deduction's `is_correct_derivation` (do not check correct application
of the rule if invalid rule name)