- English only

# Lab for Automated Reasoning and Analysis LARA

# 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 is a model for a set of formulas , written , iff for each , . In other words, we view a set of formulas as a (potentially infinite) conjunction; when is finite then is the same condition as .

Example: the set is an infinite satisfiable set. The example of one satisfying interpretation is the interpretation which evaluates all variables to .

Clearly, if and , then also .

We say that a set of formulas is satisfiable iff there exists an interpretation such that .