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

Rajeev Goré; Jimmy Thomson

doi:10.1007/978-3-642-38574-2_19

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

Rajeev Goré, Jimmy Thomson

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › peer-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 language	English
Title of host publication	CADE 2013 - 24th International Conference on Automated Deduction, Proceedings
Pages	275-281
Number of pages	7
DOIs	https://doi.org/10.1007/978-3-642-38574-2_19
Publication status	Published - 2013
Event	24th International Conference on Automated Deduction, CADE 2013 - Lake Placid, NY, United States Duration: 9 Jun 2013 → 14 Jun 2013

Publication series

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

Conference

Conference	24th International Conference on Automated Deduction, CADE 2013
Country/Territory	United States
City	Lake Placid, NY
Period	9/06/13 → 14/06/13

Access to Document

10.1007/978-3-642-38574-2_19

Cite this

Goré, R., & Thomson, J. (2013). An improved BDD method for intuitionistic propositional logic: BDDIntKt system description. In CADE 2013 - 24th International Conference on Automated Deduction, Proceedings (pp. 275-281). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7898 LNAI). https://doi.org/10.1007/978-3-642-38574-2_19

@inproceedings{752b9e2fe5134d80acc4d92b3d274e0d,

title = "An improved BDD method for intuitionistic propositional logic: BDDIntKt system description",

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.",

author = "Rajeev Gor{\'e} and Jimmy Thomson",

year = "2013",

doi = "10.1007/978-3-642-38574-2\_19",

language = "English",

isbn = "9783642385735",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "275--281",

booktitle = "CADE 2013 - 24th International Conference on Automated Deduction, Proceedings",

note = "24th International Conference on Automated Deduction, CADE 2013 ; Conference date: 09-06-2013 Through 14-06-2013",

}

Goré, R & Thomson, J 2013, An improved BDD method for intuitionistic propositional logic: BDDIntKt system description. in CADE 2013 - 24th International Conference on Automated Deduction, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7898 LNAI, pp. 275-281, 24th International Conference on Automated Deduction, CADE 2013, Lake Placid, NY, United States, 9/06/13. https://doi.org/10.1007/978-3-642-38574-2_19

An improved BDD method for intuitionistic propositional logic: BDDIntKt system description. / Goré, Rajeev; Thomson, Jimmy.
CADE 2013 - 24th International Conference on Automated Deduction, Proceedings. 2013. p. 275-281 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7898 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › peer-review

TY - GEN

T1 - An improved BDD method for intuitionistic propositional logic

T2 - 24th International Conference on Automated Deduction, CADE 2013

AU - Goré, Rajeev

AU - Thomson, Jimmy

PY - 2013

Y1 - 2013

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84879921023&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-38574-2_19

DO - 10.1007/978-3-642-38574-2_19

M3 - Conference Paper

SN - 9783642385735

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 275

EP - 281

BT - CADE 2013 - 24th International Conference on Automated Deduction, Proceedings

Y2 - 9 June 2013 through 14 June 2013

ER -

Goré R, Thomson J. An improved BDD method for intuitionistic propositional logic: BDDIntKt system description. In CADE 2013 - 24th International Conference on Automated Deduction, Proceedings. 2013. p. 275-281. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-38574-2_19

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

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this