TypeTheory/resolution
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

Worked on fixing issues

Browse source
This commit is contained in:
reijix 2023-06-04 18:11:28 +02:00
parent 93273f0cc5
commit 69f576b054
1 changed files with 26 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
app/Main.hs
View file

@ -160,12 +160,22 @@ renameBinders f = fst $ go f []
go f' vs = (f', vs)
-- prenex normalform
-- TODO make it so that forall has higher priority to be moved left (makes skolem functions smaller)
makePNF :: Formula -> Formula
makePNF form = go $ renameBinders . makeNNF $ form
where
go f = let f' = pnfStep f in
if f == f' then f else go f'
-- swapping rules
pnfStep (Conj phi (All x psi)) = All x (Conj phi psi)
pnfStep (Disj phi (All x psi)) = All x (Disj phi psi)
pnfStep (Conj (All x psi) phi) = All x (Conj psi phi)
pnfStep (Disj (All x psi) phi) = All x (Disj psi phi)
pnfStep (Conj phi (Exists x psi)) = Exists x (Conj phi psi)
pnfStep (Disj phi (Exists x psi)) = Exists x (Disj phi psi)
pnfStep (Conj (Exists x psi) phi) = Exists x (Conj psi phi)
pnfStep (Disj (Exists x psi) phi) = Exists x (Disj psi phi)
{-
pnfStep (Conj phi (Exists x psi)) = Exists x (Conj phi psi)
pnfStep (Conj phi (All x psi)) = All x (Conj phi psi)
pnfStep (Disj phi (Exists x psi)) = Exists x (Disj phi psi)
@ -174,6 +184,7 @@ makePNF form = go $ renameBinders . makeNNF $ form
pnfStep (Conj (All x psi) phi) = All x (Conj psi phi)
pnfStep (Disj (Exists x psi) phi) = Exists x (Disj psi phi)
pnfStep (Disj (All x psi) phi) = All x (Disj psi phi)
-}
-- descent rules
pnfStep (All x f) = All x (pnfStep f)
pnfStep (Exists x f) = Exists x (pnfStep f)
@ -214,7 +225,7 @@ makeSkolem form = go (makePNF form) [] []
substTermInFormula f@(All y f') x s = if x == y then f else All y (substTermInFormula f' x s)
substTermInFormula f@(Exists y f') x s = if x == y then f else Exists y (substTermInFormula f' x s)
substTermInFormula f _ _ = f
go (All x f) vs skolems = All x (go f (Var x : vs) skolems)
go (All x f) vs skolems = All x (go f (vs ++ [Var x]) skolems)
go (Exists x f) vs skolems = go (substTermInFormula f x (Fun newSkolem vs)) vs (newSkolem : skolems)
where newSkolem = fromJust $ find (`notElem` skolems) skolemFuns
go f _ _ = f
@ -227,12 +238,13 @@ makeCNF form = go $ makeSkolem form
if f == f' then f else go f'
cnfStep (Conj phi psi) = Conj (makeCNF phi) (makeCNF psi)
cnfStep (Disj (Conj phi psi) xi) = Conj (makeCNF $ Disj phi xi) (makeCNF $ Disj psi xi)
--cnfStep (Disj f1 f2) = Disj (makeCNF f1) (makeCNF f2)
cnfStep (Disj xi (Conj phi psi)) = Conj (makeCNF $ Disj xi phi) (makeCNF $ Disj xi psi)
cnfStep (All _ f) = makeCNF f
cnfStep (Exists _ f) = makeCNF f
cnfStep f = f
-- create the list of clauses from a formula
-- TODO not working correctly for `makeCNFList formula5`
makeCNFList :: Formula -> [[Formula]]
makeCNFList form = go $ makeCNF form
where
@ -347,6 +359,18 @@ formula6 = [
[Pred "D" [Fun "a" []]],
[Pred "Q" [Fun "a" []]]]
-- Drogenschmuggel but already as clauses
formula7 :: [[Formula]]
formula7 = [
[Neg $ Pred "E" [Var "x2"], Pred "I" [Var "x2"], Pred "Z" [Fun "f" [Var "x2"]]],
[Neg $ Pred "E" [Var "x3"], Pred "I" [Var "x3"], Pred "S" [Var "x3", Fun "f" [Var "x3"]]],
[Pred "D" [Fun "c" []]],
[Pred "E" [Fun "c" []]],
[Neg $ Pred "S" [Fun "c" [], Var "y"], Pred "D" [Var "y"]],
[Neg $ Pred "I" [Var "x4"], Neg $ Pred "D" [Var "x4"]],
[Neg $ Pred "Z" [Var "x5"], Neg $ Pred "D" [Var "x5"]]
]
main :: IO ()
main = do
putStrLn $ "Now making NNF of formula: " ++ show formula1