Logic Tools

Browse all available logic tools.

Available tools

A Proposition Universal Affirmative Quantity-Quality Classifier Recognize an A proposition represented as all subject members satisfying an unnegated predicate.
Absorption Law Simplifier (P∨(P∧Q)=P) Simplify either classical absorption-law form for two identifier atoms.
Addition Rule Step Validator (P ⊢ P∨Q) Validate disjunction introduction when the affirmed premise is one of the claimed disjunction operands.
Affirming the Consequent Fallacy Flag Detector Detect the affirming-the-consequent pattern with distinct identifier atoms.
Associativity Regrouping Legality Checker Classical pure Boolean associate identity witness for AND/OR; not short-circuit side-effect equivalence or arbitrary programming operator.
Barbara AAA-1 Valid Form Lookup Check Barbara (AAA-1) under explicit nonempty-term assumptions using classical categorical semantics.
Baroco AOO-2 Valid Form Lookup Check Baroco (AOO-2) under explicit nonempty-term assumptions using classical categorical semantics.
Bocardo OAO-3 Valid Form Lookup Check Bocardo (OAO-3) under explicit nonempty-term assumptions using classical categorical semantics.
Bramantip AAI-4 Fourth Figure Valid Lookup Check Bramantip (AAI-4) under explicit nonempty-term assumptions using classical categorical semantics.
Camenes AEE-4 Valid Form Lookup Check Camenes (AEE-4) under explicit nonempty-term assumptions using classical categorical semantics.
Camestres AEE-2 Valid Form Lookup Check Camestres (AEE-2) under explicit nonempty-term assumptions using classical categorical semantics.
Categorical Syllogism Mood-Figure Label Parser (EAE-1 etc.) Parse a categorical mood and figure such as AAA-1 into proposition kinds and standard S, M, and P term positions.
Celarent EAE-1 Valid Form Lookup Check Celarent (EAE-1) under explicit nonempty-term assumptions using classical categorical semantics.
Cesare EAE-2 Valid Form Lookup Check Cesare (EAE-2) under explicit nonempty-term assumptions using classical categorical semantics.
Commutativity Applicability Checker for AND/OR Classical pure Boolean commute identity witness for AND/OR; not short-circuit side-effect equivalence or arbitrary programming operator.
Complement Law Contradiction Tautology Pair Checker Check for complementary signed identifier literals and apply their conjunction or disjunction law.
Conditional Proof Assumption Discharge Depth Tracker Track nested begin(+1), neutral(0), discharge(-1) assumption events; not a validation of formulas or implication-introduction proof.
Conjunction Introduction Step Validator (P,Q ⊢ P∧Q) Validate conjunction introduction by matching its two affirmed identifier premises with the claimed conjunction.
Conjunctive Normal Form CNF Conversion Steps Counter Bounded classical propositional !,&,| parser/NNF/CNF conversion; counts distributive Cartesian merge events, not a universal proof-step metric; <=256 clauses, <=4096 literals.
Constructive Dilemma Step Validator Validate constructive dilemma by matching two conditionals, the disjunction of antecedents, and the disjunction of consequents.
Contingency Mixed-Outcome Classifier Classify a complete ordered Boolean truth column as a tautology, contradiction, or contingency.
Contradiction All-Rows-False Checker Check whether every row in a complete ordered Boolean truth column is false.
Contraposition Immediate Inference Full Transform Validator (A,O valid) Form full contraposition by swapping and complementing both categorical terms and test its validity.
Contrapositive Form Generator (P→Q ≡ ¬Q→¬P) Generate the equivalent contrapositive of a conditional between identifier atoms.
Converse Statement Generator with Validity Warning Generate a conditional converse and determine whether it is equivalent for the supplied identifier atoms.
Conversion Immediate Inference Subject-Predicate Swapper (E,I valid) Swap subject and predicate by simple conversion and test whether that conversion preserves truth for identifier categories.
Darapti AAI-3 Third Figure Valid Lookup Check Darapti (AAI-3) under explicit nonempty-term assumptions using classical categorical semantics.
Darii AII-1 Valid Form Lookup Check Darii (AII-1) under explicit nonempty-term assumptions using classical categorical semantics.
Datisi AII-3 Valid Form Lookup Check Datisi (AII-3) under explicit nonempty-term assumptions using classical categorical semantics.
De Morgan AND-to-OR Negation Transformer Rewrite a negated conjunction of two identifier atoms using ! for negation and || for disjunction.
De Morgan OR-to-AND Negation Transformer Rewrite a negated disjunction of two identifier atoms using ! for negation and && for conjunction.
Denying the Antecedent Fallacy Flag Detector Detect the denying-the-antecedent pattern with distinct identifier atoms and explicitly negated terms.
Dimaris IAI-4 Valid Form Lookup Check Dimaris (IAI-4) under explicit nonempty-term assumptions using classical categorical semantics.
Disamis IAI-3 Valid Form Lookup Check Disamis (IAI-3) under explicit nonempty-term assumptions using classical categorical semantics.
Disjunctive Syllogism Validator (P∨Q, ¬P ⊢ Q) Validate disjunctive syllogism by matching a disjunction, a negated operand, and the remaining conclusion atom.
Distributivity AND-over-OR Expansion Applier Distribute conjunction over disjunction for three identifier atoms.
Distributivity OR-over-AND Expansion Applier Distribute disjunction over conjunction for three identifier atoms.
Domination Law Annihilator Checker (P∨T=T, P∧F=F) Check whether a Boolean constant is the annihilator of conjunction or disjunction.
Don't-Care X Cell Count Flexibility Note Generator Count explicitly supplied dont-care cells and 2^X independent assignments; no minimization or arbitrary hardware validity.
Double Negation Elimination Validator (¬¬P ⊢ P) Validate double-negation elimination from an explicitly double-negated identifier to a claimed atom.
E Proposition Universal Negative Classifier Recognize an E proposition represented as all subject members satisfying a negated predicate.
Existential Generalization EG Step Validator (P(a) ⊢ ∃x P(x)) Check exact existential generalization unary atomic notation against an explicitly declared premise template; no arbitrary formula substitution/capture or proof context inference.
Existential Import Modern Invalidity Flag for AA-3 Identify categorical syllogisms that become valid only when nonempty terms are assumed.
Existential Instantiation EI Fresh Name Constraint Checker Fresh witness-name check against explicit full caller constant inventory; scope/discharge and full existential-elimination side conditions not verified.
Felapton EAO-3 Valid Form Lookup Check Felapton (EAO-3) under explicit nonempty-term assumptions using classical categorical semantics.
Ferio EIO-1 Valid Form Lookup Check Ferio (EIO-1) under explicit nonempty-term assumptions using classical categorical semantics.
Ferison EIO-3 Valid Form Lookup Check Ferison (EIO-3) under explicit nonempty-term assumptions using classical categorical semantics.
Festino EIO-2 Valid Form Lookup Check Festino (EIO-2) under explicit nonempty-term assumptions using classical categorical semantics.
Four-Term Fallacy Equivocation Detector Count distinct sense-specific term identifiers in a three-statement argument and flag exactly four terms.
Fresison EIO-4 Valid Form Lookup Check Fresison (EIO-4) under explicit nonempty-term assumptions using classical categorical semantics.
Full Adder Majority Carry Expression Checker Compute the Boolean sum and majority carry bits of a full adder with a carry input.
Full CNF Clause Set Builder from Truth Table Build equivalent canonical CNF clauses from every false truth-table row without auxiliary variables.
Full DNF Minterm List Builder from Truth Table Build canonical DNF minterms and their indices from true rows in binary counting order.
Half Adder Sum Carry Boolean Pair Checker Compute the Boolean sum and carry bits of a half adder.
Hypothetical Syllogism Chain Validator (P→Q, Q→R ⊢ P→R) Validate a hypothetical syllogism by matching two conditional links and the claimed endpoint conditional.
I Proposition Particular Affirmative Classifier Recognize an I proposition represented as some subject member satisfying an unnegated predicate.
Idempotence Duplicate Term Collapser Checker (P∧P=P) Collapse equal identifier operands under conjunction or disjunction using idempotence.
Identity Law Neutral Element Checker (P∧T, P∨F) Check whether a Boolean constant is the identity element of conjunction or disjunction.
Illicit Major Fallacy Detector Detect a major term distributed in a categorical conclusion but undistributed in its major premise.
Illicit Minor Fallacy Detector Detect a minor term distributed in a categorical conclusion but undistributed in its minor premise.
Indirect Proof Negated Goal Assumption Validator Check an atomic classical indirect-proof initial assumption against negated goal; does not establish contradiction or validate proof completion.
Inverse Statement Generator with Validity Warning Generate a conditional inverse and determine whether it is equivalent for the supplied identifier atoms.
Involution Double Complement Cancel Checker Cancel pairs of nested negations around an identifier atom using classical involution.
Karnaugh Gray Code Row Column Order Generator Binary-reflected Gray-code row/column order for a caller K-map dimension up to four bits per axis; does not minimize expressions.
Karnaugh Map Cell Count Grid Size Resolver Return the cell count and balanced row and column dimensions of a binary Karnaugh map for up to 52 variables.
Law of Non-Contradiction Violation Detector (P∧¬P) Find exact P and !P pairs in explicit classical literal inventory; no natural-language contradiction detection or SAT solving.
Lewis Carroll Sorites Premise Chain Link Counter Inspect explicit ordered universal class-inclusion sorites links; no existential import, natural-language parsing or arbitrary syllogism proof.
Logical Consistency Satisfiable-Assignment Finder Find common satisfying rows of complete premise truth columns encoded as 0/1 strings in the same valuation order.
Logical Contradiction Pair Opposed-Rows Detector Check whether two complete truth columns are exact negations in the same valuation order.
Logical Equivalence Biconditional Row Match Checker Test logical equivalence of two complete truth columns with the same valuation order.
Material Equivalence Expansion Rewriter (P↔Q two forms) Expand material equivalence between identifier atoms into the disjunction of their matching truth states.
Material Implication to Disjunction Rewriter (P→Q ≡ ¬P∨Q) Rewrite material implication between identifier atoms as a disjunction with a negated antecedent.
Maxterm Index Complement Convention Checker Construct a maxterm from a binary row index and check a proposed most-significant-bit negation mask.
Minterm Index Binary Assignment Decoder Decode a minterm index into fixed-width binary bits and the corresponding conjunction of identifier literals.
Modus Ponens Inference Step Validator (P→Q, P ⊢ Q) Validate a modus ponens step using identifier operands for its conditional, affirmed premise, and claimed conclusion.
Modus Tollens Inference Step Validator (P→Q, ¬Q ⊢ ¬P) Validate a modus tollens step by matching the identifiers negated in its premise and conclusion.
NAND-Only Equivalent Circuit Feasibility Checker Bounded NAND gate counts for standard NOT/AND/OR templates with tied inputs and unlimited fanout; logical universality not circuit timing/power feasibility.
NOR-Only Equivalent Circuit Feasibility Checker Bounded NOR gate counts for standard NOT/AND/OR templates with tied inputs and unlimited fanout; logical universality not circuit timing/power feasibility.
O Proposition Particular Negative Classifier Recognize an O proposition represented as some subject member satisfying a negated predicate.
Obversion Immediate Inference Transformer (change quality + complement) Obvert a categorical proposition by changing its quality and complementing its predicate.
Prime Implicant Pair Adjacency Edge Counter Count adjacency edges among supplied binary minterm indices differing in exactly one bit.
Principle of Explosion Ex Falso Quodlibet Derivation Note Generator Explicit classical propositional contradiction/ex-falso premise screen, not validity in paraconsistent logics or truth of real-world claims.
Quantifier Negation Push-Through Rewriter (¬∀→∃¬) Classical quantifier-negation duality for one explicitly declared unary atomic predicate only; not arbitrary capture-avoiding formula parsing.
Quantifier Scope Widening Legality Checker Restricted scope widening for (Qx P) connective R to Qx(P connective R), given caller complete free-variable inventory; preserves empty-domain exceptions.
SAT Formula to CNF Converter Convert a Boolean JSON syntax tree to equisatisfiable CNF clauses with Tseitin auxiliary variables. Supported operators are variable, NOT, AND, OR, and implication; integer literals use negative signs for negation.
Simplification Rule Step Validator (P∧Q ⊢ P) Validate conjunction elimination when the claimed conclusion is one of the premise conjunction operands.
Square of Opposition Contradictory Pair Mapper (A-O, E-I) Map a categorical proposition to its contradictory form for the same subject and predicate.
Square of Opposition Contrary Pair Mapper (A-E) Map an A or E proposition to its contrary and state whether a nonempty subject guarantees the relation.
Square of Opposition Subaltern Implication Mapper (A-I, E-O) Map A to I or E to O and state whether a nonempty subject guarantees universal-to-particular implication.
Square of Opposition Subcontrary Pair Mapper (I-O) Map an I or O proposition to its subcontrary and state whether a nonempty subject guarantees the relation.
Tautology All-Rows-True Checker Check whether every row in a complete ordered Boolean truth column is true.
Truth Table Row Count 2^n Calculator Return the exact number of rows in a truth table with zero through 10,000 propositional variables.
Undistributed Middle Fallacy Detector Detect an undistributed middle term in the two premises of a standard categorical syllogism.
Universal Generalization UG Arbitrary Constant Guard Checker Declared natural-deduction universal-generalization arbitrary-constant side condition; no omitted assumption/free-variable analysis.
Universal Instantiation UI Step Validator (∀x P(x) ⊢ P(a)) Check exact universal instantiation unary atomic notation against an explicitly declared premise template; no arbitrary formula substitution/capture or proof context inference.
Vacuous Truth Empty Domain Universal Checker Classical universal truth from complete finite domain/counterexample counts; empty domain allowed explicitly, no natural-language truth inference.
Venn Diagram Three-Set Region Number Mapper (0-7) Map three Boolean set memberships to a Venn region index and the list of containing sets.
Venn Diagram Two-Set Region Number Mapper (0-3) Map two Boolean set memberships to a Venn region using A as the most significant bit.
XNOR Equality Gate Definition Checker Evaluate XNOR equality and its classical matching-state expansion on two Boolean inputs.
XOR Definition Expansion (¬P∧Q)∨(P∧¬Q) Checker Evaluate XOR and its classical conjunction/disjunction expansion on two Boolean inputs.