Lab for Automated Reasoning and Analysis LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
sav08:polynomial_algorithm_for_horn_clauses [2008/03/12 14:10]
vkuncak
sav08:polynomial_algorithm_for_horn_clauses [2008/03/12 15:59] (current)
vkuncak
Line 5: Line 5:
 Such clause is either of the form $\{p\}$ where $p \in V$ is a variable, or $\{\lnot p\}$ for $p \in V$, or of the form $\{\lnot p_1, \ldots, \lnot p_n, q\}$ for $n \ge 1$, that is $p_1 \land \ldots \land p_n \rightarrow q$. Such clause is either of the form $\{p\}$ where $p \in V$ is a variable, or $\{\lnot p\}$ for $p \in V$, or of the form $\{\lnot p_1, \ldots, \lnot p_n, q\}$ for $n \ge 1$, that is $p_1 \land \ldots \land p_n \rightarrow q$.
  
-The following algorithm eliminates clauses of the form $\{p\}$, keeping only clauses that have at least one assumption.+The following algorithm eliminates clauses of the form $\{p\}$, keeping only clauses that have at least one negative literal.
  
 To check satisfiability of a set of Horn clauses: To check satisfiability of a set of Horn clauses:
 
sav08/polynomial_algorithm_for_horn_clauses.txt · Last modified: 2008/03/12 15:59 by vkuncak
 
© EPFL 2018 - Legal notice