Loading...
Please wait, while we are loading the content...
Similar Documents
IC3, PDR, and Friends
| Content Provider | Semantic Scholar |
|---|---|
| Author | Gurfinkel, Arie |
| Copyright Year | 2015 |
| Abstract | We describe the IC3/PDR algorithms and their various generalizations. Our goal is to give a brief overview of the algorithms and describe them using unified notation. Many crucial optimizations and implementation details are omitted. 1 Constrained Horn Clauses Given the sets F of function symbols, P of predicate symbols, and V of variables, a Constrained Horn Clause (CHC) is a First Order Logic (FOL) formula of the form: ∀V · (φ ∧ p1[X1] ∧ · · · ∧ pk[Xk]→ h[X]), for k ≥ 0 where: φ is a constraint over F and V with respect to some background theory A; Xi, X ⊆ V are (possibly empty) vectors of variables; pi[Xi] is an application p(t1, . . . , tn) of an n-ary predicate symbol p ∈ P for first-order terms ti constructed from F and Xi; and h[X] is either defined analogously to pi or is P-free (i.e., no P symbols occur in h). Here, h is called the head of the clause and φ ∧ p1[X1] ∧ . . . ∧ pk[Xk] is called the body. A clause is called a query if its head is P-free, and otherwise, it is called a rule. A rule with body true is called a fact. We say a clause is linear if its body contains at most one predicate symbol, otherwise, it is called non-linear. In this paper, we follow the Constraint Logic Programming (CLP) convention of representing Horn clauses as h[X]← φ, p1[X1], . . . , pk[Xk]. A CHC with constraint φ is satisfiable if there exists an interpretation I of the predicate symbols P such that each constraint φ is true under I. A set Π of CHCs is satisfiable if there exists an interpretation I that satisfies all clauses in Π. Satisfiability of a set Π of linear CHC is reducible to satisfiability of 3 clauses of the form: |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.dtic.mil/dtic/tr/fulltext/u2/1027075.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
