Polishing

relation $P^\mathcal{A} \subseteq A^n$. Given a $\Sigma$-structure

$\mathcal{A}$, there exists a unique homomorphic extension of

$(\_)^\mathcal{A}$ to $\Sigma$-terms, which to each $\Sigma$-term $t$

assigns an element $t^\mathcal{A} \in A$. In turn, using standard

assigns an element $t^\mathcal{A} \in A$. In turn, by using standard

definitions, the assignment $(\_)^\mathcal{A}$ can be further extended

to assign a truth value $\varphi^\mathcal{A} \in \{ \true, \false \}$

to each $\Sigma$-formula $\varphi$. A $\Sigma$-structure $\mathcal{A}$

modified. Arity of a symbol determines not only a number of its

arguments, but also their types -- each function symbol has assigned

$(n+1)$-tuple of sort symbols for a non-negative integer $n$ and each

predicate symbols has assigned a $n$-tuple of sort symbols for a

predicate symbol has assigned a $n$-tuple of sort symbols for a

non-negative integer $n$. Simultaneous inductive definition of terms

of a sort $S \in \Sigma^S$ and definitions of atoms, literals, clauses

of sorts $S \in \Sigma^S$ and definitions of atoms, literals, clauses

and formulas are straightforward and can be found for example in

Enderton~\cite{End01}.

remain, the formula is satisfiable. The main problem of \dppr is its

space complexity, since the number of the clauses may grow

exponentially even for simple formulas. To alleviate this problem, the

refinement of \dppr algorithm was introduced in 1962 by Davis,

refinement of the \dppr algorithm was introduced in 1962 by Davis,

Logemann and Loveland~\cite{DPLL62}.

The Davis--Putnam--Logemann--Loveland \quotegraffito{If you don't know