Logic

 Tautology
 test for a tautology

 Calling Sequence Tautology(b, p) Contradiction(b, p)

Parameters

 b - Boolean expression p - (optional) unevaluated name

Description

 • The Tautology and Contradiction commands test whether the given Boolean expression b is a tautology or a contradiction.
 • The Tautology(b) calling sequence returns true if b is a tautology (true for every valuation of its variables) and false otherwise. Similarly, Contradiction(b) returns true if b is a contradiction (false for every valuation of its variables) and false otherwise.
 • If the parameter p is supplied and the test returns false, then a valuation is assigned to p which demonstrates a negative result. Otherwise, p is assigned NULL. Note that the test may be significantly faster if p is not given.

Details

 • The problem of determining whether every possible assignment of truth values satisfies a given Boolean formula is the dual of the Boolean satisfiability problem and is known to be co-NP-complete, meaning that no polynomial-time algorithm is presently known.

Examples

 > $\mathrm{with}\left(\mathrm{Logic}\right):$
 > $\mathrm{Tautology}\left(\left(\left(a\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&and\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}b\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&or\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left(¬\left(a\right)\right)\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&or\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left(¬\left(b\right)\right)\right)$
 ${\mathrm{true}}$ (1)
 > $\mathrm{Tautology}\left(\left(a\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&iff\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}b\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&or\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}b,'p'\right)$
 ${\mathrm{false}}$ (2)
 > $p$
 $\left\{{a}{=}{\mathrm{true}}{,}{b}{=}{\mathrm{false}}\right\}$ (3)
 > $\mathrm{Tautology}\left(a\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&or\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left(¬\left(a\right)\right),'p'\right)$
 ${\mathrm{true}}$ (4)
 > $p$
 > $\mathrm{Contradiction}\left(\left(a\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&or\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left(¬\left(a\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&and\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}b\right)\right)\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&nor\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}b\right)$
 ${\mathrm{true}}$ (5)
 > $\mathrm{Contradiction}\left(\left(a\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&iff\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}b\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&or\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}b,'p'\right)$
 ${\mathrm{false}}$ (6)
 > $p$
 $\left\{{a}{=}{\mathrm{false}}{,}{b}{=}{\mathrm{true}}\right\}$ (7)
 > $\mathrm{Contradiction}\left(\left(¬\left(a\right)\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&and\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}a,'p'\right)$
 ${\mathrm{true}}$ (8)
 > $p$