BDD-based Automated Reasoning for Propositional Bi-Intuitionistic Tense Logics
James Thomson (ANU)
LOGIC AND COMPUTATION SEMINARDATE: 2012-06-19
TIME: 15:30:00 - 16:00:00
LOCATION: RSISE Seminar Room, ground floor, building 115, cnr. North and Daley Roads, ANU
CONTACT: JavaScript must be enabled to display this email address.
ABSTRACT:
We give Binary Decision Diagram (BDD) based methods for deciding validity and satisfiability of propositional Intuitionistic Logic and Bi-intuitionistic Tense Logic (BiKt). We handle intuitionistic implication and bi-intuitionistic exclusion by treating them as modalities, but the move to an intuitionistic basis requires careful analysis for handling the reflexivity, transitivity and antisymmetry of the underlying Kripke relation. BiKt requires a further extension to handle the interactions between the intuitionistic and modal binary relations, and their converses. We explain our methodology for using the Kripke semantics of these logics to constrain the underlying least and greatest fixpoint approaches of the finite model construction. With some optimisations this technique is competitive with the state of the art theorem provers for Intuitionistic Logic using the ILTP benchmark and randomly generated formulae.
BIO:
