Sequent Calculus

Sequent calculus is usually viewed as being applied in a backward manner to construct proofs for sequents $S$ by eliminating the logical symbols in $S$ one after the other. For this mode of application cuts are not required, although their use might lead to much smaller proofs.

Saturation-based theorem proving can be viewed as a mechanism for establishing

$$S_1,\ldots,S_k \vdash {\to}$$

that is, for deriving the empty sequent $\to$ from an inconsistent set $S_1,\ldots,S_k$ of sequents, by the forward application of the rules of the sequent calculus. In that context, the cut rule becomes the main working horse, and its combination with the substitution rule, which is an inverse form of certain quantifier rules, is called resolution. That view of resolution allows one to integrate clausal normalform transformation into resolution and chaining in a lazy manner.

The (multi-conclusion) rules that we apply in a forward manner are the inverse forms

$$\strut\displaystyle {\Gamma \to F\wedge G,\Delta } \over \strut\displaystyle {\Gamma \to F,\Delta \quad \Gamma \to G,\Delta }$$

of invertible rules such as

$$\strut \Gamma \to F,\Delta \quad \Gamma \to G,\Delta \over \strut \Gamma \to F\wedge G,\Delta$$

for the logical connectives. (The expanded formula $F\wedge G$ of the inference is called its main formula below.) The quantifier rules that we use are

$$\strut\displaystyle {\Gamma \to \forall x. F(x), \Delta } \over \strut\displaystyle {\Gamma \to F(X), \Delta }$$

where $X$ is a fresh free variable, and

$$\strut\displaystyle {\Gamma \to \exists x. F(x,\vec Y), \De... ...\strut\displaystyle {\Gamma \to F(f(\vec Y),\vec Y), \Delta }$$

where $f$ is a new (Skolem) function symbol and $\vec Y$ are the free variables in $F$. (The ``left`` versions of the rules are analoguous.)

Note that these rules are simplifications in that the premise can be deleted once its conclusions have been derived. In fact, the conclusions imply their premise and are smaller in an appropriate extension of the atom ordering to general first-order formulas. However, we apply rules only if the main formula is either maximal in the sequent or negative and selected. In other words, the rules obey the same restrictions with respect to ordering and selection functions as the chaining inferences.

Sequents in Saturate may contain equalities $F\mathrel{\mbox{{\tt ==}}}G$ between formulas $F$ and $G$, semantically denoting equivalence of $F$ and $G$, which are dealt with specifically. Only if a maximal one of the two sides $F$ and $G$ is non-atomic, the equality is expanded according to

$$\strut\displaystyle {\Gamma \to F\mathrel{\mbox{{\tt ==}}}G,... ...splaystyle {\Gamma,F\to G,\Delta \quad \Gamma,G \to F,\Delta }$$

In case $F\succ G$ and $F$ is atomic, i.e., of the form $p(s_1,\ldots,s_k)$, with a predicate symbol $p$ and terms $s_i$, the equivalence is not eliminated from the sequent. Non-eliminated equivalences are subject to ordering-restricted forms of chaining inferences such as

$$\strut \Gamma \to A\mathrel{\mbox{{\tt ==}}}F,\Delta \quad \... ...mma,\Lambda \to F\mathrel{\mbox{{\tt ==}}}G,\Delta,\Pi)\sigma$$

with $\sigma$ the mgu of the atoms $A$ and $B$, provided $F\sigma\not\succeq A\sigma$, $G\sigma\not\succeq A\sigma$, no premise contains a selected literal, and both equivalences are maximal in their respective premises.

Orientable equivalences $A\mathrel{\mbox{{\tt ==}}}F$ in which the maximal side $A$ is atomic are also used for simplification in that everywhere occurences of $A\sigma$ will be replaced by $F\sigma$. This handling of equivalences is especially useful for definition hierarchies if the definitions are to be applied in a goal to replace derived predicates and if one does not want to automatically infer lemmas for the new predicates. An example how proofs in Saturate look like when simplification with equivalences are intertwined with chaining is a simple set theory with an ordering under which definitions are expanded out.

Imprint | Data Protection