Incorporating a function for Tautological Implication in the Logic Module

[Medha210699]

This ticket defines a method is_consequence for the class BooleanFormula. This method provides the same functionality as the function valid_consequence (which is now deprecated): the method returns True if self is a tautological consequence of the given formula(s).

sage: f = propcalc.formula("a")
sage: g = propcalc.formula("a|b")
sage: f.is_consequence(g)
False
sage: g.is_consequence(f)
True

In addition, the function call is_consequence(conclusion,hypotheses) is defined to be a synonym for conclusion.is_consequence(hypotheses) and is therefore a drop-in replacement for the deprecated function valid_consequence.

Component: symbolics

Keywords: logic, symbolics, propositional formula

Author: Medha Sharma, Dave Morris

Branch/Commit: bbec2e6

Reviewer: Dave Morris, Travis Scrimshaw

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

[Medha210699]

Author: Medha Sharma

[videlec]

comment:3

A ticket should be set in needs review when it provides source code ready to be integrated into Sage.

[Medha210699]

Branch: u/Medha210699/incorporating_a_function_for_tautological_implication_in_the_logic_module

[embray]

comment:6

Ticket retargeted after milestone closed

[DaveWitteMorris]

Reviewer: Dave Morris

[DaveWitteMorris]

comment:7

I recommend closing this ticket as "invalid/wontfix", because the functionality is already available by using sage.logic.propcalc.valid_consequence.

sage: from sage.logic.propcalc import valid_consequence
sage: f = propcalc.formula("a")
sage: g = propcalc.formula("a|b")
sage: valid_consequence(g,f) # is g a tautological consequence of f ?
True
sage: valid_consequence(f,g) # is f a tautological consequence of g ?
False

[tscrim]

comment:8

Perhaps it would be good to add a method valid_consequence that redirects to this function to make it more discoverable?

[DaveWitteMorris]

comment:9

Thanks, that seems like a good idea. I'll do it soon, but probably not today. Probably it makes the most sense to move the definition into a method, and then (for backward compatibility) define a stand-alone function that calls the method. Perhaps the stand-alone should be deprecated?

[tscrim]

comment:10

I don't use this, so I don't have an option. I think it is okay to have a method redirect to a function (or vice versa; they are equivalent in my mind up to putting the definition in the method to make it easier to see via ? on the command-line). There might be some reason for having the actual computation done in a function (which could be in a separate file). Actually, the easiest thing to do would be to simply make the function into a (bounded) method of the appropriate class. I think you just need:

def foo(x, y):
    return -y
class Bar:
    foo = foo

sage: b = Bar()
sage: b.foo(2)
-2

This would mean everything in the doc, etc. is properly linked without redundancy. This would be my recommendation.

[DaveWitteMorris]

Changed branch from u/Medha210699/incorporating_a_function_for_tautological_implication_in_the_logic_module to public/28052

[DaveWitteMorris]

Commit: e9d0529

[DaveWitteMorris]

comment:12

Thanks for telling me about foo = foo. I was going to do something more complicated.

1. I defined a method of the class BooleanFormula by moving the code for valid_consequence from propcalc.py into boolformula.py.
2. I named the method is_consequence (and also defined a standalone function of this same name), to be consistent with the methods is_satisfiable, is_contradiction, etc., but retained valid_consequence as a deprecated function for backwards compatibility (in the file propcalc.py).
3. I refactored the code for the is_consequence method, added coverage of the case where there are no hypotheses, and added more doctests.
4. I made some other minor tweaks to propcalc.py and boolformula.py, such as changing "http" to "https".
5. I revised the description of this ticket.
   Should some of this be on a separate ticket?

---

New commits:

e9d0529

move function to method of BooleanFormula

[DaveWitteMorris]

Changed author from Medha Sharma to Medha Sharma, Dave Morris

[DaveWitteMorris]

comment:14

Merge conflict.

[sagetrac-git]

Changed commit from e9d0529 to 6c0e20a

[sagetrac-git]

Branch pushed to git repo; I updated commit sha1. New commits:

7dc3dcd	fix conflict with #28053
6c0e20a	merge with 9.1b8

[DaveWitteMorris]

comment:16

Fixed the merge conflict with #28053 and merged 9.1b8. I hope the patchbots will be happy now.

[tscrim]

Changed reviewer from Dave Morris to Dave Morris, Travis Scrimshaw

[tscrim]

comment:17

Some little comments:

-if not(hypotheses):
+if not hypotheses:

Remove self as an INPUT:.

Beyond that, LGTM.

[sagetrac-git]

Changed commit from 6c0e20a to bbec2e6

[sagetrac-git]

Branch pushed to git repo; I updated commit sha1. New commits:

bbec2e6

minor corrections pointed out by reviewer

[DaveWitteMorris]

comment:19

Thanks for the corrections.

[tscrim]

comment:20

Thank you. LGTM.

[vbraun]

Changed branch from public/28052 to bbec2e6