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:
 A formula.
 A list of formulas.
 A path represented as a list of nonnegative integers.
 A list of paths.
 A constant.
 A macete.
 Another sequent node (usually referred to as the major premise).
 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.
antecedentinference
A sequent node assumption.
The effect of applying this primitive
inference procedure is given by the following table.
Conclusion 

Premises 



Conclusion 

Premise 

Conclusion 

Premises


Conclusion 

Premises 



Conclusion 

Premises 



Conclusion 

Premise 

Notes:
 Each sequent in the preceding table is of
the form
,
where
is the parameter to the primitive inference procedure.

is obtained from
by renaming the
variables among
which are free in both
and
the original sequent.
backchaininference
A sequent node assumption.
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
and the assertion is ,
then backchaininference replaces the assertion with .
Similarly, if the assertion is
,
it is replaced with
.
The command extends this simplest case in four ways:
 If the assumption is universally quantified, then matching is used to
select a relevant instance.
 If the assumption is a disjunction
then, for any ,
it may be treated as
 If the assumption is of one of the forms s=t, ,
,
if a subexpression of the assertion matches s, then
it is replaced by the corresponding instance of t.
 If the assumption is a conjunction, each conjunct is tried separately,
in turn.
 These rules are used iteratively to descend through the structure of
the assumption as deeply as necessary.
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.
backchainbackwardsinference
A sequent node assumption.
This primitive inference procedure
works the same way as backchain, except that subformulas of the
assumption of the forms s=t, ,
are used from
right to left.
backchainthroughformulainference
A sequent node assumption.
Similar to backchain, except
that it does not backchain through equivalences, i.e., formulas of
the form s=t, ,
or
choice
None.
This primitive inference procedure
implements a version of the axiom of choice.
Conclusion 

Premise 

Notes:

and
have the same type for all
i with
.
 The command fails if there is any occurrence of f in
which is not in an application of the form
.
contraposition
A sequent node assumption
This primitive inference
procedure interchanges the given sequent's assertion and the
assumption
Conclusion 

Premise 

cut
A sequent node to be the major premise.
Conclusion 

Major Premise 

Minor Premises


Notes:
 The major premise is the sequent
definedness
None.
This primitive inference
procedure applies to a sequent whose assertion is a definedness
statement of the form
.
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.
definedconstantunfolding
 A list of paths
to occurrences of a defined
constant c.
 The constant c itself.
This primitive inference procedure replaces
occurrences of the defined constant c at the paths p_{i} by its
unfolding e.
directinference
None.
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 

Premise 

Conclusion 

Premises


Conclusion 

Premise 

Conclusion 

Premises 



Conclusion 

Premises 



Conclusion 

Premise 

Notes:

is obtained from
by renaming the
variables among
which are free in both
and
the context
disjunctionelimination
A sequent node.
NO DESCRIPTION.
eliminateiota
A path p to an iotaexpression
occurrence in the assertion.
This primitive inference
procedure applies to a sequent whose assertion is an atomic formula or
negated atomic formula containing a specified occurrence of an
iotaexpression. The command reduces the sequent to an equivalent
sequent in which the specified iotaexpression occurrence is
``eliminated.''
Conclusion 

Major Premise 

Conclusion 

Major Premise 



Notes:

is an atomic formula.

is the
expression located at the path p in .

is the result of replacing the ith
iotaexpression occurrence in
with y.
 The occurrence of
in
is within some argument component s of .
Moreover, the
occurrence is an extended application component of s, where a is
an extended application component of b if either a is bor b is an application of kind
and a is an extended
application component of a component of b.
existentialgeneralization
A sequent node
.
This primitive inference
procedure proves an existential assertion by exhibiting witnesses.
Conclusion 

Premise 

Notes:
 The command will fail unless the parameter sequent node is of
the form
extensionality
None.
If the sequent node assertion is an
equality or quasiequality or the negation of an equality or
quasiequality of nary functions, this primitive inference applies
the extensionality principle.
Conclusion 

Major Premise 

Minor Premise 

Minor Premise 

Conclusion 

Major Premise 

Minor Premise 

Minor Premise 

Conclusion 

Premise 

Conclusion 

Premise 

Notes:
 If the sorts of f and g are
and
,
respectively, then
for all i with
.
 A sequent node corresponding to a minor premise is not
created if the truth of the minor premise is immediately apparent to
IMPS.
 If f and g are of kind ,
then ``='' is used in
place of ``'' in the premise.
forcesubstitution
 Paths. A list of paths
 Replacements. A list of expressions
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 e_{i} at the path p_{i} with r_{i}. The other subgoals
assert that the replacements are sound.
Conclusion 

Major Premise 

Minor Premises


Notes:

is the local context of
at
the path p_{i}.

is:

if e_{i} is a formula and the parity of the path p_{i} is
0.

if e_{i} is a formula and the parity of the path
p_{i} is 1.

if e_{i} is a formula and the parity of the path p_{i} is 1.

in all other cases.
incorporateantecedent
A sequent node assumption
This primitive inference
procedure does the reverse of directinference on an
implication.
Conclusion 

Premise 

insistentdirectinference
None.
This primitive inference
procedure is equivalent to disabling all quasiconstructors and
then calling directinference.
insistentsimplification
None.
This primitive inference
procedure is equivalent to disabling all quasiconstructors and
then calling simplification.
maceteapplicationatpaths
 A list of paths
 A macete.
This primitive inference
procedure applies the argument macete to the sequent node assertion at
those occurrences specified by the paths
.
maceteapplicationwithminorpremisesatpaths
 A list of paths
 A macete
This primitive inference
procedure applies the argument macete to the given sequent node, in
the same way as maceteapplication, 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.
raiseconditionalinference
A list of paths
to
conditional subexpressions.
This primitive inference procedure will ``raise'' a subset
of the conditional expressions (i.e., expressions whose lead
constructor is if), specified by the paths p_{i}, in the
assertion of the given sequent
.
For the moment, let us assume that n=1. Suppose
the conditional expression in
located at p_{1} is the ath
occurrence of
in ;
the smallest
formula containing the ath occurrence of s in
is the
bth occurrence of
in ;
and the ath occurrence of
s in
is the cth occurrence of s in .
If every
free occurrence of a variable in s is also a free occurrence in
,
the primitive inference procedure reduces the sequent to
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 ,
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:
 If two or more specified occurrences of a conditional expression
s in
are contained in same smallest formula, they are
raised together.
 If two or more specified occurrences of distinct conditional
expressions in
are contained in same smallest formula, at
most one of the occurrences is raised.
 If
and
are the smallest formulas
respectively containing two specified occurrences of a conditional
expression in
and
is a proper subexpression of
,
then the first specified conditional expression is not
raised.
simplification
None.
This primitive inference procedure simplifies the
assertion of the given sequent with respect to the context of the
sequent. It uses both theoryspecific and general logical methods to
reduce the sequent to a logically equivalent sequent. The
theoryspecific methods include algebraic simplification, deciding
rational linear inequalities, and applying rewrite rules.
simplificationwithminorpremises
None.
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.
sortdefinedness
None.
This primitive inference
procedure applies to a sequent whose assertion is a definedness
statement of the form
.
The primitive inference
procedure first tests whether the context entails the definedness of
t in .
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
,
it distributes the sort definedness assertion into the
consequent and alternative. If t_{0} and t_{1} are not themselves
conditional terms, the new subgoal has the assertion
ifform
.
If one or both of them is a conditional term, then the sort
definedness assertion is recursively distributed into the consequents
and alternatives.
theoremassumption
A formula which must be a theorem of
the context theory.
This primitive inference procedure adds the argument
theorem to the context of the given sequent.
universalinstantiation
A sequent node
.
This primitive inference
procedure proves a formula by proving a universal.
Conclusion 

Premise 

Notes:
 The command will fail unless the parameter sequent node is of
the form
unorderedconjunctiondirectinference
None.
If the sequent node assertion is a
conjunction, this primitive inference procedure does a direct inference
without strengthening the context.
weakening
A set of formulas
This primitive inference procedure
removes one or more assumptions you specify from the context
of the given sequent.
Conclusion 

Premise 

Next: 20. The Initial Theory
Up: 3. Reference Manual
Previous: 18. The Proof Commands
System Administrator
20000723