new inference rule functions in logic module

[bd435cb6-4d8d-4732-bb6a-b71bfd0d7ca6]

This ticket is for introducing inference rules to sage's logic module. The functions were added in a new source file called rule.py. These functions return the result of applying a rule of inference to certain formulas, as well as determine whether a particular rule of inference has been applied correctly.

Depends on #14951 Depends on #14952 Depends on #15013 Depends on #15018 Depends on #15040

Component: misc

Keywords: logic, inference rules

Author: Paul Scurek

Issue created by migration from https://trac.sagemath.org/ticket/15041

[bd435cb6-4d8d-4732-bb6a-b71bfd0d7ca6]

Attachment: trac_14951_tokenize_tree_fix.patch.gz

Attachment: trac_14952_logic_if_while_syntax.patch.gz

[bd435cb6-4d8d-4732-bb6a-b71bfd0d7ca6]

Attachment: trac_15013_logic_docstrings.patch.gz

[bd435cb6-4d8d-4732-bb6a-b71bfd0d7ca6]

Attachment: trac_15018_recover_formula.patch.gz

Attachment: trac_15040_errorhandling_logicparser.patch.gz

[bd435cb6-4d8d-4732-bb6a-b71bfd0d7ca6]

Attachment: trac_15041_inference_rules.patch.gz

This is the patch for this ticket, but it depends on the previous ones. Apply all patches in the order they appear.

[bd435cb6-4d8d-4732-bb6a-b71bfd0d7ca6]

comment:1

The last patch listed in the attachments, trac_15041_inference_rules.patch​, is the only one that should be integrated into sage for this ticket. The first five patches are the patches from the dependencies of this ticket, which were placed here for the convenience of the reviewer.

[williamstein]

comment:2

REPORT:

• the first part of the patch just removes some whitespace from the general interact library, and as far as I can tell has nothing to do with this ticket. I'm still for it though, and it looks fine to me.

• What's up with this in rule.py (all over in various places) -- it seems like the "useless try/except" -- please explain:

    try:
        trees = logicparser.get_trees(premise1, premise2)
    except SyntaxError:
        raise

• Everything else looks good to me.