RunningReportML.hpp File Reference

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 PhD-dissertation see Annotations/plans/MLDissertation.hpp

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 conference-versions (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).
Relating isomorphisms of clause-sets 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 clause-sets) should be possible via the functors from graphs to clause-sets.
  • And for the other direction (finding clause-set-isomorphisms via graph-isomorphisms) 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 logic-programming-paper) we need to find out whether these are functors (or can be made functors).
Relations to graph theory
  • For graph theory we need some nice overviews.
  • See [Hell, In introduction to the category of graphs].
  • For finding "good" bicliques, get some overview on the literature.
Biclique partitions
  • Literature overview on complexity/algorithms regarding biclique partitions.

Definition in file RunningReportML.hpp.