An improved BDD method for Intuitionistic Propositional Logic: BDDIntKt System Description

Jimmy Thomson (ANU)

LOGIC AND COMPUTATION SEMINAR

DATE: 2013-06-04
TIME: 14:30:00 - 15: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 previously presented a decision procedure for satisfiability and validity in propositional intuitionistic logic Int using Binary Decision Diagrams (BDDs). We now present some further optimisations which greatly improve performance. Primarily we focus on the impact and placement of an explicit mechanism for BDD variable ordering.