import "N3Parser" import "IO" import "Utils" import "XML" import "Load" import "Interact" import "Observe" -- The data structure of this program is based on the Euler program -- by Jos De Roo : http://www.agfa.com/Euler -- The resolution engine is modelled after the mini-prolog interpreter -- of Marc P. Jones in the Hugs distribution. -- BNF for rules (in N3): -- rule ::= "{" triplelist verbimplies triplelist "}" "a" objectTruth ";" -- verbforall objectforall -- ruleSubject ::= triplelist -- triplelist ::= "{" triple* "}" -- triple ::= as usual -- verbimplies ::= "" -- objectTruth ::= "" -- verbforall ::= "" -- objectforall ::= URI ["," URI]* -- BNF of the database: -- -- database ::= clause* -- clause ::= rule | triple -- ** number is sequence number -- ** ref1 is the number of the generating N3 statement in the process -- ** of resolving abbreviations. -- ** ref2 refers to the generating N3 statement for triples that where -- ** embedded in another triple but externalised. -- triple ::= subject verb object [number] [ref1] [ref2] -- subject ::= triplelist | "" content "" -- var ::= "" String String "" -- verb ::= "" content "" -- object ::= triplelist | "" content "" -- triplelist ::= triple* -- number ::= "" n "" -- ref1 ::= "" n "" -- ref2 ::= "" n "" -- n ::= an integer -- rule ::= " " triplelist " " -- log:implies -- " " triple " " -- " " -- a http://www.w3.org/1999/02/22-rdf-syntax-ns#type -- " " -- log:Truth http://www.w3.org/2000/10/swap/log#Truth -- " " -- log:forAll http://www.w3.org/2000/10/swap/log#forAll -- "" objectlist " " -- objectlist ::= ("" content "")* -- -- Mechanism of the engine ----------------------------- -- All abbreviations of N3 have been removed (except for rules) so -- that only triples consisting of subject, verb and object rest -- (No more propertylists or objectlists). However every triple refers -- by a number to the original N3 statement. Embedded triples are -- (depending on a flag) duplicated als single triples with however also -- a reference to the original triple and an indication of its embedded -- origin. -- Unification is done on triple basis. Firsts subjects are unified, -- then verbs, then objects. Each time the current substitution is -- augmented and applied to the next unification. -- Definition of the data structures ---------------------------------------- -- infix definitions for substitutions infixr 3 @@ infix 4 ->- --- Substitutions: type Subst = Var -> Substituted -- a variable is a triple containing the short name of the variable, -- the full name and an integer: -- the integer serves for variable renaming; two variables are equal if they -- have the same name and the same value for the integer -- The format is: name1 name2 integer -- The integer is represented in string format type Var = XMLTree -- substitutions are represented by functions mapping variables to -- substituted values. -- -- app s extends the substitution s to a function mapping terms to terms -- nullSubst is the empty substitution which maps every identifier to the -- same identifier (as a term). -- v ->- t is the substitution which maps the variable v to the term t, -- but otherwise behaves like nullSubst. -- s1@@ s2 is the composition of substitutions s1 and s2 -- s @@ nullSubst = s = nullSubst @@ s app :: Subst -> Substituted -> Substituted app s (Tag tag@("Var",_, _)) = s (Tag tag) -- t is a general XML tree; the substitution has to be applied to all -- variables app s t = applySubstitution s t nullSubst :: Subst nullSubst v = v (->-) :: Var -> Substituted -> Subst (v ->- t) v1 | v1 == v = t | otherwise = v1 (@@) :: Subst -> Subst -> Subst s1 @@ s2 = app s1 . s2 -- a variable can be substituted by a variable, an URI, a general Term or -- Empty. All these are XML trees. type Substituted= XMLTree -- instance (Eq a) => Eq (XMLTree->XMLTree) where -- x1 a == x2 a = False ---------------------------------------------------------------------- -- data structure type DB = [XMLTree] -- Functions ---------------- -- start the interactive engine -- triple, tripleset or anonymous set. -- When finished enter 'q' to stop. startEngine :: IO () startEngine = do is <- getContents putStr (loopE 0 is) type SolveOut = ([Subst], [XMLTree], [Alt], Stack, [XMLTree], [XMLTree]) t = iProof "authen.axiom.n3" "authen.lemma.n3" iProof :: String -> String -> IO () iProof axiom lemma = do s1 <- readFile axiom s2 <- readFile lemma intProof (loadAndGet axiom (n3Parser s1) dbAxiom plist1) (loadAndGet lemma (n3Parser s2) dbLemma plist2) intProof :: XMLTree -> XMLTree -> IO () intProof axiomDB lemmaDB = do is <- getContents putStr ((loopE1 1 (getIdata axiomDB lemmaDB)) is) testGetIdata = putStr (showAlts alts []) where (subs, goals, alts, stack, db, trace) = getIdata testTreeT testQuery getIdata axiomDB lemmaDB = solveI nullSubst lemma1 [] db1 where (db1, varList) = generateExtendedDB axiomDB embedded (lemma1, varList1) = generateExtendedDB lemmaDB False showDBs :: XMLTree -> XMLTree -> IO () showDBs axiomDB lemmaDB = putStr (fileToXML axiomDB) -- this reads a line in a loop and call exec loopE1 :: Int -> SolveOut -> Interact loopE1 state output = readLine "> " (execE1 state output) execE1 :: Int -> SolveOut -> String -> Interact execE1 state solveOut s | bv2 = writeStr "Bye bye !!" end | bv1 = writeStr (writeData "alts = 0" goals) (loopE1 3 solveOut2) -- | bv3 = writeStr "no subs" end -- | bv1 && bv3 = writeStr "end of inference" end | state == 3 = writeStr -- (showStack stack []) -- "state3" (writeData "state3" trace1) -- (showAlts (observe "alts" alts) []) (loopE1 3 solveOut1) | state == 1 = writeStr (showAlts alts[]) -- (writeData "choose" trace3) (loopE1 3 solveOut1) | state == 2 = writeStr (writeData "backtrack" goals) (loopE1 3 solveOut1) | otherwise = writeStr (writeData "choose" trace3) (loopE1 2 solveOut1) where bv1 = length alts == 0 alts2 = [([triple1], nullSubst)] -- bv3 = length subs == 0 bv2 = startsWith s "q" (subs, goals, alts, stack, db, trace3) = solveOut (subs1, goals1, alts1, stack1, db1, trace1) = chooseI subs goals (alts, []) stack db solveOut1 = (subs1, goals1, alts1, stack1, db1, []) solveOut2 = chooseI subs goals (alts2, []) stack db writeData s mytrace = ("\n" ++ s ++ "\n" ++ treeListToXML mytrace ++ "\n") -- this reads a line in a loop and then executes exec loopE :: Int -> Interact loopE state = readLine "> " (execE state) -- this function interprets the input string execE :: Int -> String -> Interact execE state s | state == 3 = writeStr s (loopE 0) | (bv1 || bv2) && state == 0 = writeStr helpMessage (loopE 0) | bv3 && state == 0 = writeStr proofMessage (loopE 1) | bv4 && state == 0 = writeStr "Bye bye !!" end -- | state == 1 = searchProof s (loopE 0) -- | state == 1 && bv6 = loopE1 2 solveOut -- set state 2 -- | bv6 = writeStr (treeListToXML db1) (loopE1 2 solveOut) -- | bv7 = writeStr "bv7" readMyFile -- writeStr (fileToXML db3) (loopE 0) -- (treeListToXML db2) (loopE1 2 solveOut1) -- Entering interactive mode..." (loopE1 2 solveOut) | otherwise = writeStr helpMessage (loopE 0) where bv1 = startsWith s "?" bv2 = startsWith s "help" bv3 = startsWith s "proof" bv7 = startsWith s "p" bv4 = startsWith s "q" bv5 = startsWith s "trace" bv6 = startsWith s "i " s1 = drop 2 s (bool, f1, f2) = parseUntil ' ' s1 state :: Int state = 0 helpMessage = "Semantic web inference engine\n" ++ "================================\n\n" ++ "? = help function\n" ++ "help = help function\n" ++ "proof = start a proof\n" ++ "q or quit = quit the program\n" ++ "trace = trace mode\n" ++ "i = interactive mode type: i axiomfile lemmafile\n" proofMessage = "Enter all axiom files followed by the lemma files\n" -- read a parsed axiom-file, read a parsed lemma-file,execute -- the refutation algorithm and display the result. searchProof fileName1 fileName2 = do s1 <- readFile fileName1 s2 <- readFile fileName2 executeProof (loadAndGet fileName1 (n3Parser s1) dbAxiom plist1) (loadAndGet fileName2 (n3Parser s2) dbLemma plist2) executeIProof axiom lemma = solveI nullSubst lemma1 [] db1 where (db1, varList) = generateExtendedDB axiom embedded (lemma1, varList1) = generateExtendedDB lemma False proofInT fileName1 fileName2 s1 s2 = executeIProofT (loadAndGet fileName1 (n3Parser s1) dbAxiom plist1) (loadAndGet fileName2 (n3Parser s2) dbLemma plist2) executeIProofT axiom lemma = (db1, lemma1) where (db1, varList) = generateExtendedDB axiom embedded (lemma1, varList1) = generateExtendedDB lemma False testSearchProof fileName1 fileName2 = do s1 <- readFile fileName1 s2 <- readFile fileName2 testExecuteProof (loadAndGet fileName1 (n3Parser s1) dbAxiom plist1) (loadAndGet fileName2 (n3Parser s2) dbLemma plist2) -- searches a proof for a query loadAndGet :: String -> String -> XMLTree -> [String] -> XMLTree loadAndGet fileName parseString db plist = (thdTriple (loadString (parseString, plist, db))) dbAxiom = Tag ("DB", Empty, Empty) dbLemma = Tag ("DB", Empty, Empty) plist1 = [] plist2 = [] testExecuteProof axiom lemma = putStr (treeListToXML (queryDB)) where dataBase = markAllVariables db varList 1 -- number variables starting from 1 db = (markRules (generateDB axiom)) varList = eliminateEmpties(eliminateDoubles(getAllVariables db)) queryDB = markAllVariables querydb [] 1 -- number variables starting from 1 querydb = (generateDB lemma) varList1 = eliminateEmpties (getAllVariables1 (queryDB)) printDB = False embedded = False authen = searchProof "authen.axiom.n3" "authen.lemma.n3" danb = searchProof "danb.n3" "danb-query.n3" executeProof axiom lemma | printDB = stringToFile (" axiom db:\n\n" ++ treeListToXML db5 ++ "\n\n axiom variables:\n\n" ++ treeListToXML varList ++ "\n\n lemma db:\n\n" ++ treeListToXML qdb4 ++ "\n\n lemma variables:\n\n" ++ treeListToXML varList1) "databases.db" | otherwise = putStr (showSubstitutionList (fst(proof db5 qdb4)) (varList ++ varList1)) -- stringToFile (fileToXML (snd ( -- proof db5 qdb4))) "proof.eng" where (db5, varList) = generateExtendedDB axiom embedded (qdb4, varList1) = generateExtendedDB lemma False -- this extends the DB by eliminating abbreviations, adding a number -- and duplicating embedded triples if the embedded flag is set -- The passes flag indicates whether embedded triples will be -- instantiated or not. generateExtendedDB :: XMLTree -> Bool -> ([XMLTree], Varlist) generateExtendedDB input embedded | embedded = (db5, varList1) | otherwise = (db6, varList1) where db5 = eliminateDoubles(eliminateEmpties(db4 ++ getEmbedded db4)) db6 = eliminateDoubles(eliminateEmpties db4) db4 = extendDB db3 -- number variables starting from 1 db3 = addUpNumbers (eliminateDoubles( db2 )) 1 "Number" db2 = markAllVariables db1 varList 1 db1 = (markRules (generateDB input)) varList = getAllVariables db1 varList1 = eliminateEmpties(eliminateDoubles( getAllVariables1 db2)) -- read a lemma, load it, generate the DB and print the result testLemma fileName = readExternN3 fileName (loadLemma fileName) where loadLemma fileName parseString = putStr(treeListToXML(queryDB)) where queryDB = markAllVariables querydb [] 1 querydb = generateDB( thdTriple(loadString (parseString, plist2, dbLemma))) -- read a lemma, load it, generate the DB, extend the subjects -- and print the result testLemma1 fileName = readExternN3 fileName (loadLemma fileName) where loadLemma fileName parseString = stringToFile (treeListToXML(queryDB1)) (fileName ++ ".ext") where queryDB1 = extendDB queryDB queryDB = markAllVariables queryDB2 [] 1 queryDB2 = markRules querydb querydb = generateDB( thdTriple(loadString (parseString, plist2, dbLemma))) -- read a lemma, load it, solve the abbreviations, -- generate the embedded triples -- and print the result testLemma2 fileName = readExternN3 fileName (loadLemma fileName) where loadLemma fileName parseString = stringToFile (treeListToXML(queryDB5)) (fileName ++ ".emb") where queryDB4 = eliminateDoubles(eliminateEmpties(queryDB3 ++ (getEmbedded queryDB3 ))) queryDB5 = getEmbedded queryDB3 queryDB3 = extendDB queryDB queryDB = addUpNumbers (eliminateDoubles( (markAllVariables queryDB2 [] 1) )) 1 "Number" queryDB2 = markRules querydb querydb = generateDB( thdTriple(loadString (parseString, plist2, dbLemma))) -- get all embedded triples of a database and add a number -- returns only the embedded triples -- rules are skipped -- These triples are marked by a tag "Ref2" getEmbedded :: [XMLTree] -> [XMLTree] getEmbedded [] = [] getEmbedded (x:xs) | bv1 && s1 == "Rule" = getEmbedded xs | not bv2 && bv3 && not bv4 = numberedChildren ++ getEmbedded xs | otherwise = getEmbedded xs where children = getChildrenByName x "Subject" -- [addTree (Tree (getChildrenByName x "Subject")) x] -- [addTree (Tag ("test",Empty, Empty)) x] bv4 = children == [] children1 = getChildrenByName x "Ref1" (t:cs) = children1 bv3 = testTag t bv2 = children1 == [] c = getContentFromTag t Content (s, _) = c n = stringToInt s numberedChildren = addNumbers children n "Ref2" bv1 = testTag x Tag (s1, _, _) = x -- add a (same) number to each tree in a list -- The string is the name of the tag that contains the number addNumbers :: [XMLTree] -> Int -> String -> [XMLTree] addNumbers [] n s = [] addNumbers (c:cs) n s = addNumber c n:addNumbers cs n s where addNumber c n = addTree c tag1 where tag = Tag (s, Empty, Empty) c1 = Content (intToString n, Empty) tag1 = addTree tag c1 testAddUpNumbers = stringToFile (treeListToXML( addUpNumbers testDB 1 "Number")) "testAddUpNumbers.tst" -- add upgoing numbers to each tree in a list -- The string is the name of the tag that contains the number addUpNumbers :: [XMLTree] -> Int -> String -> [XMLTree] addUpNumbers [] n s = [] addUpNumbers (c:cs) n s = addNumber c n:addUpNumbers cs (n+1) s where addNumber c n = addTree c tag1 where tag = Tag (s, Empty, Empty) c1 = Content (intToString n, Empty) tag1 = addTree tag c1 -- extends the subjects in a DB (eliminate the abbreviations) extendDB :: [XMLTree] -> [XMLTree] extendDB [] = [] extendDB [Empty] = [] extendDB (x:xs) | not bv3 && bv2 && bv4 && bv1 = tree1 ++ extendDB xs | otherwise = extendSubjects tag (-1):extendDB xs where tag = Tree [x] -- Tag ("Temp", x, Empty) children = (getChildrenByName x "Number") (t:cs) = children bv4 = testTag t bv3 = children == [] c = getContentFromTag t Content (s, _) = c n = stringToInt s Tree tree = extendSubjects tag n bv1 = testContent c bv2 = testTag x tree1 = tree extendDB t = [] -- The database is a list of clauses and is constituted by the children -- of the XML tree generated by the module load. -- generate the database from the XML tree generateDB :: XMLTree -> [XMLTree] generateDB db | bv2 = t1 | bv1 = [Tag tag] | otherwise = [] where t = getChildren db bv1 = testTag t bv2 = testTree t Tree t1 = t Tag tag = t -- saveVars fileName = readExternN3 fileName (testGetVars fileName) -- displays a substitution on condition that the substituted -- variable is in the varlist. showSubstitution :: Subst -> Varlist -> String showSubstitution subst [] = "" showSubstitution subst varlist@(v:vs) | subst v == v = showSubstitution subst vs | otherwise = "\nVariable:\n" ++ fileToXML v ++ "\nTerm:\n" ++ fileToXML (subst v) ++ (showSubstitution subst vs) -- display a list of substitutions showSubstitutionList :: [Subst] -> Varlist -> String showSubstitutionList [] varlist = "" showSubstitutionList (s:ss) varlist = showSubstitution s varlist ++ showSubstitutionList ss varlist -- mark the rules in the database markRules :: DB -> DB markRules [] = [] markRules db@(x:xs) | found = tag:markRules xs | otherwise = x:markRules xs where tagList = getAllTags x found = searchContent tagList "log:implies" Tag (name, tree, parent) = x tag = Tag ("Rule", tree, parent) type Varlist = [XMLTree] -- this function marks all variables; the tag is changed to -- . markAllVariables :: DB -> Varlist -> Int -> DB markAllVariables [] varlist i = [] markAllVariables db@(x:xs) varlist i = (markVariables x varlist i):(markAllVariables xs varlist (i + 1)) -- mark the variables in a clause -- The integer parameter is for numbering anonymous variables markVariables :: XMLTree -> Varlist -> Int -> XMLTree markVariables tree varlist i = walkATree tree f where f (Tag tag@("URI", t, p)) | startsWith s "_:" = addTree (Tag ("Var", Empty, p)) (Content ("_" ++ intToString i ++ s, Empty)) | startsWith s "?:" = addTree (Tag ("Var", Empty, p)) (Content ("?" ++ intToString i ++ s, Empty)) | isIn varlist (Tag tag) = Tag tag1 | otherwise = Tag tag where Tag tag1 = Tag ("Var", t, p) Content (s, _) = getChild (Tag tag) f t = t testExtendVerbs = putStr (fileToXML (extendVerbs testTreeT)) -- this extends objectlists into separate triples extendVerbs :: XMLTree -> XMLTree extendVerbs Empty = Empty extendVerbs (Tag tag@("Rule", _, _)) = Tag tag extendVerbs (Tag tag@("Subject", t, p)) = Tag ("Subject", extendVerbs( Tree (content:tree)), p) where verbs = getDirectChildrenByName (Tag tag) "Verb" addVerbs [] = [] addVerbs (v:vs) = extendVerb v ++ addVerbs vs tree = addVerbs verbs content = getChild (Tag tag) extendVerbs (Tag tag@(s, tree,p)) = Tag (s, extendVerbs tree, p) extendVerbs (Tree []) = Tree [] extendVerbs (Tree t@(x:xs)) = merge (Tree [extendVerbs x]) (extendVerbs (Tree xs)) extendVerbs c = c -- everything else testExtendVerb = putStr (treeListToXML( extendVerb verb3)) testGetDirectChildrenByName = putStr(treeListToXML( getDirectChildrenByName verb3 "Object")) extendVerb :: XMLTree -> [XMLTree] extendVerb (Tag v@("Verb", t, p)) = createTree objects where objects = getDirectChildrenByName (Tag v) "Object" content = getChild (Tag v) createTree [] = [] createTree (o:os) = (Tag ("Verb", Tree (content:[o]), p)): createTree os extendVerb t = [t] testExtendSubjects = putStr (fileToXML (extendSubjects triple11 1)) -- this extends propertylists into separate triples extendSubjects :: XMLTree -> Int -> XMLTree extendSubjects Empty n = Empty extendSubjects (Tag tag@("Rule", _, _)) n = Tag tag extendSubjects (Tag tag@(s, t, p)) n | (s /= "Subject") && (subjects /= []) = Tag (s, extendSubjects (Tree tree) n, p) | otherwise = Tag (s, extendSubjects t n, p) where subjects = getDirectChildrenByName (Tag tag) "Subject" addSubjects [] = [] addSubjects (s1:ss) = extendSubject s1 ++ addSubjects ss tree = addNumbers (addSubjects subjects) n "Ref1" extendSubjects (Tree []) n = Tree [] extendSubjects (Tree t@(x:xs)) n = merge (Tree [extendSubjects x n]) (extendSubjects (Tree xs) n) extendSubjects c n = c -- everything else testExtendSubject = putStr (treeListToXML( extendSubject triple1)) extendSubject :: XMLTree -> [XMLTree] extendSubject (Tag s@("Subject", t, p)) = createTree verbs where Tag s1@(s2, t1, p1) = extendVerbs (Tag s) verbs = getDirectChildrenByName (Tag s1) "Verb" content = getChild (Tag s1) createTree [] = [] createTree (v:vs) = (Tag ("Subject", Tree (content:[v]), p1)): createTree vs extendSubject t = [t] -- get the list of variables getAllVariables :: DB -> Varlist getAllVariables [] = [] getAllVariables (x:xs) = (getVariables x) ++ (getAllVariables xs) -- get the variables from a tag getVariables :: XMLTree -> [XMLTree] getVariables t | tagList == [] = [] | otherwise = varList where tagList = selectFromTree t f f (Tag tag@("Verb", t, _)) | bool = [Tag tag] | otherwise = [] where list = getAllTags t bool = searchContent list "log:forAll" || searchContent list "log:forSome" f t = [] (y:ys) = getChildrenByName (Tree tagList) "URI" varList = ys getAllVariables1 :: DB -> Varlist getAllVariables1 [] = [] getAllVariables1 (x:xs) = (getVariables1 x) ++ (getAllVariables1 xs) -- get the variables from a tag getVariables1 :: XMLTree -> [XMLTree] getVariables1 t | tagList == [] = [] | otherwise = varList where tagList = selectFromTree t f f (Tag tag@("Var", _, _)) = [Tag tag] f t = [] varList = getChildrenByName (Tree tagList) "Var" -- unify a triple with a rule. The first clause is a 'simple' triple: -- with one verb and one object. The second is a rule following the bnf -- for rules given higher. -- The last returned parameter is the list of newly generated goals. unifyWithRule :: XMLTree -> XMLTree -> (Bool, Subst, XMLTree, [XMLTree]) unifyWithRule triple rule | bv1 && bool = (True, subst, observe "tree" tree, ts) | otherwise = (False, nullSubst, triple, []) where triples = selectTriplesFromRule rule (bool, subst, tree) = unifyTwoTriples triple t (t:ts) = triples bv1 = length triples > 1 -- get the premisses and the consequent of a rule. -- The first element in the returned list is the consequent. selectTriplesFromRule :: XMLTree -> [XMLTree] selectTriplesFromRule rule = reverse xs where list = selectFromTree rule f f (Tag tag@(s, _, _)) | (s == "Subject") && (bv1 || bv2) = [Tag tag] | otherwise = [] where Tag (s1, _, _) = getChild (Tag tag) bv1 = s1 == "URI" bv2 = s1 == "Var" f t = [] (xs) = eliminateEmpties list -- unify two triples; returns a substitution. -- The first tree has a single verb and a single object; -- the second tree might have multiple verbs and/or objects. -- The first node is . The children can be: or . -- The second triple is returned modified. unifyTwoTriples :: XMLTree -> XMLTree -> (Bool, Subst, XMLTree) unifyTwoTriples t1 t2 = (b1, observe "two" subst1, t3) where -- unify the subjects (b, subst) = unifyAtoms t1 t2 nullSubst v1 = eliminateEmpties (getChildrenByName t1 "Verb") v2 = eliminateEmpties (getChildrenByName t2 "Verb") -- unify the verbs (b1, subst1, v3) = unifyVerbs v1 v2 (observe "two1" subst) -- unification of the objects must be called from unifyVerbs -- reconstitute the second triple t3 = replaceChild t2 v3 s Tag (s, t, p) = v3 -- unify two atoms (subject, verb or object). Returns a substitution -- and a boolean. -- Possibilities: URI with URI; VAR with URI; VAR with VAR. unifyAtoms :: XMLTree -> XMLTree -> Subst -> (Bool, Subst) unifyAtoms Empty _ substIn = (False, nullSubst) unifyAtoms t1 t2 substIn -- this test must be first!!! | t3 == t4 = (True, substIn) | testTag1 && s1 == "Var" = (True, substIn @@ ((Tag c1) ->- t6)) | testTag2 && s2 == "Var" = (True, substIn @@ ((Tag c2) ->- t5)) | otherwise = (False, substIn) where t3 = applySubstitution substIn t1 t4 = applySubstitution substIn t2 Tag c1@(s1, _, _) = t5 Tag c2@(s2, _, _) = t6 testTag1 = testTag t5 testTag2 = testTag t6 t5 = getChild t3 t6 = getChild t4 testTag (Tag c) = True testTag t = False -- unify two "verb"trees. For two matching verbs the corresponding objects -- have to be unified as well. unifyVerbs :: [XMLTree] -> [XMLTree] -> Subst -> (Bool, Subst, XMLTree) unifyVerbs [] _ _ = (False, nullSubst, Empty) unifyVerbs [Empty] _ subst = (False, nullSubst, Empty) unifyVerbs v1 [] subst = (False, nullSubst, Empty) unifyVerbs v1 v2@(v:vs) subst | bool = (bool1, subst2, addTreeAfter v4 (mergeTreeList vs)) | otherwise = (bool2, subst4, addTreeAfter v v3) where -- unify the verbs (bool, subst1) = unifyAtoms (getChild verb) (getChild v) subst [verb] = (observe "v1" v1) -- get the objectlist o1 = eliminateEmpties (getChildrenByName verb "Object") o2 = eliminateEmpties (getChildrenByName v "Object") -- unify the objectlists (bool1, subst2, o3) = unifyObjects o1 o2 subst1 -- reconstitute the second verb v4 = replaceChild v o3 s -- failure; search further (bool2, subst4, v3) = unifyVerbs v1 vs subst Tag (s, p, t) = o3 -- unify two "object"trees. unifyObjects :: [XMLTree] -> [XMLTree] -> Subst -> (Bool, Subst, XMLTree) unifyObjects [] _ _ = (False, nullSubst, Empty) unifyObjects [Empty] _ substIn = (False, nullSubst, Empty) unifyObjects o1 [] substIn = (False, nullSubst, Empty) unifyObjects o1 o2@(o:os) substIn | bool = (observe "bool" bool, subst, addTreeAfter o3 (mergeTreeList os)) | otherwise = (bool1, subst1, addTreeAfter o o2) where -- unify the objects (o4:oss) = observe "o1" o1 (bool, subst, o3) = unifyTwoObjects (observe "o4" o4) (observe "o2" o) substIn -- failure; search further (bool1, subst1, o2) = unifyObjects o1 os substIn -- apply a substitution to a tree applySubstitution :: Subst -> XMLTree -> XMLTree applySubstitution subst tree = walkATree tree f where f (Tag tag@("Var", _, _)) = subst (Tag tag) f t = t -- apply a substitution to a list applySubstitutionToList :: Subst -> [XMLTree] -> [XMLTree] applySubstitutionToList subst [] = [] applySubstitutionToList subst (x:xs) = (applySubstitution subst x):(applySubstitutionToList subst xs) -- unify two objects. This is like unifyAtoms; only the subject is -- marked as being unified. Returns a substitution -- and a boolean. -- Possibilities: URI with URI; VAR with URI; VAR with VAR. unifyTwoObjects :: XMLTree -> XMLTree -> Subst -> (Bool, Subst, XMLTree) --unifyTwoObjects Empty t substIn = (False, nullSubst, t) unifyTwoObjects t1 t2 substIn | not testTag3 = (False, substIn, t2) | testTag2 && s2 == "Var" = (True, substIn @@ ((Tag c2) ->- t5), t3) | testTag1 && s1 == "Var" = (True, substIn @@ ((Tag c1) ->- t6), t4) | t3 == t4 = (True, substIn, t2) | otherwise = (False, substIn, t2) -- return unmodified object where t3 = applySubstitution substIn (observe "t1" t1) t4 = applySubstitution substIn t2 t5 = getChild t3 t6 = getChild (observe "t4" t4) Tag c1@(s1, _, _) = t5 Tag c2@(s2, _, _) = (observe "t6" t6) testTag1 = True --testTag t5 testTag2 = True --testTag t6 testTag3 = True -- observe "test" testValidTag t5 -- testTag4 = (observe "test1" testValidTag t6) testValidTag (Tag t@(s,Tag t1@(s1,_,_),p)) = bv1 where bv1 = s == "URI" || s == "Var" testValidTag (Tag t@(s,Tree t1,p)) = bv1 && bv2 where t2 = getChild (Tree t1) bv1 = testTag t2 Tag (s2, p2, t3) = t2 bv2 = s2 == "URI" || s2 == "Var" testValidTag t = False -- the stack is a list of triples. The first element is the substitution -- at the point where the stack entry is made; the second element is -- the list of outstanding goals and the third element is the list of altenative -- clauses at the snapshot. type Stack = [(Subst, [XMLTree], [Alt])] -- show the contents of the stack showStack :: Stack -> Varlist -> String showStack [] varlist = [] showStack ((s, g, l):xs) varlist = "STACK:\n " ++ "Substitution: " ++ (showSubstitution s varlist) ++ "\n" ++ "Goals: " ++ (treeListToXML g) ++ "\n" ++ "Alts: " ++ (showAlts l varlist) -- show an alternative list showAlts :: [Alt] -> Varlist -> String showAlts [] varlist = [] showAlts (x:xs) varlist = showAlt x varlist ++ showAlts xs varlist -- show an alternative showAlt alt@(treeList, subst) varlist = treeListToXML treeList ++ showSubstitution subst varlist ++ "\nEnd\n" -- an alternative consists of a goal and a substitution that must -- be combined with the substitution that was already found at that -- point. type Alt = ([XMLTree], Subst) -- a proof has as input the database of clauses and a query -- the output is a list of substitutions (one for each found solution) -- and an XMLTree that contains information if the verbose flag is set. -- the query is the initial goallist. proof :: [XMLTree] -> [XMLTree] -> ([Subst], XMLTree) proof db query = solve str nullSubst query [] 0 db solve :: XMLTree -> Subst -> [XMLTree] -> Stack -> Int -> [XMLTree] -> ([Subst], XMLTree) -- when the goal list is empty and the stack is empty all solutions -- have been found; if the goallist is empty but not the stack then -- a backtrack will be done in search of further solutions. solve t subs [] stack n db = (subs:sub, t1) where (sub, t1) = backtrack t stack (n+1) db -- search a solution for the goal at the top of the goallist. solve t subs goals stack n db -- testing n permits to limit the number of loops when -- the limitFlag is set. | n > loopLimit && limitFlag = ([subs], t1) | bv1 = solve t subs [] stack n db | otherwise = choose t1 subs gs1 (getAlts db (app subs g1)) stack (n+1) db where t1 = testVerbose (addTree t (Tag ("solve", Empty, Empty))) goalList = checkGrounded goals bv1 = goalList == [] gl@(g1:gs1) = goalList -- choose an alternative choose :: XMLTree -> Subst -> [XMLTree] -> ([Alt], [XMLTree]) -> Stack -> Int -> [XMLTree] -> ([Subst], XMLTree) -- the list of alternatives is empty; backtrack to -- the last list of alternatives choose t subs gs ([],_) stack n db = backtrack t stack (n+1) db -- add the goals of the first alternative to the goallist -- and combine the substitutions and try to solve; save the -- previous goallist on the stack with the previous substitution -- and the previous list of alternatives. choose t subs gs (altList, altS) stack n db = solve t1 (sub@@subs) (tree ++ gs) ((subs,gs,alts):stack) (n+1) db where t1 = testVerbose (addTree t2 (Tag ("choose", Empty, Empty))) t2 = addTree t (Tree altS) al@((tree,sub):alts) = altList -- If a goal fails then retrieve the last saved situation from -- the stack. backtrack :: XMLTree -> Stack -> Int -> [XMLTree] -> ([Subst], XMLTree) -- stack is empty; nothing to backtrack. backtrack t [] n db = ([], t) backtrack t stack n db = choose t1 subst goals (alts,[]) sts (n+1) db where t1 = testVerbose (addTree t (Tag ("backtrack", Empty, Empty))) st@((subst, goals, alts):sts) = stack -- a proof has as input the database of clauses and a query -- the output is a list of substitutions (one for each found solution) -- and an XMLTree that contains information if the verbose flag is set. -- the query is the initial goallist. proofI :: [XMLTree] -> [XMLTree] -> ([Subst],[XMLTree],[Alt], Stack,[XMLTree], [XMLTree]) proofI db query = solveI nullSubst query [] db -- the interactive solve gets returned: a substitution, the goallist, -- the alternatives [Alt], the stack and the DB. The trace XMLTree -- is not necessary here; neither the limitation integer. -- With the returned values the procs: -- bacttrackI stack db (if the goallist is empty) or -- choose subs gs1 alts stack db -- can be called. solveI :: Subst -> [XMLTree] -> Stack -> [XMLTree] -> ([Subst], [XMLTree], [Alt], Stack, [XMLTree], [XMLTree]) -- when the goal list is empty and the stack is empty all solutions -- have been found; if the goallist is empty but not the stack then -- a backtrack will be done in search of further solutions. solveI subs [] stack db = backtrackI stack db --([subs], [], [], stack, db, []) -- search a solution for the goal at the top of the goallist. solveI subs goals stack db | bv1 = solveI subs [] stack db | otherwise = ([subs], gs1, fst(alts), stack, db, snd(alts)) where goalList = checkGrounded goals alts = getAlts db (app subs g1) bv1 = goalList == [] gl@(g1:gs1) = goalList -- choose an alternative chooseI :: [Subst] -> [XMLTree] -> ([Alt], [XMLTree]) -> Stack -> [XMLTree] -> ([Subst],[XMLTree], [Alt], Stack, [XMLTree], [XMLTree]) -- the list of alternatives is empty; backtrack to -- the last list of alternatives chooseI subst gs ([],_) stack db = backtrackI stack db -- add the goals of the first alternative to the goallist -- and combine the substitutions and try to solve; save the -- previous goallist on the stack with the previous substitution -- and the previous list of alternatives. chooseI (subs:subss) gs (altList, altS) stack db | bv1 = backtrackI stack db | otherwise = (subst1, goals, alts1, stack, db, altS1) where al@((tree,sub):alts) = altList (subst1, goals, alts1, stack, db, altS1) = solveI (sub@@subs) (tree ++ gs) ((subs,gs,alts):stack) db bv1 = length al == 0 -- If a goal fails then retrieve the last saved situation from -- the stack. backtrackI :: Stack -> [XMLTree] -> ([Subst], [XMLTree], [Alt], Stack, [XMLTree], [XMLTree]) -- stack is empty; nothing to backtrack. backtrackI [] db = ([], [], [], [(nullSubst, [], [])], [], []) backtrackI stack db = ([subst], goals, alts, sts, db, []) where st@((subst, goals, alts):sts) = stack str = testVerbose (Tag ("proof", Empty, Empty)) checkGrounded :: [XMLTree] -> [XMLTree] checkGrounded [] = [] checkGrounded (x:xs) | (bv2 && bv1) || t == [] = checkGrounded xs | otherwise = x:checkGrounded xs where t = getChildrenByName x "Var" Tag (s, _, _) = x bv1 = s == "Var" bv2 = testTag x -- if the verbose flag is True then the XMLTree that is input is output -- else an empty XMLTree is returned testVerbose :: XMLTree -> XMLTree testVerbose t | verbose = t | otherwise = Empty -- if the extended flag is True then the XMLTree that is input is output -- else an empty XMLTree is returned testExtended :: XMLTree -> XMLTree testExtended t | extended = t | otherwise = Empty -- get the list of matches of a triple with the heads in the database -- unify and rename the variables -- this is the kernel of the resolution engine -- The first parameter is the database; the second is the goal to unify; -- the third is the rename level. Output is a list of alternatives -- consisting of pairs that contain a clause and a substitution: -- type Alt = (XMLTree, Subst), and an XMLTree that contains trace data. getAlts :: [XMLTree] -> XMLTree -> ([Alt], [XMLTree]) getAlts [] t = ([], []) getAlts (x:xs) t | bv2 && bv1 && bool = ([(eliminateEmpties goals, subst)] ++ alts, out1:out3:out2) | bv2 && (not bv1) && bool1 = ([([t], subst1)] ++ alts, out1:out2) | otherwise = getAlts xs t where Tag (s, _, _) = x bv2 = testTag x bv1 = s == "Rule" -- unify with a rule (bool, subst, t1, goals) = unifyWithRule t x -- unify with a triple (bool1, subst1, t2) = unifyTwoTriples t x (alts, out2) = getAlts xs t out = Tag ("Substitution", Empty, Empty) tree1 = [t, x] -- only trace output when the verbose flag is set out1 = testVerbose (addTree out (Tree tree1)) out4 = Tag ("Goals", Empty, Empty) -- if the extended flag is set the goallist is output too out3 = testExtended (addTree out4 (Tree goals)) -- Test functions and data -------------------------------- -- testdata testTestTreeT = putStr (fileToXML testTreeT) saveTestTreeT = stringToFile (fileToXML testTreeT) "testTreeT.tst" testTreeT = loadDB pa7 testTestQuery = putStr (fileToXML testQuery) testQuery = loadDB pa8 testTestDB = stringToFile (treeListToXML testDB) "testTestDB.tst" testTestQueryDB = putStr (treeListToXML testQueryDB) queryTriple = x where (x:xs) = testQueryDB -- build a query for testing. testQueryDB :: [XMLTree] testQueryDB = markAllVariables db [] 1 -- number variables starting from 1 where db = (generateDB testQuery) -- build a database for testing. testDB :: [XMLTree] testDB = markAllVariables db varList 1 -- number variables starting from 1 where db = (markRules (generateDB testTreeT)) varList = (getAllVariables db) testTestRule = putStr (fileToXML testRule) testRule = x1 where (x:x1:xs) = reverse testDB -- testdata for unification. testTriple1 = putStr (fileToXML triple1) triple1 = x where (x:xs) = testDB triple11 = addTree (addTree (Tag ("Top", Empty, Empty)) (addTree triple1 verb2)) (addTree triple2 verb1) testTriple2 = putStr (fileToXML triple2) triple2 = (getChild(getChild r)) where rules@(r:rs) = eliminateEmpties (getChildrenByName tree "Rule") tree = addTree (Tag ("DB", Empty, Empty)) (mergeTreeList testDB) testVerb1 = putStr (fileToXML verb1) verb1 = v where [v] = eliminateEmpties(getChildrenByName triple1 "Verb") testVerb2 = putStr (fileToXML verb2) verb2 = v where [v] = eliminateEmpties(getChildrenByName triple2 "Verb") verb3 = addTree verb2 object1 testObject1 = putStr (fileToXML object1) object1 = o where [o] = eliminateEmpties(getChildrenByName verb1 "Object") testObject2 = putStr (fileToXML object2) object2 = o where [o] = eliminateEmpties(getChildrenByName verb2 "Object") testTransformVarlist = putStr (treeListToXML testVarlist1) testVarlist = (eliminateEmpties(eliminateDoubles(getAllVariables (markRules (generateDB (testTreeT)))))) testVarlist1 = eliminateEmpties(markAllVariables testVarlist testVarlist 1) testVarlistQ1 = eliminateEmpties(getAllVariables1 (markAllVariables (generateDB testQuery) [] 1)) testAllVarlist = putStr (treeListToXML allVarlist) allVarlist = testVarlist1 ++ testVarlistQ1 testUnifyTwoTriples = putStr(showSubstitution (sndTriple (unifyTwoTriples triple1 triple2)) testVarlist1) testUnifyTwoTriples1 = putStr(fileToXML (thdTriple (unifyTwoTriples triple1 triple2))) testUnifyVerbs = putStr(showSubstitution (sndTriple (unifyVerbs [verb1] [verb2] nullSubst)) testVarlist1) testUnifyVerbs1 = (fstTriple (unifyVerbs [verb1] [verb2] nullSubst)) testUnifyVerbs2 = putStr(fileToXML(thdTriple (unifyVerbs [verb1] [verb2] nullSubst))) testUnifyTwoObjects = putStr(showSubstitution (sndTriple (unifyTwoObjects object1 object2 nullSubst)) testVarlist1) testUnifyTwoObjects1 = (fstTriple (unifyTwoObjects object1 object2 nullSubst)) testUnifyTwoObjects2 = putStr(fileToXML(thdTriple (unifyTwoObjects object1 object2 nullSubst))) testApplySubstitution = putStr (fileToXML (applySubstitution nullSubst object2)) testMergeTreeList = stringToFile (fileToXML (mergeTreeList testDB)) "testMergeTreeList.tst" testMarkRules = stringToFile (treeListToXML (markRules (generateDB( testTreeT)))) "testMarkRules.tst" testGetAllTags = stringToFile (showXMLlist (getAllTags testTreeT)) "testGetAllTags.tst" testGenerateDB = stringToFile (treeListToXML (generateDB testTreeT)) "testGenerateDB.tst" testMarkAllVariables = stringToFile (treeListToXML (markAllVariables db1 varlist 1)) "testMarkAllVariables.tst" where varlist = (getAllVariables db1) db1 = markRules (generateDB (testTreeT)) testMarkAllVariablesQ = stringToFile (treeListToXML (markAllVariables db1 varlist 1)) "testMarkAllVariablesQ.tst" where varlist = (getAllVariables db1) db1 = markRules (generateDB (testQuery)) testMarkVariables = putStr (fileToXML (markVariables testTreeT varlist 1)) where varlist = (getAllVariables db1) db1 = markRules (generateDB (testTreeT)) testSelectTriplesFromRule = putStr (treeListToXML (t:ts)) where (t:ts) = (selectTriplesFromRule testRule) testAdds = putStr (fileToXML (Tag tag2)) where Tag tag1 = Tag ("Var", Empty, Empty) Tag tag2 = addTree (Tag tag1) (Tag tag3) Tag tag3 = addTree (Tag ("Id", Empty, Empty)) (Content ("0", Empty)) testWalkATree1 = putStr (fileToXML (walkATree testTreeT f)) where f t = t testGetAllVariables = putStr (treeListToXML (eliminateDoubles(getAllVariables (markRules (generateDB (testTreeT)))))) testSearchContent = searchContent (getAllTags testTreeT) "log:implies" testUnifyWithRule = putStr ("Subst: " ++ (showSubstitution subst allVarlist) ++ "\nTree: " ++ (fileToXML tree) ++ "\n" ++ (show bool)) where (bool, subst, tree, treeList) = unifyWithRule queryTriple testRule testProof = stringToFile ("Subst: \n" ++ (showSubstitutionList subst varlist) ++ "\nDebug info:\n" ++ fileToXML tree) "testProof.tst" where (subst, tree) = proof testDB testQueryDB varlist = testVarlist1 ++ testVarlistQ1 testGetAlts = stringToFile (showAlts (fst(getAlts testDB x)) varlist) "testGetAlts.tst" where (x:xs) = testQueryDB varlist = testVarlist1 ++ testVarlistQ1 -- constants -------------------- -- the unloaded list of variables varlist :: XMLTree varlist = Tag ("Variables", Empty, Empty) verbose = False extended = False loopLimit :: Int loopLimit = 100 limitFlag = True swaplog = "http://www.w3.org/2000/10/swap/log" impliesURI = swaplog ++ "#implies" varURI = swaplog ++ "#forAll"