An improved BDD method for intuitionistic propositional logic: BDDIntKt system description

Rajeev Goré, Jimmy Thomson

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    2 Citations (Scopus)

    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.

    Original languageEnglish
    Title of host publicationCADE 2013 - 24th International Conference on Automated Deduction, Proceedings
    Pages275-281
    Number of pages7
    DOIs
    Publication statusPublished - 2013
    Event24th International Conference on Automated Deduction, CADE 2013 - Lake Placid, NY, United States
    Duration: 9 Jun 201314 Jun 2013

    Publication series

    NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Volume7898 LNAI
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference24th International Conference on Automated Deduction, CADE 2013
    Country/TerritoryUnited States
    CityLake Placid, NY
    Period9/06/1314/06/13

    Fingerprint

    Dive into the research topics of 'An improved BDD method for intuitionistic propositional logic: BDDIntKt system description'. Together they form a unique fingerprint.

    Cite this