next up previous contents
Next: 20. The Initial Theory Up: 3. Reference Manual Previous: 18. The Proof Commands

Subsections

  
19. The Primitive Inference Procedures

In this chapter we list and document each of the primitive inference procedures. We will use the following format to describe them.

Parameters.
A list of the arguments (other than the sequent node) required by procedure. These arguments can be of the following types:
Description.
A brief description of the primitive inference. Some of primitive inference procedures have descriptions which are identical to the description of the corresponding interactive proof command.

  
antecedent-inference

Parameters:

A sequent node assumption.

Description:

The effect of applying this primitive inference procedure is given by the following table.
Conclusion $\Gamma \cup \{ \varphi \supset \psi\} \Rightarrow \theta$
Premises $\Gamma \cup \{\neg \varphi\} \Rightarrow \theta$
  $\Gamma \cup \{\psi \} \Rightarrow \theta$
Conclusion $\Gamma \cup \{\varphi_1 \wedge \cdots \wedge \varphi_n
\} \Rightarrow \psi$
Premise $\Gamma \cup \{\varphi_1, \ldots ,\varphi_n
\} \Rightarrow \psi$
Conclusion $\Gamma \cup \{\varphi_1 \vee \cdots \vee \varphi_n \} \Rightarrow \psi$
Premises $(1\leq i \leq n)$ $\Gamma \cup \{\varphi_i \} \Rightarrow
\psi$
Conclusion $\Gamma \cup \{\varphi \equiv \psi\} \Rightarrow \theta$
Premises $\Gamma \cup \{\varphi,\psi\} \Rightarrow \theta$
  $\Gamma \cup \{\neg \varphi,\neg \psi\}\Rightarrow \theta$
Conclusion $\Gamma \cup \{\mbox{if-form}(\varphi,\psi,\theta)\} \Rightarrow
\xi$
Premises $\Gamma \cup \{\varphi,\psi\} \Rightarrow \xi$
  $\Gamma \cup \{\neg\varphi,\theta\} \Rightarrow \xi$
Conclusion $\Gamma \cup \{\exists x_1\mbox{:}\sigma_1, \ldots,
x_n\mbox{:}\sigma_n, \varphi\} \Rightarrow \psi$
Premise $\Gamma \cup \{\varphi^\prime\} \Rightarrow \psi$


Notes:

  
backchain-inference

Parameters:

A sequent node assumption.

Description

This primitive inference procedure attempts to use the assumption given as argument to replace the assertion to be proved. In the simplest case, if the given assumption is $\varphi\supset \psi$ and the assertion is $\psi$, then backchain-inference replaces the assertion with $\varphi$. Similarly, if the assertion is $\lnot \varphi$, it is replaced with $\lnot \psi$. The command extends this simplest case in four ways: If IMPS cannot recognize that the terms returned by a match are defined in the appropriate sorts, then these assertions are returned as additional minor premises that must later be grounded to complete the derivation.

  
backchain-backwards-inference

Parameters:

A sequent node assumption.

Description:

This primitive inference procedure works the same way as backchain, except that subformulas of the assumption of the forms s=t, $s\simeq t$, $s\equiv t$ are used from right to left.

  
backchain-through-formula-inference

Parameters:

A sequent node assumption.

Description:

Similar to backchain, except that it does not backchain through equivalences, i.e., formulas of the form s=t, $s\simeq t$, or $s\equiv t.$

  
choice

Parameters:

None.

Description:

This primitive inference procedure implements a version of the axiom of choice.


Conclusion $\Gamma \Rightarrow
\exists f\mbox{:}[\sigma_1,\ldots,\sigma_n,\tau],
\forall x_1\mbox{:}\sigma^{\prime}_{1},\ldots,
x_n\mbox{:}\sigma^{\prime}_{n}, \varphi$
Premise $\Gamma \Rightarrow
\forall x_1\mbox{:}\sigma^{\prime}_{1},\ldots,
x_n\mbox{:...
..._{n},
\exists y_f\mbox{:}\tau,
\varphi[{y_f}/{f(x_1,\ldots,x_n)}]_{\rm all}$


Notes:

  
contraposition

Parameters:

A sequent node assumption $\varphi.$

Description:

This primitive inference procedure interchanges the given sequent's assertion and the assumption $\varphi.$


Conclusion $\Gamma \cup \{\varphi\} \Rightarrow \psi$
Premise $\Gamma \cup \{\neg\psi \} \Rightarrow \neg \varphi$

  
cut

Parameters:

A sequent node to be the major premise.

Description:

Conclusion $\Gamma \Rightarrow \varphi$
Major Premise $\Gamma \cup \{\psi_1,\ldots,\psi_n\} \Rightarrow \varphi$
Minor Premises $(1\leq i \leq n)$ $\Gamma \Rightarrow \psi_i$


Notes:

  
definedness

Parameters:

None.

Description:

This primitive inference procedure applies to a sequent whose assertion is a definedness statement of the form $t\!\!\downarrow$. The primitive inference procedure first tests whether the context entails the definedness of t. If the test fails, the primitive inference then tries to reduce the sequent to a set of simpler sequents.

  
defined-constant-unfolding

Parameters:

Description:

This primitive inference procedure replaces occurrences of the defined constant c at the paths pi by its unfolding e.

  
direct-inference

Parameters:

None.

Description:

This primitive inference procedure applies an analogue of an introduction rule of Gentzen's sequent calculus (in reverse), based on the lead constructor of the assertion of the given sequent.


Conclusion $\Gamma \Rightarrow \varphi \supset \psi$
Premise $\Gamma \cup \{\varphi\} \Rightarrow \psi$
Conclusion $ \Gamma \Rightarrow \varphi_1 \wedge \cdots \wedge \varphi_n$
Premises $(1\leq i \leq n)$ $ \Gamma \cup \{\varphi_1, \ldots ,\varphi_{i-1}\} \Rightarrow
\varphi_i$
Conclusion $ \Gamma \Rightarrow \varphi_1 \vee \cdots \vee \varphi_n$
Premise $ \Gamma \cup \{ \neg \varphi_1 , \ldots , \neg \varphi_{n-1}\}
\Rightarrow \varphi_n$
Conclusion $\Gamma \Rightarrow \varphi \equiv \psi$
Premises $\Gamma \cup \{\varphi\} \Rightarrow \psi$
  $\Gamma \cup \{\psi\} \Rightarrow \varphi$
Conclusion $ \Gamma \Rightarrow \mbox{if-form}(\varphi,\psi,\theta) $
Premises $\Gamma \cup \{\varphi\} \Rightarrow \psi$
  $ \Gamma \cup \{\neg \psi\} \Rightarrow \theta $
Conclusion $ \Gamma \Rightarrow \forall x_1\mbox{:}\sigma_1, \ldots, x_n\mbox{:}\sigma_n,
\varphi$
Premise $ \Gamma \Rightarrow \varphi^\prime$


Notes:

  
disjunction-elimination

Parameters:

A sequent node.

Description:

NO DESCRIPTION.

  
eliminate-iota

Parameters:

A path p to an iota-expression occurrence in the assertion.

Description:

This primitive inference procedure applies to a sequent whose assertion is an atomic formula or negated atomic formula containing a specified occurrence of an iota-expression. The command reduces the sequent to an equivalent sequent in which the specified iota-expression occurrence is ``eliminated.''


Conclusion $\Gamma \Rightarrow \psi$
Major Premise $\Gamma \Rightarrow \exists y\mbox{:}\sigma,
(\varphi[{y}/{x}]_{\rm free} \wed...
...rall z\mbox{:}\sigma, (\varphi[{z}/{x}]_{\rm free}
\supset z=y) \wedge \psi')$
Conclusion $\Gamma \Rightarrow \neg \psi$
Major Premise $\Gamma \Rightarrow \exists y\mbox{:}\sigma,
(\varphi[{y}/{x}]_{\rm free} \wedge
\forall z\mbox{:}\sigma, (\varphi[{z}/{x}]_{\rm free}
\supset z=y)) \supset$
  $\exists y\mbox{:}\sigma,
(\varphi[{y}/{x}]_{\rm free} \supset
\neg\psi')$


Notes:

  
existential-generalization

Parameters:

A sequent node $\Gamma \Rightarrow \varphi$.

Description:

This primitive inference procedure proves an existential assertion by exhibiting witnesses.


Conclusion $\Gamma \Rightarrow \exists x_1\mbox{:}\sigma_1, \dots
,x_n \mbox{:}\sigma_n, \varphi$
Premise $\Gamma \Rightarrow \varphi$


Notes:

  
extensionality

Parameters:

None.

Description:

If the sequent node assertion is an equality or quasi-equality or the negation of an equality or quasi-equality of n-ary functions, this primitive inference applies the extensionality principle.


Conclusion $\Gamma \Rightarrow f=g$
Major Premise $\Gamma \Rightarrow
\forall x_1\mbox{:}\sigma_1, \dots ,x_n\mbox{:}\sigma_n,
f(x_1, \cdots ,x_n) \simeq g(x_1, \cdots ,x_n)$
Minor Premise $\Gamma \Rightarrow f\!\!\downarrow$
Minor Premise $\Gamma \Rightarrow g\!\!\downarrow$
Conclusion $\Gamma \Rightarrow f \simeq g$
Major Premise $\Gamma \Rightarrow
\forall x_1\mbox{:}\sigma_1, \dots ,x_n\mbox{:}\sigma_n,
f(x_1, \cdots ,x_n) \simeq g(x_1, \cdots ,x_n)$
Minor Premise $\Gamma \cup \{g\!\!\downarrow\} \Rightarrow
f\!\!\downarrow$
Minor Premise $\Gamma \cup \{f\!\!\downarrow\} \Rightarrow
g\!\!\downarrow$
Conclusion $\Gamma \Rightarrow \neg f=g$
Premise $\Gamma \Rightarrow
\exists x_1\mbox{:}\sigma_1, \dots ,x_n\mbox{:}\sigma_n,
\neg f(x_1, \cdots ,x_n) \simeq g(x_1, \cdots ,x_n)$
Conclusion $\Gamma \Rightarrow \neg f \simeq g$
Premise $\Gamma \Rightarrow
\exists x_1\mbox{:}\sigma_1, \dots ,x_n\mbox{:}\sigma_n,
\neg f(x_1, \cdots ,x_n) \simeq g(x_1, \cdots ,x_n)$


Notes:

  
force-substitution

Parameters:

Description:

This primitive inference procedure changes part of the sequent assertion. It yields two or more new subgoals. One subgoal is obtained from the original sequent assertion by replacing the subexpression ei at the path pi with ri. The other subgoals assert that the replacements are sound.


Conclusion $\Gamma \Rightarrow \varphi$
Major Premise $\Gamma \Rightarrow \varphi[r_i/e_i]$
Minor Premises $(1\leq i \leq n)$ $\Gamma_i \Rightarrow \varphi_i$


Notes:

  
incorporate-antecedent

Parameters:

A sequent node assumption $\varphi.$

Description:

This primitive inference procedure does the reverse of direct-inference on an implication.


Conclusion $\Gamma \cup \{\varphi\} \Rightarrow \psi$
Premise $\Gamma \Rightarrow \varphi \supset \psi$

  
insistent-direct-inference

Parameters:

None.

Description:

This primitive inference procedure is equivalent to disabling all quasi-constructors and then calling direct-inference.

  
insistent-simplification

Parameters:

None.

Description:

This primitive inference procedure is equivalent to disabling all quasi-constructors and then calling simplification.

  
macete-application-at-paths

Parameters:

Description:

This primitive inference procedure applies the argument macete to the sequent node assertion at those occurrences specified by the paths $p_1, \ldots, p_n$.

  
macete-application-with-minor-premises-at-paths

Parameters:

Description:

This primitive inference procedure applies the argument macete to the given sequent node, in the same way as macete-application, but with the following important difference: whenever the truth or falsehood of a convergence requirement cannot be determined by the simplifier, the assertion is posted as a additional subgoal to be proved.

  
raise-conditional-inference

Parameters:

A list of paths $(p_1, \ldots, p_n)$ to conditional subexpressions.

Description:

This primitive inference procedure will ``raise'' a subset of the conditional expressions (i.e., expressions whose lead constructor is if), specified by the paths pi, in the assertion of the given sequent $\Gamma \Rightarrow \varphi$.

For the moment, let us assume that n=1. Suppose the conditional expression in $\varphi$ located at p1 is the a-th occurrence of $s=\mbox{if}(\theta,t_1,t_2)$ in $\varphi$; the smallest formula containing the a-th occurrence of s in $\varphi$ is the b-th occurrence of $\psi$ in $\varphi$; and the a-th occurrence of s in $\varphi$ is the c-th occurrence of s in $\psi$. If every free occurrence of a variable in s is also a free occurrence in $\psi$, the primitive inference procedure reduces the sequent to

\begin{displaymath}\Gamma \Rightarrow
\varphi[{\mbox{if-form}(\theta,
\psi[{t_1}/{s}]_{c}, \psi[{t_2}/{s}]_{c})}/{\psi}]_{b},\end{displaymath}

and otherwise the primitive inference procedure fails.

Now assume n > 1. The primitive inference procedure will then simultaneously raise each specified occurrence of a conditional expression in $\varphi$, in the manner of the previous paragraph, if there are no conflicts between the occurrences. The kinds of conflicts that can arise and how they are resolved are listed below:

  
simplification

Parameters:

None.

Description:

This primitive inference procedure simplifies the assertion of the given sequent with respect to the context of the sequent. It uses both theory-specific and general logical methods to reduce the sequent to a logically equivalent sequent. The theory-specific methods include algebraic simplification, deciding rational linear inequalities, and applying rewrite rules.

  
simplification-with-minor-premises

Parameters:

None.

Description:

This primitive inference procedure is the same as simplification except that, instead of failing when convergence requirements are not verified, it posts the unverified convergence requirements as additional subgoals to be proved.

  
sort-definedness

Parameters:

None.

Description:

This primitive inference procedure applies to a sequent whose assertion is a definedness statement of the form $(t\downarrow\sigma)$. The primitive inference procedure first tests whether the context entails the definedness of t in $\sigma$. If the test fails, the primitive inference procedure then tries to reduce the sequent to a set of simpler sequents. In particular, when t is a conditional term if $(\varphi,
t_0, t_1)$, it distributes the sort definedness assertion into the consequent and alternative. If t0 and t1 are not themselves conditional terms, the new subgoal has the assertion if-form $(\varphi, (t_0\downarrow\sigma), (t_1\downarrow\sigma))$. If one or both of them is a conditional term, then the sort definedness assertion is recursively distributed into the consequents and alternatives.

  
theorem-assumption

Parameters:

A formula which must be a theorem of the context theory.

Description:

This primitive inference procedure adds the argument theorem to the context of the given sequent.

  
universal-instantiation

Parameters:

A sequent node $\Gamma \Rightarrow
\forall x_1\mbox{:}\sigma_1, \dots ,x_n \mbox{:}\sigma_n, \varphi$.

Description:

This primitive inference procedure proves a formula by proving a universal.


Conclusion $\Gamma \Rightarrow \varphi$
Premise $\Gamma \Rightarrow
\forall x_1\mbox{:}\sigma_1, \dots ,x_n \mbox{:}\sigma_n, \varphi$


Notes:

  
unordered-conjunction-direct-inference

Parameters:

None.

Description:

If the sequent node assertion is a conjunction, this primitive inference procedure does a direct inference without strengthening the context.

Conclusion $ \Gamma \Rightarrow \varphi_1 \wedge \cdots \wedge \varphi_n$
Premises $(1\leq i \leq n)$ $ \Gamma \Rightarrow \varphi_i$

  
weakening

Parameters:

A set of formulas $\Delta.$

Description:

This primitive inference procedure removes one or more assumptions you specify from the context of the given sequent.


Conclusion $\Gamma \cup \Delta \Rightarrow \varphi$
Premise $\Gamma \Rightarrow \varphi$


next up previous contents
Next: 20. The Initial Theory Up: 3. Reference Manual Previous: 18. The Proof Commands
System Administrator
2000-07-23