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 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:

Wolfram Research (2008), TautologyQ, Wolfram Language function, https://reference.wolfram.com/language/ref/TautologyQ.html.

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_2023_tautologyq, author="Wolfram Research", title="{TautologyQ}", year="2008", howpublished="\url{https://reference.wolfram.com/language/ref/TautologyQ.html}", note=[Accessed: 19-March-2024 ]}

BibLaTeX

@online{reference.wolfram_2023_tautologyq, organization={Wolfram Research}, title={TautologyQ}, year={2008}, url={https://reference.wolfram.com/language/ref/TautologyQ.html}, note=[Accessed: 19-March-2024 ]}