dsh-boolean

Boolean algebra toolbox for DeepSeek Harness (dsh). Parse propositional-logic expressions and get full truth tables with minterm/maxterm summaries, canonical DNF/CNF, a minimized sum of products (with don't-cares), NNF, and NAND-only / NOR-only gate networks — no hand-drawn 16-row tables, no De Morgan slips, no hand-run Karnaugh maps.

Zero runtime dependencies, pure local math.

Why

Modeled reasoning often derails on small logic chores: expanding ¬(a∧b), listing the satisfying rows of a 3-variable expression, or checking whether two formulas say the same thing. These tools do the bookkeeping exactly, one expression at a time.

Install

dsh plugin --profile web add github:TYEclipse/dsh-boolean

Restart the profile session (or start a new one) and the six tools are registered under tools for every agent. Requires pnpm on PATH (the plugin host resolves it).

Tools

Tool	What it does
truth_table	Enumerates every assignment row (up to 8 variables / 256 rows) with the result, minterm & maxterm indices, tautology / contradiction / satisfiability flags, and canonical DNF and CNF strings.
logic_eval	Evaluates an expression under one complete assignment (trueVars / falseVars); missing variables are reported, never silently defaulted.
logic_equiv	Compares two expressions over all rows of the combined table; reports how many rows differ and one concrete counterexample when they are not equivalent.
logic_convert	Converts an expression to nnf, dnf, cnf, nand, or nor canonical form. DNF/CNF come from the truth table (8-variable cap); nnf/nand/nor are structural rewrites without a cap.
logic_minimize	Minimizes to a sum of products (Quine–McCluskey): prime implicants, essential ones, and a cover of minimum term count (ties broken by fewest literals, then reading order). Optional dontCare minterm indices replace a hand-run Karnaugh map. It also names the terms that form the returned cover (coverTerms), in answer order.
logic_kmap	Lays the function out as a Karnaugh map (1–4 variables, Gray-coded axes, cells 1/x/0) and maps every term of the minimal cover back to the cells it circles — each group reports its row/col/minterm cells, whether it is essential, and whether it wraps around an edge.

Expression syntax

Meaning	Symbols	Words	Unicode
NOT (prefix)	!	not	¬
AND	&	and	∧
XOR	^	xor	⊕
OR	|	or	∨
IMPLIES	-> =>	implies	→
IFF	<-> <=>	iff	↔

• Variables are single letters a–z (upper case is normalized); parentheses () group.
• Precedence, high to low: NOT → AND → XOR → OR → IMPLIES → IFF.
• Binary operators are left-associative; parenthesize chains of -> / <-> when in doubt.
• XOR, IMPLIES and IFF are desugared at parse time to NOT/AND/OR with the textbook identities (a^b ≡ (a&!b)|(!a&b), a->b ≡ !a|b, a<->b ≡ (a&b)|(!a&!b)).
• Expressions are limited to 512 characters; truth-table enumeration to 8 variables.

Examples

All outputs below are real tool output (v0.1.0).

Truth table of XOR — every row plus the canonical forms:

truth_table { expr: "a ^ b" }
→ rows: m0(00)=0, m1(01)=1, m2(10)=1, m3(11)=0
  minterms [1,2]  DNF = (!a & b) | (a & !b)
  maxterms [0,3]  CNF = (a | b) & (!a | !b)

Check one row instead of the whole table:

logic_eval { expr: "a -> (b | c)", trueVars: ["a"], falseVars: ["b","c"] }
→ a -> (b | c) with a=true, b=false, c=false = false

Verify a rewrite identity (De Morgan):

logic_equiv { exprA: "!(a | b)", exprB: "!a & !b" }
→ equivalent: !(a | b) == !a & !b (all 4 rows agree)

Push negations down or build single-gate networks:

logic_convert { expr: "!(a & b)", operation: "nnf" } → !a | !b
logic_convert { expr: "a & b",   operation: "nand" } → NAND(NAND(a,b),NAND(a,b))
logic_convert { expr: "a | b",   operation: "nor"  } → NOR(NOR(a,b),NOR(a,b))
logic_convert { expr: "a -> b",  operation: "dnf"  } → (!a & !b) | (!a & b) | (a & b)

Invalid input is reported with a position and a reason instead of a wrong answer: a & → unexpected end of expression (at position 3); foo & a → variables must be single letters a–z.

Minimize — the smallest sum of products, plus prime implicants and essentials:

logic_minimize { expr: "((a & b) | (a & c)) | (b & c)" }
→ a & b | a & c | b & c   (3 terms, 6 literals, proven minimum, unique)
  prime implicants: a & b m[6, 7]; a & c m[5, 7]; b & c m[3, 7]

Don't-cares are the Karnaugh-map move: mark rows you don't care about and the cover grows past them.

logic_minimize { expr: "a & !b & c | a & !b & !c", dontCare: [6, 7] }
→ a   (1 term, 1 literal; the prime implicant covers m[4,5] and the don't-cares dc[6,7])

Ties are resolved deterministically (fewest terms, then fewest literals, then reading order) and the result says so instead of pretending there is only one answer:

logic_minimize { expr: "a & (b | c)", dontCare: [1, 2] }
→ a & b | a & c   (proven minimum, a tie was resolved — three 2-term covers exist)

logic_kmap draws the same reasoning as a map and says which cells each term circles:

logic_kmap { expr: "a & !b | a & c" }
→ K-map of a & !b | a & c over 3 variable(s) (rows a | cols b, c)
      00 01 11 10
  0 |  0  0  0  0
  1 |  1  1  1  0
  minimal cover: a & !b | a & c
    a & !b: 2 cell(s) — r1c0(m4) r1c1(m5) [essential, contiguous]
    a & c: 2 cell(s) — r1c1(m5) r1c2(m7) [essential, contiguous]

Don't-care cells show up as x and groups are allowed to circle them:

logic_kmap { expr: "a & !b & c | a & !b & !c", dontCare: [6, 7] }
→ 1 |  1  1  x  x   minimal cover: a
    a: 4 cell(s) — r1c0(m4) r1c1(m5) r1c3(m6) r1c2(m7)

A group that leaves one edge and re-enters on the opposite one is marked wraps an edge — that is why !c over three variables is still a single 4-cell group.

Notes & limits

• Truth-table tools cap at 8 variables (256 rows); nnf/nand/nor conversions are structural and unlimited.
• logic_eval needs every expression variable in exactly one of trueVars / falseVars; listing a variable in both, or a variable name outside a–z, is an error.
• Gate outputs use function-call syntax: NAND(a,b) / NOR(a,b), with NOT(x) written as NAND(x,x) or NOR(x,x). Input grammar does not accept gate names — convert, don't write gates.
• Canonical DNF of a contradiction and canonical CNF of a tautology are the empty string, with an explanatory note.
• logic_minimize returns "" for a function that is false on every row and 1 when the cover is the constant 1. The search is exhaustive with a node budget; in the (rare) case the budget is hit, the result is flagged exact: false and the cover is essentials + greedy rather than claimed minimal. Ties are resolved by fewest terms, then fewest literals, then reading order, so the same input always yields the same string.
• logic_kmap lays out at most 4 variables (a 5+ variable map is not a readable grid) and says so instead of truncating; use logic_minimize for wider functions. Its groups are exactly the terms of the returned cover, not every prime implicant.

Development

pnpm install
pnpm build      # tsc -> dist/ (committed: git installs do not build)
pnpm test       # 144 tests: parser semantics, oracle-anchored tables (independent Python
                # enumeration), minimization, gate networks, schema guards, lossless-JSON discipline
pnpm lint       # oxlint src test
python3 test/oracle/anchors.py --check   # re-verify the oracle's own anchors

Test anchors are generated by an independent Python oracle (test/oracle/anchors.py): itertools truth enumeration for the fixture, and an exhaustive set-cover search over all cubes in {0,1,-}^n for minimization — no Quine–McCluskey code is shared with the plugin, so agreement between oracle and implementation is evidence rather than a tautology. Every DNF/CNF string, truth row, minimized cover, prime-implicant list and uniqueness flag in the tests is printed by that oracle (regenerate the fixture with python3 test/oracle/anchors.py --write-fixture).

License

MIT — see LICENSE.