Plans for Maximacomponents regarding the basic functions for the resolution calculus.
More...
Go to the source code of this file.
Detailed Description
Plans for Maximacomponents 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:

It stands for "partial".

This is rather irrelevant  we often have that.

Furthermore in "resolvable_p" the adjective is false.

However "resolution_literal" is already used.

So we emphasise that we have a list as result.

I.e., "resolvable_p" > "resolution_literal_l".

And "two_subsumption_resolvent_p" > "two_subsumption_resolvent_l".

DONE (false understanding of the issue, and of the Maximalevel) 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 namingpractice.
 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 maximamailinglist) 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.

Perhaps we just sort the ocurring sizes together with their counts, and then output a list of pairs [size, count], sorted by size (ascending).

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 DPvariable 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 monitoringoutput 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.