Name
Abstract | ||
|---|---|---|
The Bernays-Schönfinkel class with Datalog is a 2-variable fragment of the Bernays-Schönfinkel class extended with least fixed points expressible by certain monadic Datalog programs. It was used in a bounded model checking procedure for programs manipulating dynamically allocated pointer structures, where the bounded model checking problem was reduced to the satisfiability of formulas in this logic. The best known upper bound on the complexity of the satisfiability problem for this logic was 2NEXPTIME. In this paper we extend the Bernays-Schönfinkel class with Datalog to a more expressive logic -- a fragment of two-variable logic with counting quantifiers extended with the same kind of fixed points. We prove that both satisfiability and entailment for the new logic are decidable in NEXPTIME and we give a matching lower bound for the original logic, which establishes NEXPTIME-completeness of the satisfiability and entailment problems for both of them. Our algorithm is based on a translation to 2-variable logic with counting quantifiers. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/978-3-642-16242-8_14 | LPAR (Yogyakarta) |
Keywords | Field | DocType |
satisfiability problem,2-variable fragment,two-variable logic,2-variable logic,nfinkel class,new logic,expressive logic,bounded model checking problem,original logic,certain monadic datalog program,lower bound,fixed point,satisfiability,upper bound | Bernays–Schönfinkel class,Model checking,Computer science,Satisfiability,Algorithm,Zeroth-order logic,Decidability,Transitive closure,Datalog,Higher-order logic | Conference |
Volume | ISSN | ISBN |
6397 | 0302-9743 | 3-642-16241-X |
Citations | PageRank | References |
5 | 0.48 | 23 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| witold charatonik | 1 | 349 | 28.71 |
| Piotr Witkowski | 2 | 13 | 4.09 |