Logic, Satisfiability, and Reasoning

Module 1: Propositional Logic (SAT)

1.1 Syntax and Semantics

Propositional logic evaluates the truth of basic statements. The syntactic building blocks include truth constants ( $\top$, $\bot$ ), propositional variables (atoms) $P$, and literals (variables or their negations). The language of propositional logic, $L$, is defined recursively:

where $p \in P$. The standard precedence of operations is $\neg \gg \land \gg \lor \gg \rightarrow \gg \leftrightarrow$.

An assignment $\nu: P \rightarrow \{0, 1\}$ maps variables to boolean values. The semantic interpretation function $\llbracket \cdot \rrbracket_\nu$ computes the truth value of a formula under assignment $\nu$:

• $\llbracket \neg \phi \rrbracket_\nu = 1$ iff $\llbracket \phi \rrbracket_\nu = 0$
• $\llbracket \phi \lor \psi \rrbracket_\nu = 1$ iff $\llbracket \phi \rrbracket_\nu = 1$ or $\llbracket \psi \rrbracket_\nu = 1$
• $\llbracket \phi \land \psi \rrbracket_\nu = 1$ iff $\llbracket \phi \rrbracket_\nu = 1$ and $\llbracket \psi \rrbracket_\nu = 1$
• $\llbracket \phi \rightarrow \psi \rrbracket_\nu = 1$ iff $\llbracket \phi \rrbracket_\nu = 0$ or $\llbracket \psi \rrbracket_\nu = 1$

A formula is satisfiable if there exists at least one model (assignment $\nu$ ) where $\llbracket \phi \rrbracket_\nu = 1$. It is valid (a tautology) if $\llbracket \phi \rrbracket_\nu = 1$ for all assignments, and unsatisfiable if $\llbracket \phi \rrbracket_\nu = 0$ for all assignments.

1.2 Normal Forms and Tseitin Encoding

A Conjunctive Normal Form (CNF) is a conjunction of clauses, where each clause is a disjunction of literals:

Any formula can be converted to CNF via logical equivalences (e.g., De Morgan's laws: $\neg(\phi \land \psi) \Leftrightarrow \neg\phi \lor \neg\psi$ ), but naive conversion can cause exponential blow-up. Instead, practical SAT solving introduces new labels for subformulas (Tseitin Encoding) to maintain polynomial size. For a subformula $a \leftrightarrow b$, a label $v_1$ is introduced, yielding the clauses:

$$(\neg v_1 \lor \neg a \lor b) \land (\neg v_1 \lor a \lor \neg b) \land (v_1 \lor \neg a \lor \neg b) \land (v_1 \lor a \lor b)$$
which are added to a master conjunction ensuring equi-satisfiability.

1.3 SAT Solving and Calculi

Solving SAT relies on the Davis-Putnam-Logemann-Loveland (DPLL) algorithm utilizing Binary Constraint Propagation (BCP). BCP simplifies CNF formulas when a unit clause $(l)$ is present by removing all clauses containing $l$ and all occurrences of the literal $\neg l$.

The Resolution Calculus proves unsatisfiability using a single rule on CNF clauses:

$$\frac{x \lor C \quad \neg x \lor D}{C \lor D}$$
where $x$ is the pivot and $C \lor D$ is the resolvent. Deriving the empty clause $\bot$ proves unsatisfiability.

Sequent Calculus is used to reason about formulas using sequents $\phi_1, \dots, \phi_n \vdash \psi$, meaning the assumptions $\phi_1, \dots, \phi_n$ entail the goal $\psi$.

Module 2: Satisfiability Modulo Theories (SMT)

2.1 Eager vs. Lazy SMT Solving

SMT enhances SAT by integrating domain-specific reasoning (theories).

• Eager Approach: Translates the entire SMT problem into an equi-satisfiable propositional formula (e.g., bit-blasting) and runs an off-the-shelf SAT solver.
• Lazy Approach (Lemmas on Demand): Abstracts the formula into a propositional skeleton by replacing theory constraints with boolean variables. A SAT solver finds a model, which is then checked by a theory solver. If theory-inconsistent, a Minimal Unsatisfiable Core (MUS) is returned as a lemma, constraining the SAT solver further.

2.2 Background Theories

Equality with Uninterpreted Functions (EUF): Functions lack concrete definitions but must obey the congruence axiom:

$$\forall x, y : x = y \rightarrow f(x) = f(y)$$
Satisfiability is resolved via the Congruence Closure Algorithm, which builds equivalence classes of terms and merges them upon discovering equalities. Alternatively, Ackermann's Reduction flattens terms and replaces function instances $f(u)$ with new variables $f_u$, enforcing $(u = v \rightarrow f_u = f_v)$.

Linear Real Arithmetic (LRA): Predicates include $=, <, \le$, and functions are restricted to $+$, $-$, and multiplication by a constant. Conjunctions of inequalities are solved using the Fourier-Motzkin Elimination Procedure, which isolates variables and creates new inequalities.

$$z + y \le x \land x \le 5 - 2y \implies z + y \le 5 - 2y$$

Bit-Vectors (BV): Models RTL hardware or finite-precision integer semantics. Resolved eagerly via bit-blasting. For an equality $u = v$ between width- $w$ bit-vectors, we introduce bits $u_i, v_i$ and the constraint:

$$e_{u=v} \leftrightarrow \bigwedge_{i=1}^w (u_i \leftrightarrow v_i)$$

Arrays: Modelled by read and write functions fulfilling array congruence and read-over-write axioms:

$$\forall a, v, i, j : i = j \rightarrow \text{read}(\text{write}(a, i, v), j) = v$$
$$\forall a, v, i, j : i \neq j \rightarrow \text{read}(\text{write}(a, i, v), j) = \text{read}(a, j)$$

Module 3: First-Order Logic (FOL) Syntax and Semantics

3.1 Abstract Syntax

First-Order Logic (Predicate Logic) introduces objects and properties.
Terms $t$ evaluate to objects in a domain, while formulas $F$ evaluate to truth values. The grammar is:

$$t ::= v \mid c \mid f(t_1, \dots, t_n)$$

$$F ::= p(t_1, \dots, t_n) \mid \top \mid \bot \mid (\neg F) \mid (F_1 \land F_2) \mid (F_1 \lor F_2) \mid (F_1 \rightarrow F_2) \mid (F_1 \leftrightarrow F_2) \mid (\forall v : F) \mid (\exists v : F)$$

where $v$ is a variable, $c$ is a constant, $f$ is an $n$ -ary function symbol, and $p$ is an $n$ -ary predicate symbol.
The set of free variables $\text{fv}(F)$ computes variables not bound by quantifiers. For quantifiers:

$$\text{fv}(\forall v : F) = \text{fv}(F) \setminus \{v\}, \quad \text{fv}(\exists v : F) = \text{fv}(F) \setminus \{v\}$$

3.2 Formal Semantics

The meaning of FOL depends on a structure $M = (D, I)$ and an assignment $a$. The domain $D$ is a non-empty set. The interpretation $I$ maps constants to domain elements, functions to $n$ -ary domain functions $I(f): D^n \rightarrow D$, and predicates to relations $I(p) \subseteq D^n$. An assignment $a(v)$ maps variables to objects in $D$.

Term semantics $\llbracket t \rrbracket_{a}^{D,I} \in D$ are recursively defined:

$$\llbracket v \rrbracket_{a}^{D,I} := a(v)$$

$$\llbracket c \rrbracket_{a}^{D,I} := I(c)$$

$$\llbracket f(t_1, \dots, t_n) \rrbracket_{a}^{D,I} := I(f)(\llbracket t_1 \rrbracket_{a}^{D,I}, \dots, \llbracket t_n \rrbracket_{a}^{D,I})$$

Formula semantics $\llbracket F \rrbracket_{a}^{D,I} \in \{\text{true}, \text{false}\}$ for quantifiers evaluate via assignment updates $a[x \mapsto d]$:

$$\llbracket \forall x : F \rrbracket_{a}^{D,I} := \text{true if } \llbracket F \rrbracket_{a[x \mapsto d]}^{D,I} = \text{true for all } d \in D \text{, false else}$$

$$\llbracket \exists x : F \rrbracket_{a}^{D,I} := \text{true if } \llbracket F \rrbracket_{a[x \mapsto d]}^{D,I} = \text{true for some } d \in D \text{, false else}$$

A structure $M$ is a model of $F$ ( $M \models F$ ) if $\llbracket F \rrbracket_a^M = \text{true}$ for all $a$. $F$ is valid ( $\models F$ ) if every structure is a model.

Module 4: First-Order Logic (FOL) Reasoning

4.1 Proof Calculus and Inference Rules

Formal proofs use schematic inference rules mapping premises to a conclusion:

$$\frac{S_1 \quad \dots \quad S_n}{S}$$

Sequents follow the format $K\dots \vdash G$, implying assumptions $K$ entail goal $G$. Critical quantificational rules include:

Universal Quantifier:

• Prove as a goal ( P- $\forall$ ): Skolemization. Introduce an arbitrary but fixed constant $\bar{x}$:

$$\frac{K\dots \vdash F[\bar{x}/x]}{K\dots \vdash (\forall x : F)} \quad \text{where } \bar{x} \text{ does not occur in } K\dots, F$$

• Use as assumption ( A-$\forall$ ): Instantiation. Choose a suitable witness term $t$:

$$\frac{K\dots, (\forall x : F), F[t/x] \vdash G}{K\dots, (\forall x : F) \vdash G}$$

Existential Quantifier:

• Prove as a goal ( P- $\exists$ ): Instantiation. Provide a witness term $t$:

$$\frac{K\dots \vdash F[t/x]}{K\dots \vdash (\exists x : F)}$$

• Use as assumption ( A- $\exists$ ): Skolemization. Introduce an arbitrary but fixed constant $\bar{x}$:

$$\frac{K\dots, F[\bar{x}/x] \vdash G}{K\dots, (\exists x : F) \vdash G} \quad \text{where } \bar{x} \text{ does not occur in } K\dots, F, G$$

4.2 Mathematical Induction

To reason comprehensively over $\mathbb{N}_{\ge m}$, FOL inference rules are augmented with the induction principle:

$$\frac{K\dots \vdash F[m/n] \quad K\dots, \bar{n} \in \mathbb{N}_{\ge m}, F[\bar{n}/n] \vdash F[(\bar{n}+1)/n]}{K\dots \vdash \forall n \in \mathbb{N}_{\ge m} : F}$$
This consists of the Induction Base ( $F[m/n]$ ), the Induction Hypothesis ( $F[\bar{n}/n]$ for a new constant $\bar{n} \ge m$ ), and the Induction Step (proving $F[(\bar{n}+1)/n]$ ).

4.3 Expressiveness and Limitations

First-order logic variables range strictly over domain objects, preventing direct quantification over functions or predicates (which requires second-order logic). We circumvent this via set theory, mapping functions to sets of tuples.

• Completeness (Gödel, 1929): FOL possesses a calculus that is both sound ( $\Gamma \vdash F \implies \Gamma \models F$ ) and complete ( $\Gamma \models F \implies \Gamma \vdash F$ ).
• Undecidability (Church/Turing, 1936/1937): There is no algorithm that can always terminate and decide whether $\Gamma \models F$. It is only semi-decidable.
• Incompleteness (Gödel, 1931): No sound formal system sufficiently rich to describe arithmetic can prove or disprove all true statements within itself (e.g., the infinite induction schema cannot be captured by a single FOL formula).