| dc.contributor.author | Tveretina, Olga | |
| dc.date.accessioned | 2015-04-27T09:04:01Z | |
| dc.date.available | 2015-04-27T09:04:01Z | |
| dc.date.issued | 2004 | |
| dc.identifier.citation | Tveretina , 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 Link , 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.citation | conference | |
| dc.identifier.isbn | 978-3-540-23212-4 | |
| dc.identifier.isbn | 978-3-540-30210-0 | |
| dc.identifier.uri | http://hdl.handle.net/2299/15835 | |
| dc.description.abstract | The 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 formulas | en |
| dc.language.iso | eng | |
| dc.publisher | Springer Nature Link | |
| dc.relation.ispartof | Artificial Intelligence and Symbolic Computation | |
| dc.relation.ispartofseries | Lecture Notes in Computer Science | |
| dc.title | A Decision Procedure for Equality Logic with Uninterpreted Functions | en |
| dc.contributor.institution | School of Physics, Engineering & Computer Science | |
| dc.contributor.institution | Biocomputation Research Group | |
| dc.contributor.institution | Department of Computer Science | |
| rioxxterms.versionofrecord | 10.1007/978-3-540-30210-0_7 | |
| rioxxterms.type | Other | |
| herts.preservation.rarelyaccessed | true | |
