{- |

Module : $Header$

Description : Provers for propositional logic

Copyright : (c) Till Mossakowski, Uni Bremen 2008

License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

Maintainer : till@informatik.uni-bremen.de

Stability : experimental

Portability : portable

A truth table prover for propositional logic.

Inefficient, but useful for learning purposes.

-}

module Propositional.ProveWithTruthTable

( ttProver

, ttConsistencyChecker

, ttConservativityChecker

, allModels

) where

import Common.Lib.Tabular

import Propositional.AS_BASIC_Propositional

import Propositional.Sign

import qualified Propositional.Morphism as PMorphism

import qualified Propositional.ProverState as PState

import qualified Propositional.Sign as Sig

import Propositional.Sublogic (PropSL, top)

import qualified Logic.Prover as LP

import qualified Interfaces.GenericATPState as ATPState

import GUI.GenericATP

import GUI.Utils (infoDialog, createTextSaveDisplay)

import Common.ProofTree

import qualified Common.AS_Annotation as AS_Anno

import qualified Common.Id as Id

import qualified Data.Set as Set

import qualified Common.OrderedMap as OMap

import Common.Consistency

import qualified Common.Result as Result

import Data.Time (midnight)

-- * Prover implementation

-- | the name of the prover

ttS :: String

ttS = "truth tables"

-- maximal size of the signature

maxSigSize :: Int

maxSigSize = 17

-- display error message when signature is too large

sigTooLarge :: Int -> String

sigTooLarge sigSize = unlines

[ "Signature is too large."

, "It should contain < " ++ show maxSigSize ++ " symbols,"

, "but it contains " ++ show sigSize ++ " symbols." ]

ttHelpText :: String

ttHelpText = "An implementation of the truth table method.\n"

++ "Very inefficient, but useful for learning and teaching\n"

++ "Works well for signatures with less than " ++ show maxSigSize

++ " symbols."

{- |

Models and evaluation of sentences

-}

type Model = Set.Set Id.Id -- a model specifies which propositions are true

-- | show Bools in truth table

showBool :: Bool -> String

showBool True = "T"

showBool False = "F"

-- | evaluation of sentences in a model

eval :: Model -> FORMULA -> Bool

eval m (Negation phi _) = not $ eval m phi

eval m (Conjunction phis _) = all (eval m) phis

eval m (Disjunction phis _) = any (eval m) phis

eval m (Implication phi1 phi2 _) = not (eval m phi1) || eval m phi2

eval m (Equivalence phi1 phi2 _) = eval m phi1 == eval m phi2

eval _ (True_atom _) = True

eval _ (False_atom _) = False

eval m (Predication ident) = Id.simpleIdToId ident `Set.member` m

evalNamed :: Model -> AS_Anno.Named FORMULA -> Bool

evalNamed m = eval m . AS_Anno.sentence

{- |

Evaluation of (co)freeness constraints

-}

-- | amalgamation of models

amalg :: Model -> Model -> Model

amalg = Set.union

data FormulaOrFree =

Formula FORMULA

| FreeConstraint (LP.FreeDefMorphism FORMULA PMorphism.Morphism)

evalNamedFormulaOrFree :: Model -> AS_Anno.Named FormulaOrFree -> Bool

evalNamedFormulaOrFree m = evalFormulaOrFree m . AS_Anno.sentence

evalFormulaOrFree :: Model -> FormulaOrFree -> Bool

evalFormulaOrFree m (Formula phi) = eval m phi

evalFormulaOrFree m (FreeConstraint freedef) = evalFree m freedef

reduceModel :: Sig.Sign -> Model -> Model

reduceModel sig m = Set.intersection m (items sig)

leq :: Model -> Model -> Bool

leq = Set.isSubsetOf

isMin :: Bool -> Model -> [Model] -> Bool

isMin isCo m = all (\m' -> if isCo then leq m' m else leq m m')

evalFree :: Model

-> LP.FreeDefMorphism FORMULA PMorphism.Morphism

-> Bool

evalFree m freedef =

let diffsig = Sign (items freetar `Set.difference` items freesrc)

mred = reduceModel freesrc m

modelsOverMred = map (mred `amalg`) (allModels diffsig)

modelClass = foldr (filter . flip eval) modelsOverMred freeth

in all (eval m) freeth -- the model satisfies the axioms ...

&& isMin isCo m modelClass -- ... and is the minimal one that does so

where freemor = LP.freeDefMorphism freedef

freesrc = PMorphism.source freemor

freetar = PMorphism.target freemor

freeth = map AS_Anno.sentence $ LP.freeTheory freedef

isCo = LP.isCofree freedef

-- | generate all models for a signature

allModels :: Sign -> [Model]

allModels sig = allModels1 $ Set.toList $ items sig

where allModels1 [] = [Set.empty]

allModels1 (p:rest) =

let models = allModels1 rest

in models ++ map (Set.insert p) models

data TTExtRow =

TTExtRow { rextprops, rextaxioms :: [Bool]

, rextIsModel :: Bool

}

data TTRow =

TTRow { rprops, raxioms :: [Bool]

, rgoal :: Maybe Bool

, rextrows :: [TTExtRow]

, rIsModel :: Bool

, rIsOK :: Bool

}

data TTHead =

TTHead { hprops, haxioms, hextprops, hextaxioms :: [String]

, hgoal :: Maybe String

}

data TruthTable =

TruthTable { thead :: TTHead

, trows :: [TTRow]

}

renderTT :: TruthTable -> Table String String String

renderTT tt = Table rowHeaders header table

where

hextpropsTT = hextprops (thead tt)

hextaxiomsTT = hextaxioms (thead tt)

rowsTT = trows tt

header = Group DoubleLine

( [ Group SingleLine (map Header (hprops (thead tt)))

, Group SingleLine (map Header (haxioms (thead tt)))]

++ (if null hextpropsTT && null hextaxiomsTT then []

else [ Header ""

, Group SingleLine (map Header hextpropsTT)

, Group SingleLine (map Header hextaxiomsTT)])

++ case hgoal (thead tt) of

Nothing -> []

Just g -> [Group DoubleLine [Header g]])

rowtype r = (if rIsModel r then "M" else " ")

++(if rIsOK r then (if rIsModel r then "+" else "o")

else "-")

rowHeader r = Group NoLine

$ Header (rowtype r) : map (const (Header "")) [2..length (rextrows r)]

rowHeaders = if all (null . rextrows) rowsTT

then Group NoLine (map (Header . rowtype) rowsTT)

else Group SingleLine (map rowHeader rowsTT)

makeExtRow e = (if rextIsModel e then "M" else "") :

map showBool (rextprops e) ++ map showBool (rextaxioms e)

makeRow r =

let common = map showBool (rprops r) ++ map showBool (raxioms r) ++

case (rgoal r) of

Nothing -> []

Just g -> [showBool g]

emptyPrefix = map (const "") [1..length common]

in case map makeExtRow (rextrows r) of

[] -> [common]

e : extrows -> (common ++ e) : map (emptyPrefix ++) extrows

table = concatMap makeRow rowsTT

{- |

The Prover implementation.

Implemented are: a prover GUI.

-}

ttProver :: LP.Prover Sig.Sign FORMULA PMorphism.Morphism PropSL ProofTree

ttProver = LP.mkProverTemplate ttS top ttProveGUI

{- |

The Consistency Cheker.

-}

ttConsistencyChecker :: LP.ConsChecker Sig.Sign FORMULA PropSL

PMorphism.Morphism ProofTree

ttConsistencyChecker = LP.mkConsChecker ttS top consCheck

consCheck :: String -> LP.TacticScript

-> LP.TheoryMorphism Sig.Sign FORMULA PMorphism.Morphism ProofTree

-> [LP.FreeDefMorphism FORMULA PMorphism.Morphism]

-- ^ free definitions

-> IO (LP.CCStatus ProofTree)

consCheck _ _ tm _freedefs = case LP.tTarget tm of

LP.Theory sig nSens ->

let sigSize = Set.size (items sig) in

if sigSize >= maxSigSize then

return $ LP.CCStatus (ProofTree $ sigTooLarge sigSize) midnight Nothing

else do

let axs = filter (AS_Anno.isAxiom . snd) $ OMap.toList nSens

models = allModels sig

sigList = Set.toList $ items sig

heading = TTHead { hprops = map show sigList

, haxioms = map fst axs

, hextprops = [], hextaxioms = []

, hgoal = Nothing

}

mkRow m =

let evalAx = map (eval m . AS_Anno.sentence . snd) axs

isModel = and evalAx

in TTRow { rprops = map (`Set.member` m) sigList

, raxioms = evalAx

, rextrows = []

, rgoal = Nothing

, rIsModel = isModel

, rIsOK = isModel

}

rows = map mkRow models

isOK = any rIsOK rows

table = TruthTable { thead = heading

, trows = rows

}

legend = "Legend:\nM+ = model of the axioms\n"

++ " - = not a model of the axioms\n"

body = legend ++ "\n" ++ render id id id (renderTT table)

return $ LP.CCStatus (ProofTree body) midnight $ Just isOK

-- ** prover GUI

{- |

Invokes the generic prover GUI.

-}

ttProveGUI :: String -- ^ theory name

-> LP.Theory Sig.Sign FORMULA ProofTree

-> [LP.FreeDefMorphism FORMULA PMorphism.Morphism]

-- ^ free definitions

-> IO([LP.ProofStatus ProofTree]) -- ^ proof status for each goal

ttProveGUI thName th freedefs =

genericATPgui (atpFun thName) True (LP.proverName ttProver) thName th

freedefs emptyProofTree

{- |

Record for prover specific functions. This is used by both GUI and command

line interface.

-}

atpFun :: String -- ^ Theory name

-> ATPState.ATPFunctions Sig.Sign FORMULA PMorphism.Morphism ProofTree

PState.PropProverState

atpFun thName = ATPState.ATPFunctions

{ ATPState.initialProverState = PState.propProverState

, ATPState.goalOutput = goalProblem thName

, ATPState.atpTransSenName = PState.transSenName

, ATPState.atpInsertSentence = PState.insertSentence

, ATPState.proverHelpText = ttHelpText

, ATPState.runProver = runTt

, ATPState.batchTimeEnv = ""

, ATPState.fileExtensions = ATPState.FileExtensions

{ ATPState.problemOutput = ".tt"

, ATPState.proverOutput = ".tt"

, ATPState.theoryConfiguration = ".tt"}

, ATPState.createProverOptions = createTtOptions

}

defaultProofStatus :: AS_Anno.Named FORMULA -> LP.ProofStatus ProofTree

defaultProofStatus nGoal =

LP.openProofStatus (AS_Anno.senAttr nGoal) (LP.proverName ttProver)

emptyProofTree

{- |

Runs tt.

-}

runTt :: PState.PropProverState

-- ^ logical part containing the input Sign and

-- axioms and possibly goals that have been proved

-- earlier as additional axioms

-> ATPState.GenericConfig ProofTree

-- ^ configuration to use

-> Bool

-- ^ True means save DIMACS file

-> String

-- ^ Name of the theory

-> AS_Anno.Named FORMULA

-- ^ Goal to prove

-> IO (ATPState.ATPRetval, ATPState.GenericConfig ProofTree)

-- ^ (retval, configuration with proof status and complete output)

runTt pState cfg _ _thName nGoal =

let sig = PState.initialSignature pState

sigSize = Set.size $ items sig

in if sigSize >= maxSigSize then do

infoDialog "Signature too large" $ sigTooLarge sigSize

return (ATPState.ATPTLimitExceeded,

cfg { ATPState.proofStatus = defaultProofStatus nGoal })

else do

let axs = PState.initialAxioms pState

freedefs = PState.freeDefs pState

nameFree fd =

AS_Anno.makeNamed (if LP.isCofree fd then "cofree" else "free")

(FreeConstraint fd)

sens = map (AS_Anno.mapNamed Formula) axs ++ map nameFree freedefs

models = allModels sig

sigList = Set.toList $ items sig

heading =

TTHead { hprops = map show sigList

, haxioms = map AS_Anno.senAttr sens

, hextprops = [], hextaxioms = []

, hgoal = Just $ AS_Anno.senAttr nGoal

}

mkRow m =

let evalAx = map (evalNamedFormulaOrFree m) sens

evalGoal = evalNamed m nGoal

isModel = and evalAx

in TTRow { rprops = map (`Set.member` m) sigList

, raxioms = evalAx

, rextrows = []

, rgoal = Just evalGoal

, rIsModel = isModel

, rIsOK = not isModel || evalGoal

}

rows = map mkRow models

isOK = all rIsOK rows

consistent = any rIsModel rows

table = TruthTable { thead = heading

, trows = rows

}

legend = "Legend:\nM = model of the premises\n"++

"+ = OK, model fulfills conclusion\n"++

"- = not OK, counterexample for logical consequence\n"++

"o = OK, premises are not fulfilled, hence conclusion is "

++ "irrelevant\n"

body = legend++"\n"++render id id id (renderTT table)

let status = (defaultProofStatus nGoal)

{ LP.goalStatus = if isOK then LP.Proved consistent

else LP.Disproved

,LP.usedAxioms = map AS_Anno.senAttr sens

}

return (ATPState.ATPSuccess,

cfg { ATPState.proofStatus = status

, ATPState.resultOutput = [body] })

{- |

Creates a list of all options the truth table prover runs with.

Only Option is the timelimit

-}

createTtOptions :: ATPState.GenericConfig ProofTree -> [String]

createTtOptions _cfg = [] -- [(show $ configTimeLimit cfg)]

goalProblem :: String -- ^ name of the theory

-> PState.PropProverState -- ^ initial Prover state

-> AS_Anno.Named FORMULA -- ^ goal to prove

-> [String] -- ^ Options (ignored)

-> IO String

goalProblem _ _ _ _ = return ""

{- |

Conservativity check

-}

-- | Conservativity Check via truth table

-- TODO: check for injectivity!

ttConservativityChecker ::

(Sign, [AS_Anno.Named FORMULA]) -- ^ Initial sign and formulas

-> PMorphism.Morphism -- ^ morhpism between specs

-> [AS_Anno.Named FORMULA] -- ^ Formulas of extended spec

-> IO (Result.Result (Maybe (Conservativity, [FORMULA])))

ttConservativityChecker (_, srcSens) mor tarSens =

let srcAxs = filter AS_Anno.isAxiom srcSens

tarAxs = filter AS_Anno.isAxiom tarSens

srcSig = items $ PMorphism.source mor

imageSig = Set.map (PMorphism.applyMorphism mor) srcSig

imageSigList = Set.toList imageSig

tarSig = items $ PMorphism.target mor

newSig = Set.difference tarSig imageSig

sigSize = Set.size tarSig

in if sigSize >= maxSigSize then return $ return Nothing

else do

let imageAxs = map (AS_Anno.mapNamed (PMorphism.mapSentenceH mor)) srcAxs

models = allModels (Sign imageSig)

newSigList = Set.toList newSig

heading =

TTHead { hprops = map show imageSigList,

haxioms = map AS_Anno.senAttr srcAxs,

hextprops = map show newSigList,

hextaxioms = map AS_Anno.senAttr tarAxs,

hgoal = Nothing

}

mkRow m =

let evalAx = map (evalNamed m) imageAxs

isModel = and evalAx

extmodels = allModels (Sign newSig)

extrow m' =

let evalExtAx = map (evalNamed (m `amalg` m')) tarAxs

isExtModel = and evalExtAx

in TTExtRow { rextprops = map (`Set.member` m') newSigList,

rextaxioms = evalExtAx,

rextIsModel = isExtModel

}

extrows = map extrow extmodels

in TTRow { rprops = map (`Set.member` m) imageSigList,

raxioms = evalAx,

rgoal = Nothing,

rextrows = if isModel then extrows else [],

rIsModel = isModel,

rIsOK = not isModel || any rextIsModel extrows

}

rows = map mkRow models

isOK = all rIsOK rows

table = TruthTable { thead = heading,

trows = rows

}

title = "The extension is "++ (if isOK then "" else "not ")

++ "conservative"

legend = "Legend:\n"

++ "M = model of the axioms\n"

++ "+ = OK, has expansion\n"

++ "- = not OK, has no expansion, hence conservativity fails\n"

++ "o = OK, not a model of the axioms, hence no expansion needed\n"

body = legend++"\n"++render id id id (renderTT table)

res = if isOK then Cons else Inconsistent

createTextSaveDisplay title "unnamed" body

return $ return $ Just (res, [])