Consistency of large theories via architectural specifications

From FMS-wiki
Jump to: navigation, search
  • Consistency of large logical theories is too hard for model finders. With CASL architectural specifications, the problem can be decomposed into smaller sub-problems. The goal is to develop heuristics and a (semi-)automatic tool for finding such decompositions
    • find an order on symbols, and derive archictural decompositions from such an order
    • choose units as large as possible such that model finders can still handle them
    • instead of checking conservativity (for parameterised units), one can also feed axiomatisations of the units (models) for the parameters plus the body axioms into a model finder
  • Prerequisite knowledge: understanding of logic. For the implementation, skills in a functional programming language like Haskell are needed
  • Contact person: Till Mossakowski
  • Literature: