Uses:
Exports:
Uses:
Exports:
Not exported, exploited by more than one procedure inside the package:
Uses:
Exports:
syntax analysis routines for logic system, supplements to syntax analysis and syntactic inference mechanisms
Uses:
Uses:
This package is a supplement to the main package "logic_syntax_analysis_pak",
separated out only because that other file was becoming uncomfortably large.
The processes found here handle monotone and algebraic inference, and several utilities
as seen in the header below.
It is also used as a repository for obsolete versions of inference and related codes.
Uses:
Exports:
Uses: parser, string_utility_pak, logic_syntax_analysis_pak, logic_syntax_analysis_pak2
Exports:Extracts relevant descriptors given tree of a conjunction.
This involves information concerning membership, equality, and inclusion; also particular predicates.
It looks for Ref clauses of various forms directly expressible as descriptors, and collects these descriptors into a set which is returned.
The clauses which can be handled in this way, and their translations, are x in Za, x in Re, Card(x), Ord(x), and in the other elementary sets, which translate into Za, Re, Card, Ord, etc.; x incin Za etc., which translate into
{Za}, {Re}, {Card}, {Ord}, etc. Finite(x) and Countable(x), which become Fin and Countable; not Finite(x) which becomes Infin;
and x /= 0 which becomes NonNull. This extraction is iterated twice to handle cases like 'x in n and n in Za', and also handles cases like 'x /= 0 and y incs x' and 'Finite(x) and x incs y'. We also handle Svm and one_1_map.
Note that this routine works with variables only, not with subexpressions, so in some cases local variables will need to be defined in proofs and properties stated for these variables.
More specifically, for every basic descriptor d in the domain of const_properties, it also adds the descriptor {d}.
For every descritor d in the range of m_descritors_of_basic, if d has a descriptor associated to its members (through the map descritors_of_basic), it also adds this descriptor to m_descritors_of_basic.
We are concerned here with expressions of two
principal kinds, simple expressions and setformer expressions.
Simple expressions are processed recursively, descriptors being attached to all their nodes from bottom to top
in accordance with the expressions found at each node.
Conditional expressions of the form 'if c1 then e1 elseif c2 then e2.. end if' are treated as intersections of
their 'e' parts; set-theoretic expressions have the form {e(x,y,..): x in s1, y in s2 | C } etc.
We collect relevant clauses from the condition part C, and then calculate descriptors for all of the bounding sets
s1, s2,... This gives us descriptors for their members x,y,.., which are then used to calculate
a descriptor set D for e(x,y,..). The setformer then gets the descriptor {D}, to which Fin and Countable
are attached if all the s1, s2,... have these descriptors, and NonNull is attached if all the sj are NonNull
and the condition C is missing.
The specialized procedures which are used to get the type of an expression are:
Convert descriptors to set membership assertions for use in ELEM deductions. This looks for descriptors of various forms directly expressible as Ref clauses, and generates these clauses. The descriptors which can be handled in this way, and their translations, are
This is an auxiliary package for simple algebraic parsing, useful for communicating with external provers which use only a simple algebraic language, but possibly with operator signs and precedences different from those meeting the standard SETL syntactic conventions.
Uses: string_utility_pak, get_lines_pak, sort_pak
Exports: