Name
Abstract | ||
|---|---|---|
Nielson et al. [12] exhibit a rich class of Horn clauses which they call H1. Least models of finite sets of H1 Horn clauses are regular tree languages. Nielson et al. [12] describe a normalization procedure for computing least models of finite sets of H1 Horn clauses in the form of tree automata. In the present paper, we simplify and extend this normalization procedure to a semi-procedure that deals with finite sets of linear Horn clauses. The extended semi-procedure does not terminate in general but does so on useful subclasses of finite sets of linear Horn clauses. The extension in particular coincides with the normalization procedure of Nielson et al. [12] for sets of H1 Horn clauses. In order to demonstrate the usefulness of the extension, we show how backward reachability analysis for constrained dynamic pushdown networks (see Bouajjani et al. [3]) can be encoded into a class of finite sets of linear Horn clauses for which our normalization procedure terminates after at most exponentially many steps. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/978-3-642-19829-8_16 | SBMF |
Keywords | Field | DocType |
horn clause,linear horn clause,normalization procedure terminates,normalization procedure,h1 horn clause,extended semi-procedure,regular tree language,rich class,finite set,tree automaton | Discrete mathematics,Horn clause,Normalization (statistics),Finite set,Computer science,Horn-satisfiability,Automaton,Algorithm,Theoretical computer science,Reachability,Unit propagation | Conference |
Volume | ISSN | Citations |
6527 | 0302-9743 | 0 |
PageRank | References | Authors |
0.34 | 10 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Thomas Martin Gawlitza | 1 | 88 | 6.37 |
| Helmut Seidl | 2 | 1468 | 103.61 |
| Kumar Neeraj Verma | 3 | 171 | 8.87 |