wrld

my Internet corner

Home

On logic, formal verification and decision procedures - Part I

This post tries to be the enstablishment of a series that aims to introduce the use of formal methods and decision procedures in computer science and software engineering. The structure adopted strictly follows the one used in the book "The Calculus of Computation", which is the source of most of the following material.

Fundamentals of computation

A computation is any type of calculation that includes both arithmetical and non-arithmetical steps and which follows a well-defined model (e.g. an algorithm). Wikipedia

Propositional logic

Propositional logic is the first building block necessary to embark on the long journey of formal methods. As the name suggests, it handles propositions It is a statement which has a truth value, meaning it can be proved to be true or false. For a proposition to be valid, it must be possible to prove the proposition is either true or false. and are usually noted as $$P, Q, R$$

Syntax

Propositional logic (from now on PL) is made of three primitive elements:

Truth values

$$\top$$ (true) and $$\bot$$ (false)

Propositional variables

In mathematical logic, a propositional variable (also called a sentential variable or sentential letter) is a variable which can either be true or false. Wikipedia

They are usually denoted as $$P, Q, R, P_1, P_2, \dots$$

Logical conjectives

They are respectively: "not", "and", "or", "implies", "if and only if"

$\neg, \wedge, \vee, \rightarrow, \leftrightarrow$

Except negation which is unary, all of the aforementioned operators are binary.

In OCaml, we can create this type as follows:

type formula =
| False
| True
| And of formula * formula
| Not of formula * formula
| Or of formula * formula
| Imp of formula * formula
| Iif of formula * formula
;;


These logical connectives have an aritythe number of aguments that it takes.

Subformula

Formula $$G$$ is a subformula of formula $$F$$ if it occures syntactically within $$G$$.

Semantics

Semantics (from Ancient Greek: σημαντικός sēmantikós, "significant") is the study of meaning, reference, or truth. Wikipedia

In order to define the semantics of PL there must be a mechanism in place for evaluating the propositional variables. An interpretation $$I$$ assigns to every propositional variable exactly one truth value.

$I: \{P \rightarrow true, Q \rightarrow false \}$

In the example, $$I$$ assigns $$true$$ to $$P$$ and $$false$$ to $$Q$$ Given a PL formula $$F$$ and an interpretation $$I$$, the simplest way to compute the value (or truth value) of $$F$$ is via a truth table. The readers of likely fall in categories that are very much acquainted to the process of reading and interpreting a truth table, therefore I, as of now, won't delve too much into it in favor of covering potentially more interesting By "more interesting" I mean't to say "potentially less known" What I will specify, are a couple of things in regards to notation. These notions will be further explored in future posts.

Inductive definition of PL's semantics

Truth tables, as convenient as they are a notation, are unsuitable for predicate logic, therefore we give now an inductive definition of PL's semantics.

Inductive definitions of sets are often informally presented by giving some rules for generating elements of the set and then adding that an object is to be in the set only if it has been generated according to the rules. An equivalent formulation is to characterize the set as the smallest set closed under the rules.

We write $$I \models F$$ if $$F$$ evaluates to $$true$$ under $$I$$ and $$I \not \models F$$To be read as "does not evaluate" if it evaluates to $$false$$.

Lets start by defining giving meaning to truth symbols

$I \models \top$ $I \not \models \bot$

Regardless of which interpretation $$I$$, $$\top$$, has a value $$true$$ and $$\bot$$ has value $$false$$.

$I \models P, \text{ iif } I[P] = true$

Next, the definition of propositional variables:

$I \not \models P \text{ iif } I[P] = false$

This is the base case of the inductive definition. The inductive step is made of the combinations of the following more complex formuales:

\begin{align*} & I \models \neg F, & \; \text{ iif } I \not \models F \\ & I \models F_1 \wedge F_2, & \; \text{ iif } I \models F_1 \text{ and } I \models F_2 \\ & I \models F_1 \vee F_2, & \; \text{ iif } I \models F_1 \text{ or } I \models F_2\\ & I \models F_1 \rightarrow F_2, & \; \text{ iif, if } I \models F_1 \text{ then } \models I \models F_2 \\ & I \models F_1 \leftrightarrow F_2, & \; \text{ iif } I \models F_1 \text{ and } I \models F_2, \text{ or } I \not \models F_1 \text{ and } I \not \models F_2 \\ \end{align*}

Satisfiability and Validity

Here follow two fundamental properties that are of interest in the study of formulaes

Satisfiability

A formula $$F$$ is said to be satisfiable if and only if there exists an interpretation $$I$$ such that

$I \models F$

Validity

A formula $$F$$ is valid if and only if for all interpretation $$I$$

$I\models F$

They are often times interchangeable to a certain degree, one gives information about the other as through the semantics of negation they can be proven to be dual. This allows us to choose whatever is most comfortable for a given task. As anyone might have guessed at this point, it is very interesting to determine whether a formulae is satisfiable and/or valid.

Equivalence and Implication

Two formulae $$F_1$$ and $$F_2$$ are equivalent if they evaluate to the same truth value under all interpretations $$I$$. That is, for all interpretations $$I$$, $$I \models F_1$$ iif $$I\models F_2$$.

Formula $$F_1$$ implies formula $$F_2$$ if $$I \models F_2$$ for every interpretation $$I$$ such that $$I\models F_1$$.

Substitution

A substitution $$\sigma$$ is a mapping from formulae to formulae:

$\sigma: \{F_1 \rightarrow G_1, \dots, F_n \rightarrow G_n \}$

The domain of $$\sigma$$ is:

$domain(\sigma): \{F_1, \dots, F_n \}$

The range of $$\sigma$$ is:

$range(\sigma): \{G_1, \dots, G_n \}$

Replacements occur all at once.

Substitution of Equivalent Formulae

Consider substitution

$\sigma: \{F_1 \rightarrow G_1, \dots, F_n \rightarrow G_n \}$

such that for each $$i, F_i \leftrightarrow, G_i$$ . Then $$F \leftrightarrow F_{\sigma}$$

which means that given a formula and a substitution, if each part of the derived formula is equivalent to its substitution, the derived formula is equivalent to the starting one.

One very mathematically interesting thing is that proving the validity of a PL formula $$F$$ proves the validity of an infinite set of formulae, the set of all formulaes that can be derived via a variable substitution

Valid Template

If $$F$$ is valid and $$G = F_{\sigma}$$ for some variable substitution $$\sigma$$, then $$G$$ is valid.

Normal Forms

A normal form of formulae is a syntactic restriction such that for every formula of the logic, there is an equivalent formula in the normal form. Three normal forms are particularly important for PL.

Negation normal form (NNF)

A NNF requires that $$\neg, \wedge, \vee$$ be the only connectives and that negations appear only in literals

Disjuntive normal form (DNF)

A formula is in DNF if it is a disjunction of conjunction of literals

$\bigvee_i \bigwedge_j\text{ for literals }\mathcal{l}_{i,j}$

Conjuctive normal form (CNF)

A formula is in CNF if it is a conjunction of disjunction literals. This is the dual of DNF

$\bigwedge_i \bigvee_j \text{ for literals }\mathcal{l}_{i,j}$