TautologyQ[bf]
gives True if all combinations of values of variables make the Boolean function bf yield True.
TautologyQ[expr,{a1,a2,…}]
gives True if all combinations of values of the ai make the Boolean expression expr yield True.
TautologyQ
TautologyQ[bf]
gives True if all combinations of values of variables make the Boolean function bf yield True.
TautologyQ[expr,{a1,a2,…}]
gives True if all combinations of values of the ai make the Boolean expression expr yield True.
Details and Options
- TautologyQ is also known as tautology checking and validity checking.
Examples
open all close allBasic Examples (2)
Test whether Boolean expressions are always true:
TautologyQ[(a || b) && (!a || !b), {a, b}]TautologyQ[(a || b) || (!a && !b), {a, b}]Test whether pure Boolean functions are always true:
TautologyQ[BooleanFunction[220, 3]]TautologyQ[BooleanFunction[2 ^ 2 ^ 10 - 1, 10]]Applications (4)
Use TautologyQ to prove equivalence for different representations:
Table[BooleanConvert[BooleanFunction[30, {a, b, c}], form], {form, {"DNF", "CNF", "ANF", "NAND", "NOR"}}]TautologyQ[Equivalent@@%]Convert a Boolean function using a "care set" or condition:
f = BooleanCountingFunction[{2, 3}, 4][a, b, c, d]cond = Xor[a, b, c, d]g = BooleanConvert[f, cond]h = BooleanConvert[f, "CNF", cond]The resulting forms are equivalent when cond is true:
TautologyQ[Implies[cond, Equivalent[f, g, h]]]They are not equivalent without the condition:
TautologyQ[Equivalent[f, g, h]]Prove proof rules, like modus ponens
:
TautologyQ[Implies[Implies[a, b]∧a, b]]TautologyQ[Implies[Implies[a, b]∧¬b, ¬a]]TautologyQ[Implies[(a∨b)∧¬a, b]]TautologyQ[Implies[¬(a∧b)∧a, ¬b]]TautologyQ[Implies[Implies[a, b]∧Implies[a, ¬b], ¬a]]A Boolean function
is increasing in
iff
. Implement a test for a Boolean function to be increasing and explore what Boolean functions are increasing:
BooleanIncreasingQ[f_, vars_List] :=
And@@Table[TautologyQ[Implies[f /. vars[[i]] -> False, f /. vars[[i]] -> True]], {i, Length[vars]}]BooleanIncreasingQ[f_] := BooleanIncreasingQ[f, BooleanVariables[f]]These functions are all increasing in all their variables:
{BooleanIncreasingQ[x], BooleanIncreasingQ[x∧y], BooleanIncreasingQ[x∨y]}These functions are all decreasing in
:
{BooleanIncreasingQ[¬x, {x}], BooleanIncreasingQ[¬x∧y, {x}], BooleanIncreasingQ[¬x∨y, {x}]}{BooleanIncreasingQ[¬x, {y}], BooleanIncreasingQ[¬x∧y, {y}], BooleanIncreasingQ[¬x∨y, {y}]}Find all increasing bivariate functions:
fl = Table[BooleanFunction[i, {x, y}], {i, 0, 2 ^ 2 ^ 2 - 1}];Select[fl, BooleanIncreasingQ]Find all increasing trivariate functions:
fl = Table[BooleanFunction[i, {x, y, z}], {i, 0, 2 ^ 2 ^ 3 - 1}];Select[fl, BooleanIncreasingQ]Properties & Relations (4)
An expression is a tautology if it is true for all variable assignments:
BooleanTable[Implies[Implies[a, b]∧¬b, ¬a], {a, b}]TautologyQ[Implies[Implies[a, b]∧¬b, ¬a], {a, b}]TautologyQ[f] is equivalent to ¬SatisfiableQ[¬f]:
¬SatisfiableQ[¬Implies[Implies[a, b]∧¬b, ¬a]]TautologyQ[Implies[Implies[a, b]∧¬b, ¬a]]An expression of
variables is a tautology if the SatisfiabilityCount is
:
SatisfiabilityCount[Implies[Implies[a, b]∧¬b, ¬a]]TautologyQ[Implies[Implies[a, b]∧¬b, ¬a]]Use TrueQ to test whether an expression is explicitly identical to True:
TrueQ[True]TrueQ[Implies[Implies[a, b]∧¬b, ¬a]]See Also
Related Guides
History
Text
Wolfram Research (2008), TautologyQ, Wolfram Language function, https://reference.wolfram.com/language/ref/TautologyQ.html.
CMS
Wolfram Language. 2008. "TautologyQ." Wolfram Language & System Documentation Center. Wolfram Research. https://reference.wolfram.com/language/ref/TautologyQ.html.
APA
Wolfram Language. (2008). TautologyQ. Wolfram Language & System Documentation Center. Retrieved from https://reference.wolfram.com/language/ref/TautologyQ.html
BibTeX
@misc{reference.wolfram_2026_tautologyq, author="Wolfram Research", title="{TautologyQ}", year="2008", howpublished="\url{https://reference.wolfram.com/language/ref/TautologyQ.html}", note=[Accessed: 13-June-2026]}
BibLaTeX
@online{reference.wolfram_2026_tautologyq, organization={Wolfram Research}, title={TautologyQ}, year={2008}, url={https://reference.wolfram.com/language/ref/TautologyQ.html}, note=[Accessed: 13-June-2026]}