define Hets core functionality

[tillmo]

Define a list of Hets core functionalities. These should be covered with tests and be provided by an internal API, see #1790. In a next step, interfaces should provide this core functionality (only), and an --experimental flag could be used to have more functionality. There should be two Ubuntu prover packages: one for the core, one for the non-core provers. In this way, Hets will become easier to use and will have fewer bugs. The core functionality should include:

• logics CASL, OWL, Common Logic, TPTP
• suitable comorphisms for these
• suitable provers: Vampire, Eprover, SPASS, Pellet, Fact, Leo-II, Satallax, Zipperposition
• suitable consistency checkers: Darwin, Vampire
• output logics, comorphisms, provers
• the DOL language
• Parsing, printing, static analysis of documents, computation of a library env with development graphs
• output library env as XML
• auto command for a development graph (shifts proof obligations from edges to nodes)
• select a node from a DG (if there is a unique node of a unique DG, it will be preselected)
• for the current (or an explicitly specified) node:
  • output node type
  • output signature
  • output theory and proof obligations
  • output logic and sublogic
  • translate theory along comorphism
  • select prover and axioms to use
  • select consistency checker
  • set time limit
  • prove, output proof
  • check consistency, output model
  • for an edge in the DG, display edge type, comorphism (if not identity) and signature morphism

[mcodescu]

I like this idea very much. I just wonder if we currently support Common Logic enough to include it as a core logic. We should at least make sure that the Common Logic issues that are currently open aren't critical.