## Ref maintenance notes: SETL source files, packages, and procedures

# EtnaNova_main.stl

- ## prynter:

  auxiliary routines for capturing and transforming "print" statements

  Uses:

  - logic_parser_globals, logic_syntax_analysis_pak,
  - sort_pak, string_utility_pak -- to get user_prefix

  Exports:

  - set_output_phase(n):
  - printy(tup):
    - convert_to_row(stg):
  - unicode_unpahrse(tree): unparse in one of two modes

- ## verifier_top_level:

  top level routines of logic verifier

  *************** Detailed Index, showing procedures ***************

  - (A) ***** Top level parsing procedures *****

    - procedure parse_scenario(file_name,first_proof,last_proof); -- parse a specified Defs_w_proofs file
    - procedure parse_Defs_w_proofs(lines); -- parse the Defs_w_proofs file

  - [A.1] Main program for scenario decomposition into numbered sections

    - procedure parse_file(lines_tup); -- extracts the sequence of definitions, theorems, proofs, and theories from a scenario file -- division of proof lines into "hint" and "body" portions
    - procedure digest_proof_lines(proof_sect_num); -- finds location of ==> in string, if any; position of last character is returned
    - procedure theorem_text(sect_no); -- gets stripped text of theorem
    - procedure definition_text(sect_no); -- gets stripped text of definition

  - [A.2] Collection and numbering of theory sections

    - procedure take_section(now_in,current_section); -- collects section

  - [A.3] Enforcement of special Ref syntactic/semantic rules

    - procedure tree_check(node); -- checks that there are no compound functions, enomerated tuples of length > 2, and unrestricted iterators in setformers
    - procedure get_theorem_name(stg); -- extracts theorem name from string
    - procedure check_theorem_map(); -- check the syntax of all the theorems written to the theorem_map_file

  - [A.4] Interfaces to the native SETL parser

    - procedure parze_expr(stg); -- preliminary printing/diagnosing parse
    - procedure pahrse_expr(stg); -- parse with check of syntactic restrictions
    - procedure collect_fun_and_pred_arity(node,dno); -- collect the arity of functions and predicates (main entry)
    - procedure collect_fun_and_pred_arity_in(node,bound_vars); -- collect the arity of functions and predicates (workhorse)

  - (B) ***** Master control of in-proof inferencing and related utilities *****

    - [B.0] Initial read-in of digested proof and theory related files

      - procedure read_proof_data(); -- ensure that the list of digested_proofs,
      - procedure init_proofs_and_theories();
      - procedure check_proofs(list_of_proofs); -- check ELEM and discharge inferences in given range

    - [B.1] Master entry for checking inferences in a single proof

      - procedure check_a_proof(proofno); -- read a given proof and check all its inferences

    - [B.2] conjunction building for inference checking

      - procedure form_elem_conj(hint,statement_stack); -- build conjunction to use in ELEM-type deductions
      - procedure build_conj(citation_restriction,statement_stack,final_stat); -- context-stack to conjuction conversion for inferencing in general

    - [B.3] Definition checking

      - procedure check_definitions(start_point,end_point); -- check the definition citation inferences in the indicated range -- Checking of recursive definitions
      - procedure recursive_definition_OK(symbdef,arglist,right_part); -- check a recursive definition for syntactic validity
      - procedure recursive_definition_OK_in(node,var_bindings); -- check a recursive definition for syntactic validity (inner workhorse)

    - [B.4] Removal of internal labels from proof lines

      - procedure drop_labels(stg); -- finds location of Statnnn: in string, if any. These labels are dropped, and positions of first characters are returned

    - [B.5] Interface to the MLSS routines

      - procedure test_conj(conj); -- test a conjunct for satisfiability
      - procedure show_conj();
      - procedure conjoin_last_neg(stat_tup); -- invert the last element of a collection of clauses and rewrite using 'ands'
      - procedure conjoin_last_neg_nosemi(stat_tup);
      - procedure conjoin_last(stat_tup); -- rewrite a collection of clauses and using 'ands'
      - procedure collect_conjuncts(tree); -- extract all top-level terms from a conjunction
      - procedure collect_equalities(tree); -- extract all top-level collect_equalities from a conjunction

    - [B.6] Routine to disable/enable checking of particular classes of inference

      - procedure disable_inferences(stg); -- disables and re-enables the various kinds of inferences

  - (C) ***** Library of routines which handle details of individual inference classes *****

    - [C.1] Discharge inference checking

      - procedure check_discharge(statement_stack,prior_suppose_m1,stat_in_discharge,discharge_stat_no,hint);

    - [C.2] Statement citation inference checking

      - procedure check_a_citation_inf(count,statement_cited,statement_stack,hbk,citation_restriction,piece);

    - [C.3] Theorem citation inference checking

      - procedure check_a_tsubst_inf(count,theorem_id,statement_stack,hbk,piece,statno); -- check a single tsubst inference

    - [C.4] Equality inference checking

      - procedure check_an_equals_inf(conj,stat,statement_stack,hint,stat_no); -- handle a single equality inference
      - procedure extract_equalities(conj); -- extract and arrange all top-level equalities and equivalences from a conjunction

    - [C.5] Algebra inference checking

      - procedure check_an_algebra_inf(conj,stat); -- handle a single algebraic inference
      - procedure alg_node_bottoms(tree,plus_op); -- return list of algebraic node base elements for given node
      - procedure alg_node_bottoms_in(tree,plus_op); -- recursive workhorse

    - [C.6] Simplification inference checking

      - procedure check_a_simplf_inf(statement_stack,stat,stat_no,hint,restr); -- handle a single set-theoretic standardization inference

    - [C.7] Use_def inference checking

      - procedure check_a_use_def(statement_stack,stat,theorem_id,hint,j); -- check a single Use_def inference
      - procedure get_symbol_def(symb,thry); -- get the definition of a symbol, in 'thry' or any of its ancestors

    - [C.8] Suppose_not inference checking

      - procedure check_suppose_not(supnot_trip,pno,th_id); -- check the suppose_not inferences in the indicated range

    - [C.9] Monotonicity inference checking

      - procedure check_a_monot_inf(count,statement_stack,hbk,theorem_id); -- check a single Set_monot inference

    - [C.10] Loc_def inference checking

      - procedure check_a_loc_def(statement_stack,theorem_id); -- check a single Loc_def inference

    - [C.11] Assumption inference checking for theorems within theories

      - procedure check_an_assump_inf(conj,stat,theorem_id); -- handle a single 'Assumption' inference

    - [C.12] THEORY application inference checking (outside proofs)

      - procedure check_an_apply_inf(next_thm_name,theory_name,apply_params,apply_outputs);
      - procedure check_apply_syntax(text_of_apply); -- special processing for global definitions by "APPLY" -- APPLY conclusion checking (for THEORY application outside proofs)
      - procedure test_conclusion_follows(next_thm_name,desired_concl); -- test desired conclusion of a top-level APPLY inference

    - [C.12a] THEORY application inference checking (within proofs)

      - procedure check_an_apply_inf_inproof(thm_name,stat_stack,theory_name,apply_params,apply_outputs); -- Syntax checking for THEORY application
      - procedure test_apply_syntax(theory_name,apply_params,apply_outputs); -- Analysis of APPLY hints within proofs
      - procedure decompose_apply_hint(hint); -- decomposes the 'hint' portion of an APPLY statement -- Finding the variables to be sustituted for APPLY _thryvars
      - procedure get_apply_output_params(apply_outputs,hint); -- decompose and validate apply_outputs, returning them as a tuple of pairs

    - [C.13] Skolemization inference checking (outside proofs)

      - procedure check_a_skolem_inf(next_thm_name,theorem_to_derive,apply_params,apply_outputs);
      - procedure check_skolem_conclusion_tree(desired_conclusion,apply_params,apply_outputs);
      - procedure build_Skolem_hypothesis(desired_conclusion,tree,split_apply_outputs);

    - [C.13a] Skolemization inference checking (within proofs)

      - procedure check_a_Skolem_inf_inproof(stat_stack,theory_name,apply_params,apply_outputs);
      - procedure conclusion_follows(theory_name,apply_outputs,apply_params_parsed,conclusion_wanted);
      - procedure build_required_hypothesis(hypotheses_list,apply_params_parsed);
      - procedure def_as_eq(symb,args_and_def); -- rebuild a definition as an equality or equivalence
      - procedure tree_is_boolean(tree); -- test a tree to see if its value is boolean

  - (D) ***** Interfacing to external provers *****

    - [D.1] Interface to 'Otter' prover

      - procedure check_an_external_theory(th,assumed_fcns,assumps_and_thms); -- check declaration of an external THEORY
      - procedure otter_clean(line); -- removes otter comments and forumla_to_use lines
      - procedure check_an_otter_theory(th,assumed_fcns,assumps,thms); -- check declaration of an otter THEORY
      - procedure suppress_thryvar(stg); -- suppresses all instances of '_THRYVAR' in string
      - procedure otter_to_ref(otter_item,otfile_name); -- converts an otter item to SETL syntax; returns unparsed tree or OM

  - (E) ***** Miscellaneous utilities *****

    - [E.1] Formula feature search utilities

      - procedure find_free_vars_and_fcns(node); -- find the free variables and function symbols in a tree (main entry)
      - procedure find_free_vars_and_fcns_in(node,bound_vars); -- find the free variables in a tree (recursive workhorse)
      - procedure find_quantifier_bindings(node); -- find the variable bindings at the top of an iterator tree
      - procedure list_of_vars_defined(theory_in,kind_hint_stat_tup); -- find the ordered list of variables defined in a proof
      - procedure trim_front(stg); -- removes leading whitespace
      - procedure front_label(stg); -- finds prefixed Statnnn: in string, if any and returns it
      - procedure loc_break(stg); -- finds location of ==> in string, if any; returns pos. of last character
      - procedure split_at_bare_commas(stg); -- splits a string at commas not included in brackets
      - procedure trim(line); -- trim off whitespace
      - procedure paren_check(stg); -- preliminary parenthesis-check
      - procedure find_defined_symbols(); -- extracts the sequence of definitions, theorems, and theories from a scenario file
      - procedure strip_quants(tree,nquants); -- strip a specified number of quantifiers from a formula
      - procedure strip_quants_in(tree,nquants); -- strip a specified number of quantifiers from a formula
      - procedure setup_vars(il,offs); -- 'offs' flags nature of variable returned (universal or existential)
      - procedure conjoin_iters(list_of_iters,quant_body); -- conjoin list of iterators to formula body
      - procedure ordered_free_vars(node); -- find the free variables in a tree, in order of occurrence (main entry)
      - procedure ordered_free_vars_in(node,bound_vars); -- find the free variables in a tree (recursive workhorse)
      - procedure remove_arguments(node,fcn_list); -- remove arguments from list of functions
      - procedure remove_arguments_in(node,fcn_list,bound_vars); -- remove arguments from list of functions (recursive workhorse)
      - procedure symbol_occurences(tree,symbol_list);
      - procedure symbol_occurences_in(node,symbol_list,bound_vars);
      - procedure free_vars_and_fcns(thm); -- get all the free variables and functions of a theorem
      - procedure fully_quantified(theory_nm,thm); -- construct the fully quantified form of a theorem in a theory
      - procedure fully_quantified_external(theory_nm,thm);
      - procedure freevars_of_theorem(theory_nm,thm); -- find the quantifiable free variables of a theorem, given theory
      - procedure not_all_alph(stg);

    - [E.2] Utilities for statistical analysis of the proof scenarios

      - procedure get_hints(proofno1,proofno2); -- examine the hints which occur in a given range of proofs and report statistics
      - procedure view_theorem_citations(proofno1,proofno2); -- count the number of theorem citations in a given range, and print them
      - procedure inspect_proofs(tup_of_numbers); -- inspect a specified list of proofs, from digested_proof_file

  - (F) ***** Test Program collection for Ref top level routines *****

    - procedure do_tests3(); -- do tests for this package
    - procedure test_check_a_skolem_inf; -- test of check_a_skolem_inf function
    - procedure test_check_an_apply_inf; -- test of check_an_apply_inf function

  Uses:

  - string_utility_pak, get_lines_pak, parser, sort_pak
  - logic_syntax_analysis_pak, proof_by_computation, logic_syntax_analysis_pak2, logic_parser_globals, prynter, algebraic_parser, proof_by_structure

  Exports:

  - verifier_invoker(uid): master invocation routine
    - parse_Defs_w_proofs(lines_tup): parse a raw scenario, producing all the files used subsequently
      - parse_file(lines_tup): extracts the sequence of definitions, theorems, proofs, and theories from a scenario file
        - take_section(now_in,current_section): collects section
        - digest_proof_lines(proof_sect_num): digests the proof lines into triples
        - theorem_text(sect_no): gets stripped text of theorem
        - definition_text(sect_no): gets stripped text of definition
    - -- parse_scenario(file_name,first_proof,last_proof): parse a specified Defs_w_proofs file -- DISABLED
    - pretty_theorem(theorem_num): returns [thm_name (with 'T'),thm_statement,thm_proof (digested into pairs)]
      - pretty_line(proof_line_pair): create the pretty version of a single proof line
        - unicode_apply_param(stg_param): convert item from theory application substitution list to Unicode form
        - to_unicode(stg_piece,lab): convert piece of formula, possibly ending in ampersand, to unicode
  - disable_inferences(stg): disables and re-enables the various kinds of inferences -- include a "*" in the list to disable by default
  - find_defined_symbols(): extracts the sequence of definitions, theorems, and theories from a scenario file
  - collect_fun_and_pred_arity(node,dno): collect the arity of functions and predicates (main entry)
  - test_conj(conj): test a conjunct for satisfiability
  - check_proofs(list_of_proofs): check all inferences in given range
    - prepare_theorem_templates(): convert the theorem_map into a map "theorem_templates" of theorem names into pairs
  - check_suppose_not(supnot_trip,pno,th_id): check the indicated suppose_not inference (initial statements of proof)
  - check_definitions(start_point,end_point): check the definitions in the indicated range
  - check_an_equals_inf(conj,stat,statement_stack,hint,stat_no): handle a single equality inference
    *********** lower-level routines ***********
  - strip_quants(tree,nquants): strip a specified number of quantifiers from a formula
    *********** auxiliaries for having a glimpse at the digested_proof_file and related items ***********
  - inspect_proofs(tup_of_numbers): inspect a specified list of proofs, from digested_proof_file and the
  - get_hints(proofno1,proofno2): read the hints which occur in a given proof
  - view_theorem_citations(proofno1,proofno2): count the number of theorem citations in a given range, and print them
    *********** procedures for APPLY inference checking ***********
  - check_a_skolem_inf(next_thm_name,theorem_to_derive,apply_params,apply_outputs): checks a skolem inference
  - check_an_apply_inf(next_thm_name,theory_name,apply_params,apply_outputs): checks a non-skolem APPLY inference
  - ordered_free_vars(node): find the free variables in a tree, in order of occurrence (main entry)
    *********** procedures for ALGEBRA inference checking ***********
  - check_an_algebra_inf(conj,stat): handle a single algebraic inference
  - alg_node_bottoms(tree,plus_op): return list of algebraic node base elements for given node
    *********** procedures for external prover interface ***********
  - otter_to_ref(otter_item,otfile_name): converts an otter item to SETL syntax
    ********** Miscellaneous utilities **********
  - read_range(stg): convert to list of proofs to be printed; force range indicator to legal form and return it
  - --first_last(stg): reduce dotted ranges to first and last elements, and read
    *********** test procedures ***********
  - miscellaneous_tests(): repository for miscellaneous top-level logic verifier tests under development

  Not exported, exploited by more than one procedure inside the package:

  - read_proof_data(): ensure that the
    - list of digested_proofs,
    - the theorem_map of theorem names to theorem statements,
    - the theorem_sno_map_handle of theorem names to theorem statements,
    - its inverse inverse_theorem_sno_map,
    - the theory-related maps parent_of_theory,theors_defs_of_theory,assumps_and_consts_of_theory
    - defs_of_theory,defsymbs_of_theory,defconsts_of_theory,
    - and the theory_of map sending each theorem and definition into its theory
    - the theorem_list, and the theorem_name_to_number (list of theorem names in order, and inverse)
    are all available

  - parze_expr(stg): preliminary printing/diagnosing parse
  - pahrse_expr(stg): parse with check of syntactic restrictions -- called initially in place of parse_expr, to enforce Ref syntactic rules

# EtnaNova_ELEM_collection.stl

*********** This file contains most of the logic system code ***********
It consists of four packages, the first two quite short, the final one long. The first package merely concentrates various global variables used in this file (some of which are accessed externally). The third package contains many of the principal logic system procedures, plus an extensive collection (1300 lines) of direct tests of these routines, used in debugging them, and potentially useful for reversion testing.

- ## logic_parser_globals:

  This is a package of global variables used by logic parser and other basic packages.
  (Just variables and constants, the body is empty).

- ## logic_parser_aux:

  Uses:

  - logic_parser_globals: global variables for logic parser and other basic packages

  Exports:

  - build_model(membs_inv,givn_vars,sorted_membs): build a model for a saturated set of memberships
  - set_rep(n): returns the set representation of an integer (memoized using globals)

- ## logic_syntax_analysis_pak:

  syntax analysis routines for logic system, supplements to syntax analysis and syntactic inference mechanisms

  *************** Detailed Index, (not yet) showing procedures ***************

  - Section (1): utilities
    - (1.1) utility parse and print routines
    - (1.2) topological sort of strings
  - Section (2): logic procedures proper (approx. 4800 lines)
    - (2.1) blobbing routines, which prepare for use of the battery of decision algorithms
    - (2.2) routines intermediate between blobbing and MLSS inference proper
    - (2.3) simplifications of various built-in operations
    - (2.4) additional special simplifications, for use with the ELEM decision routines
    - (2.5) propositional-level simplifications involving the signs of propositional variables
    - (2.6) direct interfaces between blobbing and the 'ELEM' logical inference mechanism
    - (2.7) analysis of formulae for monotonicity
    - (2.8) auxiliary routine for standardizing chains of associative operators
    - (2.9) routines which handle 'algebraic' deduction
    - (2.10) substitution routines: replace free variables in a formula by specified expression
    - (2.11) simplification of setformers (these routines are invoked by the 'SIMPLF' hint)
    - (2.12) equality inference routines (these routines are invoked by the 'EQUAL' hint)
  - Section (3): additional utilities

  Uses:

  - string_utility_pak, parser, sort_pak: various auxiliary packages used. 'parser' is the standard SETL parser
  - logic_parser_globals: global variables for logic parser and other basic packages
  - logic_parser_aux: auxiliary routines for logic basic routines
  - proof_by_computation: proof_by_computation routines
  Exports:
  - init_logic_syntax_analysis(): initialize for logic syntax-tree operations.
    This setup procedure must be called (just once!) before any parsing begins: it just sets up a map of standard SETL syntactic markers to more readable abbreviated forms of the same.
  - parze_expr(stg): print source; then parse
  - unparse(tree): puts a tree back into string format
  - apparently_pred(tree): routine determining wheter an expression is a predicate or not
  - unicode_unparse(tree): puts a tree back into a unicode version of its original string format
  - convert_to_unicode(stg): convert a formula to unicode
  - cleanup(parse_tree): simplifies the parse_tree; returns string
  - clean_tree(parse_tree): simplifies the parse_tree; returns tree
  - dump_tree(parse_tree): dumps the parse_tree in indented format
  - dump_in(parse_tree,indent): recursive workhorse for dump-tree
  - prant(stg): auxiliary compressing print
  - end_prant(): terminates compressing print sequence
    ********** srecursive tree-walkers, which detect and summarize various aspects of syntax trees **********
  - standardize_bound_vars(formula): standardize the bound variable names in a formula
  - standardize_bound_vars_noad(formula): standardize the bound variable names in a formula, restarting bound variable names counter
  - drop_parens(stg): drop some unnecessary parens
  - tree_starts(treetop_tup,node): tests the structure of the top of a tree
  - flatten_same_ops(node): get the chain of all identical infix operations starting at a given node at which this operation appears
  - ----* defmemb(tree1,tree2,substitution_map): check validity of a defmemb deduction involving a quantified statement or a set membership relation
  - substitute(tree,substitution_map): makes substitutions for specified free variables of a formula. (main entry; uses workhorse)
  - substitute_in(tree,substitution_map,bound_vars): inner recursive workhorse of substitution routine
  - gen_name(rw name_ctr): generate a new blob name
  - ----* check_definition(tree,symbols): check a recursive or nonrecursive definition for validity
  - ----* check_pred_definition(tree,statement,symbols): checks skolem-type definition for validity
  - ----* range_blob(node): this blobs a set expressions and quantifiers down functions involving basic set-theretic operators -- which may be amenable to specialized decison algorithms
  - find_free_vars(node): find the free variables in a tree (main entry)
  - find_free_vars_in(node,bound_vars): find the free variables in a tree (recursive workhorse)
  - find_free_vars_from(node,bound_vars): find the free variables in a tree (alternative main entry, used by blob_to_monotone)
  - find_bound_vars(node): find the bound variables at the top of an iterator tree
  - find_all_vars(node): find all the variables in a formula
  - find_iterators(node): find the iterator list at the top of an iterator tree
  - new_name(stg,nameset): generates new names for bound variables during a simplification operation
  - simplify_setformer(tree): removes specified membership iterators over setformer expressions
  - top_sort_stgs(G): topological sorting procedure. G is a dependency graph for a set of strings; used to sort iterators
    ********** formula blobbing **********
  - blob_tree(tree): blobs a tree down to extended MLSS (other versions will also be needed); top entry
  - get_blob(stg): once a tree has been blobbed to a structured string, this routine looks it up -- in the collection of all such strings, to determine its blob number
  - blob_tree_in(node): blobs a tree down to extended MLSS; recursive workhorse
  - blob_to_string(node,bound_vars,name_ctr): blobs a tree down to a string (main subroutine for blob_tree_in)
  - boil_down_blobbed(tree): this vital routine removes useless clauses from the blobbed version of a formula -- performs simplify_builtins, simplify_onces, exploit_prop_sign in order
  - simplify_builtins(tree): simplifies various expressions involving built-in operators
    ********** interface to the "ELEM" logical inference mechanism **********
  - model_blobbed(formula): models a blobbed mlss formula, or pronounces it unsatisfiable by returning OM
  - decompose_post_blobbing(formula): decomposition procedure for formulae blobbed to a decidable language
  - Davis_Putnam(clause_set,term_decider,td_prms): Extended Davis-Putnam procedure for verifying propositional consistency.
  - mlss_decider(truth_value,td_params): tableau-based term decider for mlss
  - find_repmap(equalities): find mapping of items to representatives for a set of equalities
  - reduce_by_repmap(items,repmap): reduce a set of tuples using a mapping of items to representatives
    ********** interface to the "ALGEBRA" logical inference mechanism **********
  - enable_algebra(operator_list,context): enables elementary algebraic deduction for elements of a set and operators on it
  - algebra(formula,context): handles elementary algebraic deduction
  - standardize_formula(poly_tree,op_obj_tup): standardizes a polynomial tree belonging to a specified algebraic theory
  - check_member(blob_tree,alg_objects_set,context):
    ********** interface to the "DIFFERENCE" logical inference mechanism **********
  - verify_equality(tree1,tree2,context,is_pred): verifies equality or equivalence of two formulae (main entry)
  - verify_equality_in(tree1,tree2,bound_vars_with_ranges,context,is_pred): verifies equality or equivalence of two formulae (workhorse)
  - flatten_universal(node): get the chain of universal quantifiers starting at a given node a first universal appears
  - flatten_existential(node): get the chain of all existential quantifiers starting at a given node a first existential appears
  - common_iter_len(list_of_iters_1,list_of_iters_2,body_1,body_2): find the iterator portions which are of the same types
  - build_quantified_version(formula,bnd_vars_with_ranges): add appropriate quantifiers to a formula
    ********** monotonicity interface **********
  - post_monotone(op_and_arg_string): note the monotonicity property of one or more function symbols
  - drop_monotone(ops): drop the monotonicity property of one or more function symbols
  - -- monotone_inference(node1,node2): [MOVED] calculates conditions for value defined by node 1 to include value defined by node 2 [MOVED TO logic_syntax_analysis_pak2]
    *********** Test Collection ***********
  - test_basic_parses): view parse trees of basic constructions
  - test_standardize_bound_vars): tests of standardize bound variables function
  - test_blob_to_string(): tests of blob_to_string function
  - test_blobbing(): test the blob_tree function
  - test_top_sort_stgs(): test the top_sort_stgs function
  - unparse_test(): test unparse operation
  - blobstring_tests(): direct test of blobstring operation
  - test_find_bound_vars(): test the "find_bound_vars" operation, for setformer and iteration nodes
  - test_find_free_vars(): test the "find_free_vars" operation, for setformer and iteration nodes
  - -- test_monotone_inference(): [MOVED] test of the monotone_inference procedure [MOVED TO logic_syntax_analysis_pak2]
  - test_simplify_setformer(): test the simplify_setformer routine
  - test_bool_exp(stg,fcn): check agreement of davis_putnam and truth-table for 4-variable boolean expressions
  - small_mlss_test(): initial explicit test of mlss decider
  - test_model_blobbed(): initial tests and timing of the mlss verifier
  - test_build_quantified(): test of "build_quantified_version" routine
  - test_algebra(): initial tests of ALGEBRA deduction
  - test_equality_inference(): initial tests of equality inferencing
  - test_equality_more(): supplemental equality tests
  - timing_tests(): a few tests of MLSS timing
  - test_mls(): Eugenio's collection of MLS tests
  - substitution_test(): substitution test
  - test_find_diffs(): test of "find_diffs" procedure
  - test_simplify_builtins(): test of special simplifications for builtin operators
  - test_simplify_onces(): test of special simplifications for variables appearing once
  - test_count_free_vars(): test of count_free_vars routine
  - test_find_prop_signs(): test of search routine for propositional variables of one sign
  - test_exploit_prop_signs(): test of search routine exploiting propositional variables of one sign
  - test_boil_down_blobbed(): test overall simplification of blobbed expression
  - test_proof_by_computation(): proof by computation test
    *********** decision algorithm tests ***********
  - test_Davis_Putnam(): test the Davis_Putnam propositional decision algorithm

- ## proof_by_computation:

  Uses:

  - string_utility_pak,
  - logic_syntax_analysis_pak, logic_parser_aux, logic_parser_globals
  Exports:
  - compute_check(tree): main proof by computation routine
  - test_equality(u,v): recursive test for object equality
  - test_membership(u,v): test for object membership
  - set_encoding(n): compute the set encoding of an integer n
  - map_comp_simplif(tree): simplify a map composition (see comment attached to code)

# EtnaNova_ELEM_supplement.stl

- ## logic_syntax_analysis_pak2:

  second part of logic_syntax_analysis_pak

  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:

  - string_utility_pak,parser,sort_pak: standard Setl utilities
  - logic_parser_globals: global variables for logic parser and other basic packages
  - logic_parser_aux: auxiliary routines for logic basic routines
  - logic_syntax_analysis_pak: use the main package of inferencing routines

  Exports:

  *********** Monotonicity-based inference ***********
  - monotone_infer(node): prepare to deduce a formula by monotone inference -- called from "check_a_monot_inf" in top-level package
  - test_monotone_infer(): test of the monotone_infer procedure
    *********** Algebraic inference ***********
  - find_algebraic_nodes(tree): finds the algebraic nodes in a tree, and returns them
  - standardize_subtree(tree,plus_op):
  - re_nest(flattened_tree): reconvert a standardized (flattened) tree to its ordinary 'nested' form
  - canorder_subtree(tree): sorts the terms and factors of a standardized (flattened) subtree and performs cancellations
  - generate_algebraic_identity(tree): generates identity of tree with standardized form
  - find_ring_members(tree): collects the ring membership assertions at the top conjuctive level of a tree
  - post_alg_roles(stg): adds an algebraic set to alg_of and alg_role_of maps
    *********** Miscellaneous tree searching and transformation routines ***********
  - find_setformers_and_quants(tree): finds the setformer and quantifier nodes in a tree, and returns them
  - find_fnc_symbs(node): find the function symbols in a tree
  - dequantify(tree,substitution_tup): general substitution for quantified variables
  - replace_fcn_symbol(expn,symbol,symbvars,symbdef)): at each occurrence of a symbol in expn, finds the arguments of symbol, and substitutes them in symbdef for the indicated free variables of symbdef replacing the symbol occurrence by this substituted form
    *********** Test Collection ***********
  - test_find_fnc_symbs(): test of the find_fnc_symbs procedure
  - test_replace_fcn_symbol(): test of the replace_fcn_symbol procedure
  - test_dequantify(): test of the dequantify procedure
    *********** Obsolete code ***********
  - monotone_inference(node1,node2): [OBSOLETE]
  - test_monotone_inference(): test of the monotone_inference procedure -- calculates conditions for value defined by node 1 to include value defined by node 2 [OBSOLETE]

- ## proof_by_structure:

  Uses: parser, string_utility_pak, logic_syntax_analysis_pak, logic_syntax_analysis_pak2

  Exports:
  - extract_relevant_descriptors(conj_tree): This is the main routine of the the proof_by_structure system.

    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.

    - init_proof_by_structure(): This procedure does some basic initializations of the maps: const_properties and m_descritors_of_basic.

      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.

    - extract_relevant_conjuncts(tree): (wrapper) Walk the tree, collecting the relevant top-level conjuncts. The relevant conjuncts are those stating membrship or inclusion of one variable in another
      - extract_relevant_conjuncts_in_new(tree): internal recursive workhorse
      RETURNS [memb_conjs, inc_conjs, equality_conjs]
      1. memb_conjs: conjuncts designating membership: will be collected as pairs;
      2. inc_conjs: conjuncts designating inclusion: will be collected as pairs
      3. equality_conjs: conjuncts designating equalities to setformers: will be collected as pairs
    CONSTRUCTS vars_to_descriptors
    A set valued map which for every variable gives gives its set of descriptors.

  - expression_descriptor(expn_stg,vars_to_descriptors): This is a counterfeited main routine of the the proof_by_structure system, possibly useful for ad hoc debugging.

  - expression_descriptor_in(expn_stg,vars_to_descriptors): debugging wrapper
    - expression_descriptor_inn(expn_stg,vars_to_descriptors): Calculates result descriptor set given an expression in the form of string (to be internally parsed into a tree) and the descriptors applicable to its free variables.

      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:

      - descriptor_action_of_pow(descriptor_set):
      - descriptor_action_of_Un(descriptor_set):
      - descriptor_action_of_union(descriptor_set1,descriptor_set2):
      - descriptor_action_of_intersection(descriptor_set1,descriptor_set2):
      - descriptor_action_of_difference(descriptor_set1,descriptor_set2):
      - descriptor_action_of_range(descriptor_set):
      - descriptor_action_of_domain(descriptor_set):
      - descriptor_action_of_arb(descriptor_set):
      - descriptor_action_of_pair(descriptor_set1,descriptor_set2):
      - descriptor_action_of_car(descriptor_set):
      - descriptor_action_of_cdr(descriptor_set):
      - descriptor_action_of_count(descriptor_set):
      - descriptor_action_of_cartprod(descriptor_set1,descriptor_set2):
      - descriptor_action_of_funcprod(descriptor_set1,descriptor_set2):
      - descriptor_action_of_func_inv(descriptor_set):
      - descriptor_action_of_func_ident(descriptor_set): UNUSED
  - get_assertions_from_descriptors(vars_to_descriptors): convert descriptors to set membership assertions

    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

    - Za, Re, Card, Ord, and the other elementary sets, which translate into x in Za, x in Re, Card(x), Ord(x), etc.;
    - {Za}, {Re}, {Card}, {Ord}, which translate into x ¥incin Za etc.;
    - {{Za}}, {{Re}}, etc., which translate into x ¥incin pow(Za) etc.;
    - Fin and Countable, which become Finite(x) and Countable(x);
    - Infin which becomes not Finite(x);
    - NonNull, which becomes x /= 0;
    - we also handle Svm and one_1_map.

- ## algebraic_parser:

  package for simple algebraic parsing

  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:

  - alg_parse(stg): the parsing routine
  - setup_parse_priorities_and_monadics(pri_map,mon_set,refversion): set up the priorities and monadics for algebraic test parsing