\documentclass[11pt,a4paper]{article}
\usepackage[margin=2.5cm]{geometry}
\usepackage{amssymb}
\usepackage{booktabs}
\usepackage{boolalg}

\title{\texttt{boolalg}: Boolean Logic Truth Tables,\\Simplification, and Algebraic Proofs}
\author{Param Srivastava}
\date{Version 1.0.0 --- October 22, 2026}

\begin{document}
\maketitle

\section{Overview}
The \texttt{boolalg} package provides pure-\LaTeX{} macros for generating truth tables, simplifying Boolean expressions step-by-step, and proving algebraic equivalence (or finding counterexamples) directly in your document without external scripts or shell-escape.

\section{Commands}
\begin{itemize}
  \item \verb|\btable{<expr>}| --- Truth table with intermediate sub-expression columns (aliases: \verb|\btruth|, \verb|\truthtable|, \verb|\btruthtable|, \verb|\booltruthtable|).
  \item \verb|\btable*{<expr>}| --- Truth table followed by the simplified expression.
  \item \verb|\bsimplify{<expr>}| --- Step-by-step algebraic simplification with law justifications (alias: \verb|\boolsimplify|).
  \item \verb|\bsimplify*{<expr>}| --- Final simplified expression only.
  \item \verb|\bprove{<lhs> = <rhs>}| --- Step-by-step algebraic proof or counterexample (alias: \verb|\boolprove|).
\end{itemize}

\section{Input Syntax}
Operators are listed from highest to lowest precedence:
\begin{center}
\begin{tabular}{@{}lll@{}}
\toprule
\textbf{Precedence} & \textbf{Operator} & \textbf{Accepted Input Syntax} \\
\midrule
Highest & Grouping & \texttt{( ... )} \\
        & Variables / Constants & \texttt{A--Z}, \texttt{a--z}, \texttt{0}, \texttt{1} \\
1 & NOT & \verb|not|, \verb|\not|, \verb|\lnot|, \verb|\neg|, \verb|'|\ (postfix), \verb|!|, \verb|~| \\
2 & AND & Implicit (\verb|AB|), \verb|*|, \verb|.|, \verb|&|, \verb|and|, \verb|\and|, \verb|\land|, \verb|\wedge|, \verb|\cdot| \\
  & NAND & \verb|nand|, \verb|\nand|, \verb|\uparrow|, \verb|\barwedge| \\
3 & OR & \verb|+|, \verb|||, \verb|or|, \verb|\or|, \verb|\lor|, \verb|\vee| \\
  & NOR & \verb|nor|, \verb|\nor|, \verb|\downarrow| \\
4 & XOR & \verb|^|, \verb|xor|, \verb|\xor|, \verb|\oplus|, \verb|\veebar| \\
  & XNOR & \verb|xnor|, \verb|\xnor|, \verb|\odot|, \verb|\equiv|, \verb|\leftrightarrow|, \verb|\iff| \\
\bottomrule
\end{tabular}
\end{center}

\begin{center}
\emph{Note: Place a space after word operators (e.g., \texttt{not A}, \texttt{A and B}).}
\end{center}

\section{Configuration}
You can customize output symbols and parameters using standard \verb|\def|:
\begin{verbatim}
\def\boolfname{f}          % Name of the truth table output column (\empty to hide)
\def\booltablemaxvars{5}   % Maximum number of variables before table is omitted
\def\boolandsym{\land}     % Display symbol for AND
\def\boolorsym{\lor}       % Display symbol for OR
\def\boolnotsym{\lnot}     % Display symbol for NOT
\def\boolxorsym{\oplus}    % Display symbol for XOR
\def\boolxnorsym{\odot}    % Display symbol for XNOR
\def\boolnandsym{\uparrow} % Display symbol for NAND
\def\boolnorsym{\downarrow}% Display symbol for NOR
\end{verbatim}

\section{Examples}

\subsection{Truth Table with Simplification}
\begin{verbatim}
\btable*{A'B + AB'}
\end{verbatim}
\btable*{A'B + AB'}

\subsection{Step-by-Step Simplification}
\begin{verbatim}
\bsimplify{(A + B)(A + B')}
\end{verbatim}
\bsimplify{(A + B)(A + B')}

\subsection{Algebraic Equivalence Proof}
\begin{verbatim}
\bprove{A \oplus B = (A + B)(AB)'}
\end{verbatim}
\bprove{A \oplus B = (A + B)(AB)'}

\subsection{Counterexample Generation for Non-Equivalent Expressions}
\begin{verbatim}
\bprove{A + B = AB}
\end{verbatim}
\bprove{A + B = AB}

\end{document}