Logic.hs revision 99249aeda5fac6f8f0b2316ca357bac898af1928
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaederDescription : infrastructure needed for presenting a logic to Hets
3a6c7a7ff823616f56cd3d205fc44664a683effdChristian MaederThe folder "Logic" contains the infrastructure needed for
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maederpresenting a logic to Hets. A logic here is understood in
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maederthe theory of institutions. More precisely, a logic is
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian Maederan entailment system in the sense of Meseguer.
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederAn entailment system consists of a category
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maederof signatures and signature morphisms, a set of sentences
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederfor each signature, a sentence translation map of each
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maedersignature morphism, and an entailment relation
44fb55f639914f4f531641f32dd4904f15c510a4Till Mossakowskibetween sets of sentences and sentences for each signature.
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiThe module "Logic.Logic" contains all the type classes for interfacing
af0cbe339851fc558d2b18cde3666981325e667cTill Mossakowskientailment systems in this sense, including the type class
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski'Logic.Logic.Logic'. The entailment relation is given by one or more
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskitheorem provers, rewriters, consistency checkers, model checkers. The
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maedermodule "Logic.Prover" is for the interface to these. The data types
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder'Logic.Prover.Proof_Status' and 'Logic.Prover.Prover' provides the
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederinterface to provers. In case of a successful proof, also the list of
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederaxioms that have been used in the proof can be returned.
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederNote that the type class 'Logic.Logic.Logic' contains much more than
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederjust an entailment system. There is infrastructure for parsing,
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederprinting, static analysis (of both basic specifications and symbols
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maedermaps) , conversion to ATerms, sublogic recognition etc. You see that
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederin order to really work with it, one needs much more than just
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederan entailment system in the mathematical sense.
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederWe will use the term /logic/ synonymously with an extended entailment
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maedersystem in this sense.
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Module "Logic.Comorphism" provides type classes for the various kinds
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederof mappings between logics, and module "Logic.Grothendieck"
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederrealizes the Grothendieck logic and also contains a type
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder/How to add a new logic to Hets/
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederA good idea is to look at an existing logic, say "Propositional" or
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder"CASL", and look how it realizes the abstract interface given in
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder"Logic.Logic" - this is done in "Propositional.Logic_Propositional"
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiresp. "CASL.Logic_CASL", where the whole of
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskithe "Propositional" resp. "CASL" folder is imported.
63324a97283728a30932828a612c7b0b0f687624Christian MaederYou also should have a look at some of the "Common" modules,
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maederproviding data structures for identifiers ("Common.Id"),
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maedersets ("Common.Lib.Set"), maps ("Common.Lib.Map") and relations
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder("Common.Lib.Rel"). These are used quite frequently.
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maedermodule Logic where