Argument validity checker: premises, conclusion, counterexample or proof

Enter premises and a conclusion and find out whether the conclusion follows. If it does not, the tool gives the counterexample: an assignment that makes every premise true and the conclusion false.

Everything runs in your browser; nothing is sent anywhere.

Premises (one per line)A -> B BConclusionA

Run

An argument is valid when no assignment makes all its premises true and its conclusion false. The checker asks exactly that question with the engine's exact methods, and answers with a verdict, the method, and, for an invalid argument, the counterexample replayed through the evaluator with the value of each premise and of the conclusion. It also asks whether the premises can all be true together, because an argument with inconsistent premises is valid for a bad reason: it has no case to fail on.

That second check is what separates this tool from a plain validity test. A result that holds only because the premises contradict each other is labelled vacuous, never shown as an unqualified success, following the product's rule that a vacuous truth carries a warning.

Write one premise per line in the engine's notation (A -> B for if A then B, NOT, AND, OR, <->), and the conclusion in the last field. The classic forms (modus ponens, modus tollens, hypothetical and disjunctive syllogism, constructive dilemma) and the classic fallacies (affirming the consequent, denying the antecedent) are worked examples on this site.

Limits

• Truth tables up to 12 inputs (4096 rows).
• Karnaugh maps up to 4 effective variables.
• Normal forms up to 4096 terms; expressions up to 20000 characters and 64 inputs.

How to write expressions

Write inputs as names (member, A, credit_ok) and combine them with AND, OR, NOT, XOR, -> (implies), <-> (if and only if), NAND(a, b), NOR(a, b), XNOR(a, b), or the symbols &&, ||, !, ∧, ∨, ¬, ·, +, ′. Minterm and maxterm forms work too: Σm(A, B, C; 1, 3), ΠM(A, B; 0). Precedence: NOT, then AND, then XOR, then OR, then ->, then <->; use parentheses to be explicit. =, ==, ^, &, | and ~ are rejected with a repair.

Example

Questions

Does validity mean the conclusion is true?

No. Validity is about the form: whenever the premises are true, the conclusion is true. Whether the premises are actually true is soundness, which no tool can decide about the world. The glossary has both terms.

Can it handle quantifiers (all, some)?

No. The engine covers propositional logic and two-valued Boolean algebra. Arguments that need predicates and quantifiers are outside its scope, and the page says so rather than approximating them.

Related

Tools

• Truth table generator: any Boolean expression, up to 12 variables, with intermediate columns
• Boolean algebra calculator and simplifier with steps (every law named and verified)
• Karnaugh map solver: 2 to 4 variables, groups, SOP and POS, don’t-cares from assumptions
• CNF and DNF converter: conjunctive and disjunctive normal forms, minterms and maxterms
• NAND-only and NOR-only converter with equivalence proof
• Logical equivalence checker: two expressions, exact verdict, counterexample
• Logic circuit generator: Boolean expression to gate diagram (SVG)
• Boolean expression to Python, SQL, SMT-LIB and LaTeX

Practice

• Argument validity exercises with answers

Tools

• Truth table generator: any Boolean expression, up to 12 variables, with intermediate columns
• Boolean algebra calculator and simplifier with steps (every law named and verified)
• Karnaugh map solver: 2 to 4 variables, groups, SOP and POS, don’t-cares from assumptions
• CNF and DNF converter: conjunctive and disjunctive normal forms, minterms and maxterms

Generated from the Tangibool engine, semantics tangibool-semantics/1, engine 1.0.0, build 2026-11-07. Every table, map, simplification and verdict on these pages was computed by the Tangibool engine when the site was built, and every claim was re-checked by the same exact checker the app uses. Limits are stated where they apply. © 2026 Foreranger LTD.