{-# LANGUAGE MultiParamTypeClasses #-}

{- |

Module : $Header$

Description : Instance of class Logic for propositional logic

Copyright : (c) Dominik Luecke, Uni Bremen 2007

License : GPLv2 or higher, see LICENSE.txt

Maintainer : luecke@informatik.uni-bremen.de

Stability : experimental

Portability : non-portable (imports Logic.Logic)

Instance of class Logic for the propositional logic

Also the instances for Syntax and Category.

-}

{-

Ref.

http://en.wikipedia.org/wiki/Propositional_logic

Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.

What is a Logic?.

In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-@133. Birkhaeuser.

2005.

-}

module Propositional.Logic_Propositional where

import ATC.ProofTree ()

import Logic.Logic

import Propositional.Sign

import Propositional.Morphism

import Propositional.AS_BASIC_Propositional

import Propositional.ATC_Propositional ()

import Propositional.Fold

import Propositional.Symbol as Symbol

import Propositional.Parse_AS_Basic

import Propositional.Analysis

import Propositional.Sublogic as Sublogic

import Propositional.ProveWithTruthTable

import Propositional.Prove

import Propositional.Conservativity

import Propositional.ProveMinisat

import Common.ProverTools

import Common.Consistency

import Common.ProofTree

import Common.Id

import qualified Data.Map as Map

import Data.Monoid

-- | Lid for propositional logic

data Propositional = Propositional deriving Show

instance Language Propositional where

description _ = "Propositional Logic\n"

++ "for more information please refer to\n"

++ "http://en.wikipedia.org/wiki/Propositional_logic"

-- | Instance of Category for propositional logic

instance Category Sign Morphism where

-- Identity morhpism

ide = idMor

-- Returns the domain of a morphism

dom = source

-- Returns the codomain of a morphism

cod = target

-- check if morphism is inclusion

isInclusion = Map.null . propMap

-- tests if the morphism is ok

legal_mor = isLegalMorphism

-- composition of morphisms

composeMorphisms = composeMor

-- | Instance of Sentences for propositional logic

instance Sentences Propositional FORMULA

Sign Morphism Symbol where

negation Propositional = Just . negForm nullRange

-- returns the set of symbols

sym_of Propositional = singletonList . symOf

-- returns the symbol map

symmap_of Propositional = getSymbolMap

-- returns the name of a symbol

sym_name Propositional = getSymbolName

symKind Propositional _ = "prop"

-- translation of sentences along signature morphism

map_sen Propositional = mapSentence

-- there is nothing to leave out

simplify_sen Propositional _ = simplify

instance Monoid BASIC_SPEC where

mempty = Basic_spec []

mappend (Basic_spec l1) (Basic_spec l2) = Basic_spec $ l1 ++ l2

-- - | Syntax of Propositional logic

instance Syntax Propositional BASIC_SPEC

Symbol SYMB_ITEMS SYMB_MAP_ITEMS where

parsersAndPrinters Propositional =

addSyntax "Hets" (basicSpec, pretty)

$ makeDefault (basicSpec, pretty)

parse_symb_items Propositional = Just symbItems

parse_symb_map_items Propositional = Just symbMapItems

-- | Instance of Logic for propositional logc

instance Logic Propositional

PropSL -- Sublogics

BASIC_SPEC -- basic_spec

FORMULA -- sentence

SYMB_ITEMS -- symb_items

SYMB_MAP_ITEMS -- symb_map_items

Sign -- sign

Morphism -- morphism

Symbol -- symbol

Symbol -- raw_symbol

ProofTree -- proof_tree

where

-- hybridization

parse_basic_sen Propositional = Just $ const impFormula

stability Propositional = Experimental

top_sublogic Propositional = Sublogic.top

all_sublogics Propositional = sublogics_all

empty_proof_tree Propositional = emptyProofTree

-- supplied provers

provers Propositional =

[zchaffProver, minisatProver Minisat, minisatProver Minisat2, ttProver]

cons_checkers Propositional =

[ propConsChecker, minisatConsChecker Minisat

, minisatConsChecker Minisat2, ttConsistencyChecker]

conservativityCheck Propositional =

[ ConservativityChecker "sKizzo" (checkBinary "sKizzo") conserCheck

, ConservativityChecker "Truth Tables" (return Nothing)

ttConservativityChecker]

-- | Static Analysis for propositional logic

instance StaticAnalysis Propositional

BASIC_SPEC -- basic_spec

FORMULA -- sentence

SYMB_ITEMS -- symb_items

SYMB_MAP_ITEMS -- symb_map_items

Sign -- sign

Morphism -- morphism

Symbol -- symbol

Symbol -- raw_symbol

where

basic_analysis Propositional =

Just basicPropositionalAnalysis

sen_analysis Propositional = Just pROPsen_analysis

empty_signature Propositional = emptySig

is_subsig Propositional = isSubSigOf

subsig_inclusion Propositional s = return . inclusionMap s

signature_union Propositional = sigUnion

symbol_to_raw Propositional = symbolToRaw

id_to_raw Propositional = idToRaw

matches Propositional = Symbol.matches

stat_symb_items Propositional _ = mkStatSymbItems

stat_symb_map_items Propositional _ _ = mkStatSymbMapItem

morphism_union Propositional = morphismUnion

induced_from_morphism Propositional = inducedFromMorphism

induced_from_to_morphism Propositional = inducedFromToMorphism

signature_colimit Propositional = signatureColimit

-- | Sublogics

instance SemiLatticeWithTop PropSL where

lub = sublogics_max

top = Sublogic.top

instance MinSublogic PropSL BASIC_SPEC where

minSublogic = sl_basic_spec bottom

instance MinSublogic PropSL Sign where

minSublogic = sl_sig bottom

instance SublogicName PropSL where

sublogicName = sublogics_name

instance MinSublogic PropSL FORMULA where

minSublogic = sl_form bottom

instance MinSublogic PropSL Symbol where

minSublogic = sl_sym bottom

instance MinSublogic PropSL SYMB_ITEMS where

minSublogic = sl_symit bottom

instance MinSublogic PropSL Morphism where

minSublogic = sl_mor bottom

instance MinSublogic PropSL SYMB_MAP_ITEMS where

minSublogic = sl_symmap bottom

instance ProjectSublogicM PropSL Symbol where

projectSublogicM = prSymbolM

instance ProjectSublogic PropSL Sign where

projectSublogic = prSig

instance ProjectSublogic PropSL Morphism where

projectSublogic = prMor

instance ProjectSublogicM PropSL SYMB_MAP_ITEMS where

projectSublogicM = prSymMapM

instance ProjectSublogicM PropSL SYMB_ITEMS where

projectSublogicM = prSymM

instance ProjectSublogic PropSL BASIC_SPEC where

projectSublogic = prBasicSpec

instance ProjectSublogicM PropSL FORMULA where

projectSublogicM = prFormulaM