LARA

Differences

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

Link to this comparison view

Next revision
Previous revision
Last revision Both sides next revision
sav08:satisfiability_of_sets_of_formulas [2008/03/10 18:10]
vkuncak created
sav08:satisfiability_of_sets_of_formulas [2008/03/11 18:21]
vkuncak
Line 1: Line 1:
 ====== Satisfiability of Sets of Formulas ====== ====== Satisfiability of Sets of Formulas ======
 +
 +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$.