Algorithm.FOLModelFinder

Contents

• Formula types
• Model types
• Main function

Description

Synopsis

• type Var = String
• type FSym = String
• type PSym = String
• data GenLit a
  • = Pos a
  • | Neg a
• data Term
  • = TmApp FSym [Term]
  • | TmVar Var
• data Atom = PApp PSym [Term]
• type Lit = GenLit Atom
• type Clause = [Lit]
• type Formula = GenFormula Atom
• data GenFormula a
  • = T
  • | F
  • | Atom a
  • | And (GenFormula a) (GenFormula a)
  • | Or (GenFormula a) (GenFormula a)
  • | Not (GenFormula a)
  • | Imply (GenFormula a) (GenFormula a)
  • | Equiv (GenFormula a) (GenFormula a)
  • | Forall Var (GenFormula a)
  • | Exists Var (GenFormula a)
• toSkolemNF :: forall m. Monad m => (String -> Int -> m FSym) -> Formula -> m [Clause]
• data Model = Model {
  • mUniverse :: [Entity]
  • mRelations :: Map PSym [[Entity]]
  • mFunctions :: Map FSym [([Entity], Entity)]
  }
• type Entity = Int
• showModel :: Model -> [String]
• showEntity :: Entity -> String
• findModel :: Int -> [Clause] -> IO (Maybe Model)

Formula types

Model types

Main function