Overview -------- This is a simple boolean calculator. It reads a boolean formula and checks whether it is valid. In case '-s' is specified satisfiability is checked instead of validity (tautology). Language -------- The input format has the following syntax in BNF: ( [ ... ] means optional, { ... } means repeated arbitrary many times) expr ::= iff iff ::= implies { '<->' implies } implies ::= or [ '->' or | '<-' or ] or ::= and { '|' and } and ::= not { '&' not } not ::= basic | '!' not basic ::= var | '(' expr ')' and 'var' is a string over letters, digits and the following characters: - _ . [ ] $ @ The last character of 'var' should be different from '-'. Armin Biere, Johannes Kepler University, Thu Nov 22 15:47:00 CET 2012