0095c7efbddd0ffeed6aaf8ec015346be161d819Till MossakowskiDescription : infrastructure needed for presenting a logic to Hets
e687bd70d6e6c98d82b239e01fef4a60de6739f4Till MossakowskiThe folder "Logic" contains the infrastructure needed for
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskipresenting a logic to Hets. A logic here is understood in
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskithe theory of institutions. More precisely, a logic is
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskian entailment system in the sense of Meseguer.
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill MossakowskiAn entailment system consists of a category
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiof signatures and signature morphisms, a set of sentences
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskifor each signature, a sentence translation map of each
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskisignature morphism, and an entailment relation
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskibetween sets of sentences and sentences for each signature.
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill MossakowskiThe module "Logic.Logic" contains all the type classes for interfacing
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskientailment systems in this sense, including the type class
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski'Logic.Logic.Logic'. The entailment relation is given by one or more
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskitheorem provers, rewriters, consistency checkers, model checkers. The
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskimodule "Logic.Prover" is for the interface to these. The data types
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski'Logic.Prover.Proof_Status' and 'Logic.Prover.Prover' provides the
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiinterface to provers. In case of a successful proof, also the list of
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiaxioms that have been used in the proof can be returned.
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill MossakowskiNote that the type class 'Logic.Logic.Logic' contains much more than
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskijust an entailment system. There is infrastructure for parsing,
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiprinting, static analysis (of both basic specifications and symbols
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskimaps) , conversion to ATerms, sublogic recognition etc. You see that
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiin order to really work with it, one needs much more than just
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskian entailment system in the mathematical sense.
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill MossakowskiWe will use the term /logic/ synonymously with an extended entailment
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskisystem in this sense.
37bca994f215449238dd0c8308a94a83ae184d38Mihai CodescuThe type class 'Logic.Logic.LogicalFramework' is an interface for the
37bca994f215449238dd0c8308a94a83ae184d38Mihai Codesculogics which can be used as logical frameworks, in which object
c561172957d9f9a3e248b8c5bd8d8f5e6470d2beChristian Maederlogics can be specified by the user. Its methods are used in the
c561172957d9f9a3e248b8c5bd8d8f5e6470d2beChristian Maederanalysis of newlogic definitions, in "Framework.Analysis".
c561172957d9f9a3e248b8c5bd8d8f5e6470d2beChristian MaederThe method 'Logic.Logic.LogicalFramework.base_sig'
c561172957d9f9a3e248b8c5bd8d8f5e6470d2beChristian Maederreturns the base signature of the framework
c561172957d9f9a3e248b8c5bd8d8f5e6470d2beChristian MaederThe method 'Logic.Logic.LogicalFramework.write_logic'
37bca994f215449238dd0c8308a94a83ae184d38Mihai Codescuconstructs the contents of the Logic_L
37bca994f215449238dd0c8308a94a83ae184d38Mihai Codescufile, where L is the name of the object logic passed as an argument.
37bca994f215449238dd0c8308a94a83ae184d38Mihai CodescuTypically, this file will declare the lid of the object logic L and
37bca994f215449238dd0c8308a94a83ae184d38Mihai Codescuinstances of the classes Language, Syntax, Sentences, Logic, and
37bca994f215449238dd0c8308a94a83ae184d38Mihai CodescuStaticAnalysis. The instance of Category is usually inherited from
37bca994f215449238dd0c8308a94a83ae184d38Mihai Codescuthe framework itself as the object logic reuses the signatures and
c561172957d9f9a3e248b8c5bd8d8f5e6470d2beChristian Maedermorphisms of the framework. The function
c561172957d9f9a3e248b8c5bd8d8f5e6470d2beChristian Maeder'Logic.Logic.LogicalFramework.write_syntax' constructs
c561172957d9f9a3e248b8c5bd8d8f5e6470d2beChristian Maederthe contents of the file declaring the Ltruth morphism.
37bca994f215449238dd0c8308a94a83ae184d38Mihai CodescuCurrently we simply store the morphism using its representation as
8f3c5acc87958cc3f4e413c37b0f124fb4e3db47Mihai Codescua Haskell datatype value.
e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski Module "Logic.Comorphism" provides type classes for the various kinds
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiof mappings between logics, and module "Logic.Grothendieck"
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskirealizes the Grothendieck logic and also contains a type
e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski/How to add a new logic to Hets/
7474388b4c2236f8ab2327289555000268c7901aTill MossakowskiA good idea is to look at an existing logic, say "Propositional" or
7474388b4c2236f8ab2327289555000268c7901aTill Mossakowski"CASL", and look how it realizes the abstract interface given in
7474388b4c2236f8ab2327289555000268c7901aTill Mossakowski"Logic.Logic" - this is done in "Propositional.Logic_Propositional"
7474388b4c2236f8ab2327289555000268c7901aTill Mossakowskiresp. "CASL.Logic_CASL", where the whole of
7474388b4c2236f8ab2327289555000268c7901aTill Mossakowskithe "Propositional" resp. "CASL" folder is imported.
da955132262baab309a50fdffe228c9efe68251dCui JianYou also should have a look at some of the "Common" modules,
e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowskiproviding data structures for identifiers ("Common.Id"),
8d6aa4bda97770cc79cf96de3c0f9dfa4d7d7aafChristian Maederresults ("Common.Result"), and relations
99249aeda5fac6f8f0b2316ca357bac898af1928Christian Maeder("Common.Lib.Rel"). These are used quite frequently.
4918e2f622cfb96f9a57b7617cd18ca7e4f8b5d4Christian Maedermodule Logic where