gives True if all combinations of values of variables make the Boolean function bf yield True.


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.


open allclose all

Basic Examples  (2)

Test whether Boolean expressions are always true:

Test whether pure Boolean functions are always true:

Applications  (4)

Use TautologyQ to prove equivalence for different representations:

Convert a Boolean function using a "care set" or condition:

The resulting forms are equivalent when cond is true:

They are not equivalent without the condition:

Prove proof rules, like modus ponens :

Modus tollens :

Modus tollendo ponens :

Modus ponendo tollens :

Reductio ad absurdum :

A Boolean function is increasing in iff . Implement a test for a Boolean function to be increasing and explore what Boolean functions are increasing:

These functions are all increasing in all their variables:

These functions are all decreasing in :

And increasing in :

Find all increasing bivariate functions:

Find all increasing trivariate functions:

Properties & Relations  (4)

An expression is a tautology if it is true for all variable assignments:

TautologyQ[f] is equivalent to ¬SatisfiableQ[¬f]:

An expression of variables is a tautology if the SatisfiabilityCount is :

Use TrueQ to test whether an expression is explicitly identical to True:

Introduced in 2008