Student Project

Visualising Proof Trees for the Tableau WorkBench

==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.
Syndicate content