Plans regarding the running report of ML.
More...
Go to the source code of this file.
Detailed Description
Plans regarding the running report of ML.
For the PhDdissertation see Annotations/plans/MLDissertation.hpp
 Todo:
 Using homomorphisms in resolution proofs

Obtain an overview on the literature of symmetries in resolution proofs (starting with Krisnamurthy, then Urquhart, then Arai/Urquhart).

Obtain on overview on Szeider's extensions by homomorphisms.

If possible, obtain the journal or conferenceversions (more authoritative than preprints).

Always have complete references (using Latex_bib/TempML.bib, if needed).

Summarise these definitions/results, structuring the discussions by using lemmas, theorems and definitions.

Also relate to our notions and constructions (e.g., different categories).
 Todo:
 Relating isomorphisms of clausesets with isomorphisms of graphs

Consider [The complexity of homomorphisms ..., Buening, Xu] from our point of view, using categories and functors.

Find better proofs!

The reductions of the graph isomorphism problems to isomorphisms of (various types of clausesets) should be possible via the functors from graphs to clausesets.

And for the other direction (finding clausesetisomorphisms via graphisomorphisms) see module Symmetries in the OKlibrary.

One should look at the specific constructions from the paper above (whether they yield something new).

For all the constructions (also for example those in the logicprogrammingpaper) we need to find out whether these are functors (or can be made functors).
 Todo:
 Relations to graph theory

For graph theory we need some nice overviews.

See [Hell, In introduction to the category of graphs].
 Todo:
 Bicliques

For finding "good" bicliques, get some overview on the literature.
 Todo:
 Biclique partitions

Literature overview on complexity/algorithms regarding biclique partitions.
Definition in file RunningReportML.hpp.