Show simple item record

dc.contributor.authorTveretina, Olga
dc.contributor.authorWesselink, Wieger
dc.date.accessioned2013-01-15T17:29:01Z
dc.date.available2013-01-15T17:29:01Z
dc.date.issued2009
dc.identifier.citationTveretina , O & Wesselink , W 2009 , EufDpll - A Tool to Check Satisfiability of Equality Logic Formulas . in Procs of the Irish Conference on the Mathematical Foundations of Computer Science and Information Technology . vol. 225 , Electronic Notes in Theoretical Computer Science , pp. 405-420 . https://doi.org/10.1016/j.entcs.2008.12.089
dc.identifier.otherPURE: 1303104
dc.identifier.otherPURE UUID: c7c90226-f134-48cb-86c4-da4c2dd37af0
dc.identifier.otherScopus: 58149305574
dc.identifier.urihttp://hdl.handle.net/2299/9667
dc.description.abstractDecision procedures for subsets of First-Order Logic form the core of many verification tools. Applications include hardware and software verification. The logic of Equality with Uninterpreted Functions (EUF) is a decidable subset of First-Order Logic. The EUF logic and its extensions have been applied for proving equivalence between systems. We present a branch and bound decision procedure for EUF logic based on the generalisation of the Davis-Putnam-Loveland-Logemann procedure (EUF-DPLL). EufDpll is a tool to check satisfiability of EUF formulas based on this procedure.en
dc.language.isoeng
dc.publisherElectronic Notes in Theoretical Computer Science
dc.relation.ispartofProcs of the Irish Conference on the Mathematical Foundations of Computer Science and Information Technology
dc.subjectEquality logic with uninterpreted functions, satisfiability, DPLL procedure
dc.titleEufDpll - A Tool to Check Satisfiability of Equality Logic Formulasen
dc.contributor.institutionSchool of Computer Science
dc.contributor.institutionScience & Technology Research Institute
dc.identifier.urlhttp://www.scopus.com/inward/record.url?scp=58149305574&partnerID=8YFLogxK
rioxxterms.versionVoR
rioxxterms.versionofrecordhttps://doi.org/10.1016/j.entcs.2008.12.089
rioxxterms.typeOther
herts.preservation.rarelyaccessedtrue


Files in this item

FilesSizeFormatView

There are no files associated with this item.

This item appears in the following Collection(s)

Show simple item record