Implementing tableau calculi using BDDs: BDDtab system description

Simple item page
dc.contributor.authorGore, Rajeev
dc.contributor.authorOlesen, Kerry
dc.contributor.authorThomson, James
dc.coverage.spatialVienna Austria
dc.date.accessioned2015-12-13T22:29:17Z
dc.date.createdJuly 19-22 2014
dc.date.issued2014
dc.date.updated2015-12-11T08:47:48Z
dc.description.abstractWe present a modification of the DPLL-based approach to decide modal satisfiability where we substitute DPLL by BDDs. We demonstrate our method by implementing the standard tableau calculi for automated reasoning in propositional modal logics K and S4, along with extensions to the multiple modalities of. We evaluate our implementation of such a reasoner using several K and S4 benchmark sets, as well as some ontologies. We show, with comparison to FaCT++, InKreSAT and SAT, that it can compete with other state of the art methods of reasoning in propositional modal logic. We also discuss how this technique extends to tableau for other propositional logics.
dc.identifier.isbn9783319085869
dc.identifier.urihttp://hdl.handle.net/1885/74624
dc.publisherSpringer Verlag
dc.relation.ispartofseries7th International Joint Conference on Automated Reasoning, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014
dc.sourceLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
dc.source.urihttp://link.springer.com/book/10.1007/978-3-319-08587-6
dc.titleImplementing tableau calculi using BDDs: BDDtab system description
dc.typeConference paper
local.bibliographicCitation.lastpage343
local.bibliographicCitation.startpage337
local.contributor.affiliationGore, Rajeev, College of Engineering and Computer Science, ANU
local.contributor.affiliationOlesen, Kerry, College of Engineering and Computer Science, ANU
local.contributor.affiliationThomson, James, College of Engineering and Computer Science, ANU
local.contributor.authoremailu9409448@anu.edu.au
local.contributor.authoruidGore, Rajeev, u9409448
local.contributor.authoruidOlesen, Kerry, u5162413
local.contributor.authoruidThomson, James, u4308348
local.description.embargo2037-12-31
local.description.notesImported from ARIES
local.description.refereedYes
local.identifier.absfor080200 - COMPUTATION THEORY AND MATHEMATICS
local.identifier.absfor010100 - PURE MATHEMATICS
local.identifier.ariespublicationU3488905xPUB4212
local.identifier.doi10.1007/978-3-319-08587-6_25
local.identifier.scopusID2-s2.0-84904818749
local.identifier.uidSubmittedByU3488905
local.type.statusPublished Version

Downloads

Original bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
01_Gore_Implementing_tableau_calculi_2014.pdf
Size:
197.81 KB
Format:
Adobe Portable Document Format
Download

Collections

ANU Research Publications

DSpace software copyright © 2002-2024 LYRASIS