Logic programs

Logic programming languages are declarative programming languages based on the entailment relation. Logic programs are the core of programs in logic programming languages.

Definition Let $\mathcal S$ be a signture. A logic program over $\mathcal S$ is a finite set of $\mathcal S$-formulas of the form \begin{align} \bigwedge_{i<n} L_i \rightarrow L \enspace, \end{align} where each $L_i$ and $L$ are positive $\mathcal S$-literals.

Example The following list of formulas, viewed as a set, is a logic program over $\{\text{true}, \text{false}, \text{not}/\!/1, \text{and}/\!/2, \text{or}/\!/2, \text{True}/1, \text{False}/1\}$ which describes how truth values are combined using boolean connectives. \begin{align} & \text{True}(\text{true})\\ & \text{False}(\text{false})\\ & \text{False}(x_0) \rightarrow \text{True}(\text{not}(x_0))\\ & \text{True}(x_0) \rightarrow \text{False}(\text{not}(x_0))\\ & \text{True}(x_0) \rightarrow \text{True}(\text{or}(x_0,x_1))\\ & \text{True}(x_1) \rightarrow \text{True}(\text{or}(x_0,x_1))\\ & \text{False}(x_0) \wedge \text{False}(x_1) \rightarrow \text{False}(\text{or}(x_0,x_1))\\ & \text{False}(x_0) \rightarrow \text{False}(\text{and}(x_0,x_1))\\ & \text{False}(x_1) \rightarrow \text{False}(\text{and}(x_0,x_1))\\ & \text{True}(x_0) \wedge \text{True}(x_1) \rightarrow \text{True}(\text{and}(x_0,x_1))\\ \end{align}

In Swish prolog, this looks as follows.

 true(true).
 true(not(X)) :- false(X).
 true(or(X,_)) :- true(X). 
 true(or(_,Y)) :- true(Y).
 true(and(X,Y)) :- true(X),true(Y).
 false(false).
 false(not(X)) :- true(X).
 false(or(X,Y)) :- false(X),false(Y).
 false(and(X,_)) :- false(X).
 false(and(_,Y)) :- false(Y).

The semantics of a logic program draws on entailment.

Definition Let $\mathcal S$ be a signature. An $\mathcal S$-goal is of the form $\bigwedge_{i<n}L_i$ where each $L_i$ is a positive $\mathcal S$-literal.

Let $\Phi$ be a logic program over $\mathcal S$ and denote the above goal by $\psi$. An answer substitution for $\Phi$ and $\psi$ is a substitution $\sigma$ with $\text{dom}(\sigma) \subseteq \text{vars}(\psi)$ such that $\{\forall \phi \colon \phi \in \Phi\} \models \forall (\psi\sigma)$.

This definition says, in particular, that the formulas a logic program consists of are viewed as universal formulas.

Example Let $\Phi$ be the logic program from above and the goal $\psi$ defined by $\psi = \text{True}(\text{and}(x_0, \text{not}(x_1))$. The answer substitutions for $\Phi$ and $\psi$ are the substitutions $\{x_0 \mapsto t_0, x_1 \mapsto t_1\}$ where $t_0$ and $t_1$ are terms which, when viewed as boolean formulas evaluate to 1 and 0, respectively.

The above logic program can be used to check propositional formulas for satisfiability.