ProveWithTruthTable.hs revision e9458b1a7a19a63aa4c179f9ab20f4d50681c168
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian MaederModule : ./Propositional/ProveWithTruthTable.hs
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian MaederDescription : Provers for propositional logic
cd7372fc7e6e43c389619f63daa6eb872d9d5b16Christian MaederCopyright : (c) Till Mossakowski, Uni Bremen 2008
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian MaederMaintainer : till@informatik.uni-bremen.de
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederStability : experimental
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederPortability : portable
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederA truth table prover for propositional logic.
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederInefficient, but useful for learning purposes.
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder , ttConsistencyChecker
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder , ttConservativityChecker
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maederimport qualified Propositional.Morphism as PMorphism
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maederimport qualified Propositional.ProverState as PState
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maederimport qualified Propositional.Sign as Sig
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maederimport Propositional.Sublogic (PropSL, top)
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maederimport qualified Logic.Prover as LP
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maederimport qualified Interfaces.GenericATPState as ATPState
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maederimport GUI.Utils (infoDialog, createTextSaveDisplay)
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maederimport qualified Common.AS_Annotation as AS_Anno
989ba1f28e0846635a9f098bebbfbdfa9b1c5ed0Jonathan von Schroederimport qualified Common.Id as Id
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maederimport qualified Data.Set as Set
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maederimport qualified Common.OrderedMap as OMap
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maederimport qualified Common.Result as Result
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maederimport Data.Time (midnight)
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder-- * Prover implementation
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | the name of the prover
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederttS = "truth tables"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- maximal size of the signature
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimaxSigSize :: Int
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimaxSigSize = 17
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- display error message when signature is too large
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinisigTooLarge :: Int -> String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinisigTooLarge sigSize = unlines
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder [ "Signature is too large."
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , "It should contain < " ++ show maxSigSize ++ " symbols,"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , "but it contains " ++ show sigSize ++ " symbols." ]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinittHelpText :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinittHelpText = "An implementation of the truth table method.\n"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ++ "Very inefficient, but useful for learning and teaching\n"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ++ "Works well for signatures with less than " ++ show maxSigSize
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ++ " symbols."
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Models and evaluation of sentences
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinitype Model = Set.Set Id.Id -- a model specifies which propositions are true
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | show Bools in truth table
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinishowBool :: Bool -> String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinishowBool True = "T"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinishowBool False = "F"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | evaluation of sentences in a model
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinieval :: Model -> FORMULA -> Bool
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinieval m (Negation phi _) = not $ eval m phi
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinieval m (Conjunction phis _) = all (eval m) phis
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinieval m (Disjunction phis _) = any (eval m) phis
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinieval m (Implication phi1 phi2 _) = not (eval m phi1) || eval m phi2
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinieval m (Equivalence phi1 phi2 _) = eval m phi1 == eval m phi2
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinieval _ (True_atom _) = True
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinieval _ (False_atom _) = False
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinieval m (Predication ident) = Id.simpleIdToId ident `Set.member` m
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinievalNamed :: Model -> AS_Anno.Named FORMULA -> Bool
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinievalNamed m = eval m . AS_Anno.sentence
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini Evaluation of (co)freeness constraints
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini-- | amalgamation of models
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torriniamalg :: Model -> Model -> Model
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinidata FormulaOrFree =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Formula FORMULA
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | FreeConstraint (LP.FreeDefMorphism FORMULA PMorphism.Morphism)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinievalNamedFormulaOrFree :: Model -> AS_Anno.Named FormulaOrFree -> Bool
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillyevalNamedFormulaOrFree m = evalFormulaOrFree m . AS_Anno.sentence
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillyevalFormulaOrFree :: Model -> FormulaOrFree -> Bool
d9c1248c7972dfdafbacb1b73b2eb965eac9ef42Liam O'ReillyevalFormulaOrFree m (Formula phi) = eval m phi
d9c1248c7972dfdafbacb1b73b2eb965eac9ef42Liam O'ReillyevalFormulaOrFree m (FreeConstraint freedef) = evalFree m freedef
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyreduceModel :: Sig.Sign -> Model -> Model
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyreduceModel sig m = Set.intersection m (items sig)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyleq :: Model -> Model -> Bool
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillyisMin :: Bool -> Model -> [Model] -> Bool
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillyisMin isCo m = all (\ m' -> if isCo then leq m' m else leq m m')
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillyevalFree :: Model
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly -> LP.FreeDefMorphism FORMULA PMorphism.Morphism
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederevalFree m freedef =
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder let diffsig = Sign (items freetar `Set.difference` items freesrc)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder mred = reduceModel freesrc m
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder modelsOverMred = map (mred `amalg`) (allModels diffsig)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini modelClass = foldr (filter . flip eval) modelsOverMred freeth
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini in all (eval m) freeth -- the model satisfies the axioms ...
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini && isMin isCo m modelClass -- ... and is the minimal one that does so
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini where freemor = LP.freeDefMorphism freedef
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini freesrc = PMorphism.source freemor
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini freetar = PMorphism.target freemor
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini freeth = map AS_Anno.sentence $ LP.freeTheory freedef
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini isCo = LP.isCofree freedef
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | generate all models for a signature
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniallModels :: Sign -> [Model]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniallModels sig = allModels1 $ Set.toList $ items sig
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini where allModels1 [] = [Set.empty]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini allModels1 (p : rest) =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let models = allModels1 rest
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini in models ++ map (Set.insert p) models
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinidata TTExtRow =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini TTExtRow { rextprops, rextaxioms :: [Bool]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , rextIsModel :: Bool
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini TTRow { rprops, raxioms :: [Bool]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , rgoal :: Maybe Bool
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , rextrows :: [TTExtRow]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , rIsModel :: Bool
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , rIsOK :: Bool
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini TTHead { hprops, haxioms, hextprops, hextaxioms :: [String]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , hgoal :: Maybe String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinidata TruthTable =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini TruthTable { thead :: TTHead
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , trows :: [TTRow]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinirenderTT :: TruthTable -> Table String String String
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederrenderTT tt = Table rowHeaders header table
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder hextpropsTT = hextprops (thead tt)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini hextaxiomsTT = hextaxioms (thead tt)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini rowsTT = trows tt
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini header = Group DoubleLine
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ( [ Group SingleLine (map Header (hprops (thead tt)))
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , Group SingleLine (map Header (haxioms (thead tt)))]
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04Paolo Torrini ++ (if null hextpropsTT && null hextaxiomsTT then []
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04Paolo Torrini else [ Header ""
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04Paolo Torrini , Group SingleLine (map Header hextpropsTT)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , Group SingleLine (map Header hextaxiomsTT)])
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ++ case hgoal (thead tt) of
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder Nothing -> []
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Just g -> [Group DoubleLine [Header g]])
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder rowtype r = (if rIsModel r then "M" else " ")
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ++ (if rIsOK r then (if rIsModel r then "+" else "o")
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini rowHeader r = Group NoLine
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder $ Header (rowtype r) : map (const (Header "")) [2 .. length (rextrows r)]
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder rowHeaders = if all (null . rextrows) rowsTT
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder then Group NoLine (map (Header . rowtype) rowsTT)
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder else Group SingleLine (map rowHeader rowsTT)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini makeExtRow e = (if rextIsModel e then "M" else "") :
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini map showBool (rextprops e) ++ map showBool (rextaxioms e)
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder let common = map showBool (rprops r) ++ map showBool (raxioms r) ++
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder case rgoal r of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Nothing -> []
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Just g -> [showBool g]
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder emptyPrefix = map (const "") [1 .. length common]
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder in case map makeExtRow (rextrows r) of
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder [] -> [common]
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini e : extrows -> (common ++ e) : map (emptyPrefix ++) extrows
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini table = concatMap makeRow rowsTT
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder The Prover implementation.
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini Implemented are: a prover GUI.
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinittProver :: LP.Prover Sig.Sign FORMULA PMorphism.Morphism PropSL ProofTree
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinittProver = LP.mkProverTemplate ttS top ttProveGUI
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder The Consistency Cheker.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinittConsistencyChecker :: LP.ConsChecker Sig.Sign FORMULA PropSL
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaederttConsistencyChecker = LP.mkConsChecker ttS top consCheck
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniconsCheck :: String -> LP.TacticScript
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini -> LP.TheoryMorphism Sig.Sign FORMULA PMorphism.Morphism ProofTree
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder -> [LP.FreeDefMorphism FORMULA PMorphism.Morphism]
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder -- ^ free definitions
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder -> IO (LP.CCStatus ProofTree)
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian MaederconsCheck _ _ tm _freedefs = case LP.tTarget tm of
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder let sigSize = Set.size (items sig) in
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder if sigSize >= maxSigSize then
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder return $ LP.CCStatus (ProofTree $ sigTooLarge sigSize) midnight Nothing
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let axs = filter (AS_Anno.isAxiom . snd) $ OMap.toList nSens
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder models = allModels sig
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini sigList = Set.toList $ items sig
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder heading = TTHead { hprops = map show sigList
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , haxioms = map fst axs
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini , hextprops = [], hextaxioms = []
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini , hgoal = Nothing
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini let evalAx = map (eval m . AS_Anno.sentence . snd) axs
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini isModel = and evalAx
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini in TTRow { rprops = map (`Set.member` m) sigList
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini , raxioms = evalAx
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder , rextrows = []
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini , rgoal = Nothing
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder , rIsModel = isModel
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , rIsOK = isModel
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder rows = map mkRow models
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder isOK = any rIsOK rows
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini table = TruthTable { thead = heading
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder , trows = rows
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini legend = "Legend:\nM+ = model of the axioms\n"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ++ " - = not a model of the axioms\n"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini body = legend ++ "\n" ++ render id id id (renderTT table)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return $ LP.CCStatus (ProofTree body) midnight $ Just isOK
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- ** prover GUI
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Invokes the generic prover GUI.
ce31795240d8fb340bc984b8b35147c955e29afaChristian MaederttProveGUI :: String -- ^ theory name
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -> [LP.FreeDefMorphism FORMULA PMorphism.Morphism]
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder -- ^ free definitions
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -> IO [LP.ProofStatus ProofTree] -- ^ proof status for each goal
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinittProveGUI thName th freedefs =
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder genericATPgui (atpFun thName) True (LP.proverName ttProver) thName th
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder freedefs emptyProofTree
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder Record for prover specific functions. This is used by both GUI and command
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini line interface.
603e326e7b189de8c1e4ea8c89470b3a61154019Christian MaederatpFun :: String -- ^ Theory name
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder -> ATPState.ATPFunctions Sig.Sign FORMULA PMorphism.Morphism ProofTree
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder { ATPState.initialProverState = PState.propProverState
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder , ATPState.goalOutput = goalProblem thName
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder , ATPState.atpTransSenName = PState.transSenName
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder , ATPState.atpInsertSentence = PState.insertSentence
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder , ATPState.fileExtensions = ATPState.FileExtensions
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , ATPState.createProverOptions = createTtOptions
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaederdefaultProofStatus :: AS_Anno.Named FORMULA -> LP.ProofStatus ProofTree
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederdefaultProofStatus nGoal =
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder LP.openProofStatus (AS_Anno.senAttr nGoal) (LP.proverName ttProver)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder emptyProofTree
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini {- ^ logical part containing the input Sign and
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder axioms and possibly goals that have been proved
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder earlier as additional axioms -}
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder -- ^ configuration to use
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder -- ^ True means save DIMACS file
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder -- ^ Name of the theory
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder -- ^ Goal to prove
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder -> IO (ATPState.ATPRetval, ATPState.GenericConfig ProofTree)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder -- ^ (retval, configuration with proof status and complete output)
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaederrunTt pState cfg _ _thName nGoal =
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder sigSize = Set.size $ items sig
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder in if sigSize >= maxSigSize then do
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder infoDialog "Signature too large" $ sigTooLarge sigSize
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder cfg { ATPState.proofStatus = defaultProofStatus nGoal })
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder freedefs = PState.freeDefs pState
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder nameFree fd =
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder AS_Anno.makeNamed (if LP.isCofree fd then "cofree" else "free")
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder (FreeConstraint fd)
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder sens = map (AS_Anno.mapNamed Formula) axs ++ map nameFree freedefs
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder models = allModels sig
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder sigList = Set.toList $ items sig
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder TTHead { hprops = map show sigList
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , haxioms = map AS_Anno.senAttr sens
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder , hextprops = [], hextaxioms = []
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder , hgoal = Just $ AS_Anno.senAttr nGoal
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let evalAx = map (evalNamedFormulaOrFree m) sens
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini evalGoal = evalNamed m nGoal
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini isModel = and evalAx
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini in TTRow { rprops = map (`Set.member` m) sigList
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder , raxioms = evalAx
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , rextrows = []
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , rgoal = Just evalGoal
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder , rIsModel = isModel
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , rIsOK = not isModel || evalGoal
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder rows = map mkRow models
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini isOK = all rIsOK rows
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini consistent = any rIsModel rows
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder table = TruthTable { thead = heading
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder , trows = rows
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder legend = "Legend:\nM = model of the premises\n" ++
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini "+ = OK, model fulfills conclusion\n" ++
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini "- = not OK, counterexample for logical consequence\n" ++
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini "o = OK, premises are not fulfilled, hence conclusion is "
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ++ "irrelevant\n"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder body = legend ++ "\n" ++ render id id id (renderTT table)
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder let status = (defaultProofStatus nGoal)
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder { LP.goalStatus = if isOK then LP.Proved consistent
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder Creates a list of all options the truth table prover runs with.
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly Only Option is the timelimit
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillycreateTtOptions :: ATPState.GenericConfig ProofTree -> [String]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicreateTtOptions _cfg = [] -- [(show $ configTimeLimit cfg)]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinigoalProblem :: String -- ^ name of the theory
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -> PState.PropProverState -- ^ initial Prover state
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -> AS_Anno.Named FORMULA -- ^ goal to prove
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly -> [String] -- ^ Options (ignored)
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillygoalProblem _ _ _ _ = return ""
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly Conservativity check
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | Conservativity Check via truth table
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- TODO: check for injectivity!
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaederttConservativityChecker ::
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder (Sign, [AS_Anno.Named FORMULA]) -- ^ Initial sign and formulas
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -> PMorphism.Morphism -- ^ morhpism between specs
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder -> [AS_Anno.Named FORMULA] -- ^ Formulas of extended spec
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder -> IO (Result.Result (Conservativity, [FORMULA]))
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinittConservativityChecker (_, srcSens) mor tarAxs =
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder let srcAxs = filter AS_Anno.isAxiom srcSens
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini srcSig = items $ PMorphism.source mor
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder imageSig = Set.map (PMorphism.applyMorphism mor) srcSig
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini imageSigList = Set.toList imageSig
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini tarSig = items $ PMorphism.target mor
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder newSig = Set.difference tarSig imageSig
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini sigSize = Set.size tarSig
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder in if sigSize >= maxSigSize
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder then return $ return (Unknown "signature too big", [])
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let imageAxs = map (AS_Anno.mapNamed (PMorphism.mapSentenceH mor)) srcAxs
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini models = allModels (Sign imageSig)
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder newSigList = Set.toList newSig
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini TTHead { hprops = map show imageSigList,
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini haxioms = map AS_Anno.senAttr srcAxs,
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini hextprops = map show newSigList,
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini hextaxioms = map AS_Anno.senAttr tarAxs,
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini hgoal = Nothing
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let evalAx = map (evalNamed m) imageAxs
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder isModel = and evalAx
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder extmodels = allModels (Sign newSig)
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini let evalExtAx = map (evalNamed (m `amalg` m')) tarAxs
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini isExtModel = and evalExtAx
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini in TTExtRow { rextprops = map (`Set.member` m') newSigList,
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini rextaxioms = evalExtAx,
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini rextIsModel = isExtModel
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini extrows = map extrow extmodels
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini in TTRow { rprops = map (`Set.member` m) imageSigList,
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini raxioms = evalAx,
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini rgoal = Nothing,
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini rextrows = if isModel then extrows else [],
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini rIsModel = isModel,
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini rIsOK = not isModel || any rextIsModel extrows
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini rows = map mkRow models
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini isOK = all rIsOK rows
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini table = TruthTable { thead = heading,
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini title = "The extension is " ++ (if isOK then "" else "not ")
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini ++ "conservative"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini legend = "Legend:\n"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ++ "M = model of the axioms\n"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ++ "+ = OK, has expansion\n"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ++ "- = not OK, has no expansion, hence conservativity fails\n"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ++ "o = OK, not a model of the axioms, hence no expansion needed\n"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini body = legend ++ "\n" ++ render id id id (renderTT table)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini res = if isOK then Cons else Inconsistent
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini createTextSaveDisplay title "unnamed" body
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini return $ return (res, [])