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:satisfiability_of_sets_of_formulas [2008/03/11 18:21]
vkuncak
sav08:satisfiability_of_sets_of_formulas [2008/03/18 00:45] (current)
tatjana
Line 3: Line 3:
 We next introduce sets of formulas as a way of talking about potentially infinite conjunctions of formulas. ​ We will need this when reducing reasoning in first-order logic to reasoning in propositional logic. We next introduce sets of formulas as a way of talking about potentially infinite conjunctions of formulas. ​ We will need this when reducing reasoning in first-order logic to reasoning in propositional logic.
  
-We say that interpretation $I$ is a model for a set of formulas $S$, written $I \models S$, iff for each $F \in S$, $I \models F$.  In other words, we view a set of formulas as a (potentially infinite) conjunction;​ when $S$ is finite then $I \models S$ is the same condition as $I \models \bigwedge_{F \in S} F$.+We say that interpretation $I$ is a model for a set of formulas $S$, written $I \models S$, iff for each $F \in S$, $I \models F$.  In other words, we view a set of formulas as a (potentially infinite) conjunction;​ when $S$ is finite then $I \models S$ is the same condition as $I \models \bigwedge_{F \in S} F$. 
  
-Example: the set $\{p_1, \lnot p_1 \lor p_2, \lnot p_2 \lor p_3, \lnot p_3 \lor p_4, \ldots \}$ is an infinite satisfiable set.+Example: the set $\{p_1, \lnot p_1 \lor p_2, \lnot p_2 \lor p_3, \lnot p_3 \lor p_4, \ldots \}$ is an infinite satisfiable set. The example of one satisfying interpretation is the interpretation which evaluates all variables to $true$.
  
 Clearly, if $I \models B$ and $A \subseteq B$, then also $I \models A$. Clearly, if $I \models B$ and $A \subseteq B$, then also $I \models A$.
  
-We say that a set of formulas $S$ is satisfiable iff there exists an interpretation $I$ such that $I \models ​F$.+We say that a set of formulas $S$ is satisfiable iff there exists an interpretation $I$ such that $I \models ​S$.
 
sav08/satisfiability_of_sets_of_formulas.txt · Last modified: 2008/03/18 00:45 by tatjana
 
© EPFL 2018 - Legal notice