5645e0c82a55b05abb975bd91b9566823dc5efb0Evan Hunt{- |

87708bde16713bc02ff2598f4a82f98c699a2f2dMark AndrewsModule : $Header$

87708bde16713bc02ff2598f4a82f98c699a2f2dMark AndrewsDescription : Provers for propositional logic

87708bde16713bc02ff2598f4a82f98c699a2f2dMark AndrewsCopyright : (c) Till Mossakowski, Uni Bremen 2008

87708bde16713bc02ff2598f4a82f98c699a2f2dMark AndrewsLicense : GPLv2 or higher, see LICENSE.txt

87708bde16713bc02ff2598f4a82f98c699a2f2dMark Andrews

87708bde16713bc02ff2598f4a82f98c699a2f2dMark AndrewsMaintainer : till@informatik.uni-bremen.de

87708bde16713bc02ff2598f4a82f98c699a2f2dMark AndrewsStability : experimental

87708bde16713bc02ff2598f4a82f98c699a2f2dMark AndrewsPortability : portable

87708bde16713bc02ff2598f4a82f98c699a2f2dMark Andrews

87708bde16713bc02ff2598f4a82f98c699a2f2dMark AndrewsA truth table prover for propositional logic.

87708bde16713bc02ff2598f4a82f98c699a2f2dMark AndrewsInefficient, but useful for learning purposes.

87708bde16713bc02ff2598f4a82f98c699a2f2dMark Andrews-}

87708bde16713bc02ff2598f4a82f98c699a2f2dMark Andrews

c19cfefe7e345c37ef3bb98b0db2d14fe7b1d583Evan Huntmodule Propositional.ProveWithTruthTable

87708bde16713bc02ff2598f4a82f98c699a2f2dMark Andrews ( ttProver

87708bde16713bc02ff2598f4a82f98c699a2f2dMark Andrews , ttConsistencyChecker

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver , ttConservativityChecker

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver , allModels

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver ) where

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryverimport Common.Lib.Tabular

87708bde16713bc02ff2598f4a82f98c699a2f2dMark Andrews

87708bde16713bc02ff2598f4a82f98c699a2f2dMark Andrewsimport Propositional.AS_BASIC_Propositional

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryverimport Propositional.Sign

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryverimport qualified Propositional.Morphism as PMorphism

475b1ed9cced1f92ce34bc2e59b3065dae48f366Mark Andrewsimport qualified Propositional.ProverState as PState

afaa290bb6acc504e93a0adbf20b6dd6c64e6d63Vernon Schryverimport qualified Propositional.Sign as Sig

87708bde16713bc02ff2598f4a82f98c699a2f2dMark Andrewsimport Propositional.Sublogic (PropSL, top)

475b1ed9cced1f92ce34bc2e59b3065dae48f366Mark Andrews

afaa290bb6acc504e93a0adbf20b6dd6c64e6d63Vernon Schryverimport qualified Logic.Prover as LP

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryverimport qualified Interfaces.GenericATPState as ATPState

afaa290bb6acc504e93a0adbf20b6dd6c64e6d63Vernon Schryverimport GUI.GenericATP

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryverimport GUI.Utils (infoDialog, createTextSaveDisplay)

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryverimport Common.ProofTree

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryverimport qualified Common.AS_Annotation as AS_Anno

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryverimport qualified Common.Id as Id

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryverimport qualified Data.Set as Set

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryverimport qualified Common.OrderedMap as OMap

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryverimport Common.Consistency

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryverimport qualified Common.Result as Result

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryverimport Data.Time (midnight)

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver-- * Prover implementation

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver-- | the name of the prover

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon SchryverttS :: String

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon SchryverttS = "truth tables"

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver-- maximal size of the signature

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon SchryvermaxSigSize :: Int

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon SchryvermaxSigSize = 17

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver-- display error message when signature is too large

afaa290bb6acc504e93a0adbf20b6dd6c64e6d63Vernon SchryversigTooLarge :: Int -> String

afaa290bb6acc504e93a0adbf20b6dd6c64e6d63Vernon SchryversigTooLarge sigSize = unlines

afaa290bb6acc504e93a0adbf20b6dd6c64e6d63Vernon Schryver [ "Signature is too large."

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

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

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver

afaa290bb6acc504e93a0adbf20b6dd6c64e6d63Vernon SchryverttHelpText :: String

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon SchryverttHelpText = "An implementation of the truth table method.\n"

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

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver ++ "Works well for signatures with less than " ++ show maxSigSize

afaa290bb6acc504e93a0adbf20b6dd6c64e6d63Vernon Schryver ++ " symbols."

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver

afaa290bb6acc504e93a0adbf20b6dd6c64e6d63Vernon Schryver{- |

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver Models and evaluation of sentences

afaa290bb6acc504e93a0adbf20b6dd6c64e6d63Vernon Schryver-}

afaa290bb6acc504e93a0adbf20b6dd6c64e6d63Vernon Schryver

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryvertype Model = Set.Set Id.Id -- a model specifies which propositions are true

afaa290bb6acc504e93a0adbf20b6dd6c64e6d63Vernon Schryver

afaa290bb6acc504e93a0adbf20b6dd6c64e6d63Vernon Schryver-- | show Bools in truth table

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon SchryvershowBool :: Bool -> String

9fee08f655527a5dd849b171daeeee1dbbccca76Vernon SchryvershowBool True = "T"

afaa290bb6acc504e93a0adbf20b6dd6c64e6d63Vernon SchryvershowBool False = "F"

afaa290bb6acc504e93a0adbf20b6dd6c64e6d63Vernon Schryver

afaa290bb6acc504e93a0adbf20b6dd6c64e6d63Vernon Schryver-- | evaluation of sentences in a model

7b4b6f361b2fb2291c2019b377a9c0c8e80cfd6bMark Andrewseval :: Model -> FORMULA -> Bool

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

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

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

87708bde16713bc02ff2598f4a82f98c699a2f2dMark Andrewseval 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, [])