Develop heuristics for comorphism and prover selection in Hets

From FMS-wiki
Jump to: navigation, search


  • Hets is a tool that can prove open proof goals in a certain logic by
    • selecting a logic translation (comorphism) into a prover-supported logic, and
    • selecting a prover that supports theorem proving in that logic
  • This selection process shall be supported by the development of suitable methods, like heuristics and/or machine learning and/or case-based reasoning
  • there is a (small) set of worked examples that can be used as a starting point
  • see also the Hets issue


  • Skills in machine learning and/or case-based reasoning
  • Programming skills in Python and/or Haskell