OKlibrary  0.2.1.6
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.

Todo:
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.
Todo:
Renewal
• 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.
Todo:
DP
• 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.
Todo:
resolution_closure_cs
• 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.
Todo:
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.