PV4 Barcelogicproduces a satisfiability result for a formula

Application domain/field

SMT solving

Type of tool

SMT solver

Expected input

SMT formula

Format:

SMT-LIB format

Expected output

If satisfiable, then a model (in SMT-LIB format) which describes the truth value for each Boolean variable, a concrete integer or real for each numeric variable and a partial mapping for each uninterpreted function symbol in the formula Else, unsatisfiable
SMT

Links

Related papers

https://doi.org/10.1007/978-3-540-70545-1_27

Last publication date

2008

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.