{- |
Module : ./Propositional/ProveWithTruthTable.hs
Description : Provers for propositional logic
Copyright : (c) Till Mossakowski, Uni Bremen 2008
License : GPLv2 or higher, see LICENSE.txt
Maintainer : till@informatik.uni-bremen.de
Stability : experimental
Portability : portable
A truth table prover for propositional logic.
Inefficient, but useful for learning purposes.
-}
( ttProver
, ttConsistencyChecker
, ttConservativityChecker
, allModels
) where
import Common.Lib.Tabular
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
-}
-- | 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.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.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.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
atpFun thName = ATPState.ATPFunctions
, ATPState.goalOutput = goalProblem thName
, ATPState.proverHelpText = ttHelpText
, ATPState.runProver = runTt
, ATPState.batchTimeEnv = ""
{ ATPState.problemOutput = ".tt"
, ATPState.proverOutput = ".tt"
, ATPState.theoryConfiguration = ".tt"}
, ATPState.createProverOptions = createTtOptions
}
defaultProofStatus :: AS_Anno.Named FORMULA -> LP.ProofStatus ProofTree
defaultProofStatus nGoal =
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 (Conservativity, [FORMULA]))
ttConservativityChecker (_, srcSens) mor tarAxs =
let srcAxs = filter AS_Anno.isAxiom srcSens
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 (Unknown "signature too big", [])
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 (res, [])