MVL is a theorem-proving shell in
Common Lisp.  It includes first-order logic, ATMSs, default reasoning
and circumscription as special cases.