Logic programs

From Learning Logic for Computer Science

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(not(X)) :- false(X).
 true(or(X,_)) :- true(X). 
 true(or(_,Y)) :- true(Y).
 true(and(X,Y)) :- true(X),true(Y).
 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.