Show simple item record

dc.contributor.authorTveretina, Olga
dc.date.accessioned2015-04-27T09:04:01Z
dc.date.available2015-04-27T09:04:01Z
dc.date.issued2004
dc.identifier.citationTveretina , O 2004 , A Decision Procedure for Equality Logic with Uninterpreted Functions . in Artificial Intelligence and Symbolic Computation . Lecture Notes in Computer Science , vol. 3249 , Springer Nature , pp. 66-79 , AISC 2004, 7th Int Conf , Linz , Austria , 22/09/04 . https://doi.org/10.1007/978-3-540-30210-0_7
dc.identifier.citationconference
dc.identifier.isbn978-3-540-23212-4
dc.identifier.isbn978-3-540-30210-0
dc.identifier.otherPURE: 1302920
dc.identifier.otherPURE UUID: 2747463a-cf8e-4e0e-bebb-f72da586f435
dc.identifier.otherScopus: 26844437239
dc.identifier.urihttp://hdl.handle.net/2299/15835
dc.description.abstractThe equality logic with uninterpreted functions (EUF) has been proposed for processor verification. A procedure for proving satisfiability of formulas in this logic is introduced. Since it is based on the DPLL method, the procedure can adopt its heuristics. Therefore the procedure can be used as a basis for efficient implementations of satisfiability checkers for EUF. A part of the introduced method is a technique for reducing the size of formulas, which can also be used as a preprocessing step in other approaches for checking satisfiability of EUF formulasen
dc.language.isoeng
dc.publisherSpringer Nature
dc.relation.ispartofArtificial Intelligence and Symbolic Computation
dc.relation.ispartofseriesLecture Notes in Computer Science
dc.titleA Decision Procedure for Equality Logic with Uninterpreted Functionsen
dc.contributor.institutionSchool of Physics, Engineering & Computer Science
rioxxterms.versionofrecordhttps://doi.org/10.1007/978-3-540-30210-0_7
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