Framework.hs revision a51b009f79b8bd39d71571e01e607173b134cce8
3ee0a2095e7213b1b7889025658f784ef48426eaRazvan PascanuDescription : syntax and analysis for adding object logics to Hets
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elknerfrom their specification in a logical framework
3ee0a2095e7213b1b7889025658f784ef48426eaRazvan PascanuThe folder "Framework" contains the infrastructure needed for
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescuextending Hets with new logics which are specified in
3ee0a2095e7213b1b7889025658f784ef48426eaRazvan Pascanusome logical framework. Currently, this only works for LF, but
3ee0a2095e7213b1b7889025658f784ef48426eaRazvan Pascanureading Isabelle and Maude definitions of logics is also
3ee0a2095e7213b1b7889025658f784ef48426eaRazvan PascanuThe module "Framework.AS" gives the abstract syntax, while the
3ee0a2095e7213b1b7889025658f784ef48426eaRazvan Pascanustatic analysis of the newly defined logics is implemented in
3ee0a2095e7213b1b7889025658f784ef48426eaRazvan Pascanuthe module "Framework.Analysis" and it relies on the methods
3ee0a2095e7213b1b7889025658f784ef48426eaRazvan Pascanuprovided by the instances of the class 'Logic.Logic.LogicalFramework'.
fc1a590cd3ee36797c0a032ff41e07f8e2469341Christian Maedermodule Framework where