202311141411

Tags : Logic

---

Finite Essentially Uninterpreted (FEU) fragment

Satisfiability Modulo Theories (SMT)

Consider $(\mathbb{N};+;<;0)f,g,p,r$, where the things in the bracket are ‘interpreted’ (i.e. they have the general interpretation) and the ones outside are ‘uninterpreted’ (i.e. they can be anything, which can later be interpreted). We want to check the satisfiability of $\phi$ modulo these constraints. This problem is what is solved by SMT solvers.

Skolemization

We can trade existential quantified variables for (Skolem) functions. example

$$\phi :\forall \bar{x}\exists y(\dots r(\dots y\dots )\dots )$$

means that for every tuple $\bar{x}$ we can find a $y$ that satisfies the formula, This can be represented with the function $f:S^k\to S$ and we can rewrite the formula as

$$\phi :\forall \bar{x}(\dots r(\dots f(\bar{x})\dots )\dots )$$

Essentially uninterpreted formulas

A formula $\phi$ is essentially uninterpreted if any variable in $\phi$ appears only as an argument of uninterpreted function or predicate symbols (= relation symbols). So $f(g(x_1)+0)\le h(x_1)\cup p(f(x_1)+b.x_2)$ is uninterpreted while $x_1+f(x_2)$ is not, because $x_1$ is an argument of ${}^{\prime }{+}^{\prime }$, which is interpreted.

Conjunctive Normal Form:

• Literal: atomic formula or its negation
• Clause: disjunction of literals
• CNF formula: conjunction of clauses

Ground formulas: formulas that don’t use variables

Goal

Given a CNF formula $\phi$, we would like to come up with a Ground formula ${\phi }^{\ast }$ s.t. ${\phi }^{\ast }$ is satisfiable iff $\phi$ is satisfiable.

Notation

---

References