README

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