Mon, 2007-05-07 20:50 — pietro
==Background==
Tableau calculi are now routinely used to determine whether or not a particular statement A is a logical consequence of another collection of statements Gamma in some (non-classical) logic L. Such provers have applications in Hardware Verification, Artificial Intelligence and Hybrid Systems. Tableau calculi (and sequent calculi) can be efficiently automated for a broad range of logics.