Basics.hpp File Reference

Plans for Maxima-components regarding the basic functions for the resolution calculus. More...

Go to the source code of this file.

Detailed Description

Plans for Maxima-components regarding the basic functions for the resolution calculus.

resolvable versus resolvable_p
  • We should reconsider the naming scheme used in Satisfiability/Lisp/Resolution/Basics.mac.
  • The only issue here is that in "resolvable_p" and "two_subsumption_resolvent_p" the "_p" is misleading:
    1. It stands for "partial".
    2. This is rather irrelevant --- we often have that.
    3. Furthermore in "resolvable_p" the adjective is false.
    4. However "resolution_literal" is already used.
    5. So we emphasise that we have a list as result.
    6. I.e., "resolvable_p" -> "resolution_literal_l".
    7. And "two_subsumption_resolvent_p" -> "two_subsumption_resolvent_l".
  • DONE (false understanding of the issue, and of the Maxima-level) Currently
    • resolvable(C,D) is a predicate which returns whether C and D are resolvable, and
    • resolvable_p(C,D) returns either the empty list if C and D are not resolvable or a list containing the resolvent if they are.
  • DONE (false understanding) This also occurs with two_subsumption_resolvable (predicate) and two_subsumption_resolvent_p (returns list).
  • Typically, in the Maxima system, the "p" suffix denotes a predicate.
  • DONE ("p" stands not for "predicate", but for "partial") resolvable_p should be a predicate, returning a boolean for consistency.
  • DONE (false understanding) Making resolvable_p a predicate ensures we obey the principle of "least surprise" for the user of the library.
  • DONE (false understanding) Possible solutions:
    • Switch the definitions of resolvable and resolvable_p.
      • This has the disadvantage that it is still not clear from the name what resolvable (previously resolvable_p) returns.
    • DONE (we never use such hacks) Add a notion of "safe" functions which compute the result of a computation and return the empty list otherwise.
      • We could use "safe" or the abbreviation "_sfe".
      • resolvable would be renamed to resolvable_p.
      • resolvable_p would be renamed to resolvable_safe.
      • This would then be applied to the rest of the library.
  • Iterated resolution and DP should go into its own files.
  • Write tests.
  • The partial forms (like resolvable_p) should be supplied throughout.
  • Establish consistent naming-practice.
  • The current implementation of opt_min_dp can be improved if only the minimum or the maximum is sought.
  • DONE (there is only the technical problem that apparently local hash arrays are not recognised by "arrayinfo" and "listarray" ? We should ask about this at the maxima-mailing-list) To make the current implementation worthwhile, perhaps it should show the full distribution of sizes, using a map (size -> count).
  • DONE The output of distribution_min_dp should be further processed, so that easily all information is available.
    1. Perhaps we just sort the ocurring sizes together with their counts, and then output a list of pairs [size, count], sorted by size (ascending).
    2. It seems actually, that "arrayinfo" already returns a sorted list, so that nothing needs to be done.
  • We need also the greedy heuristics, which chooses the DP-variable such that the number of clauses for the next level is minimised.
  • The implementation is very similar to min_resolution_closure_cs: Should we construct a common generalisation?
  • DONE Same regarding monitoring as min_resolution_closure_cs.
min_resolution_closure_cs : DONE
  • DONE As in "Maxima"-"Monitoring" in ComputerAlgebra/plans/general.hpp, perhaps the monitoring-output should be standardised, containing the name of the function?
  • A second output is needed, with the list of c(F_i) for the successive stages. DONE
  • In monitoring mode these numbers are output once a round is completed (compare "Maxima"-"Monitoring" in ComputerAlgebra/plans/general.hpp). DONE

Definition in file Basics.hpp.