module Folly.ResolutionTests(allResolutionTests) where import Folly.Formula import Folly.Resolution import Folly.Theorem import Folly.TestUtils allResolutionTests = do testIsValid testIsValid = testFunction isValid isValidTestCases isValidTestCases :: [(Theorem, Bool)] isValidTestCases = [(theorem [] (fa (var "a") (dis (pr "d" [var "a"]) (neg (pr "d" [var "a"])))), True), (theorem [] (pr "d" [var "k"]), False), (theorem [pr "Dog" [var "x"]] (pr "Dog" [var "x"]), True), (theorem [(fa (var "d") (imp (pr "Dog" [var "d"]) (pr "Loves" [constant "John", var "d"]))), (pr "Dog" [constant "Fido"])] (pr "Loves" [constant "John", constant "Fido"]), True), (theorem [(fa (var "p") (imp (te (var "d") (con (pr "Dog" [var "d"]) (pr "Owns" [var "p", var "d"]))) (pr "LovesAnimals" [var "p"]))), (imp (pr "LovesAnimals" [var "x"]) (fa (var "a") (neg (pr "Kills" [var "x", var "a"])))), (pr "Owns" [constant "John", constant "Fido"]), (pr "Dog" [constant "Fido"])] (fa (var "a") (neg (pr "Kills" [constant "John", var "a"]))), True), (theorem groupWithEquals (imp (con (con (con (pr "=" [func "*" [var "x", var "y"], constant "1"]) (pr "=" [func "*" [var "y", var "x"], constant "1"])) (pr "=" [func "*" [var "x", var "z"], constant "1"])) (pr "=" [func "*" [var "z", var "x"], constant "1"])) (pr "=" [var "y", var "z"])), True), (theorem groupWithEquals (imp (fa (var "x") (con (pr "=" [func "*" [var "x", var "z"], constant "1"]) (pr "=" [func "*" [var "z", var "x"], constant "1"]))) (pr "=" [var "z", constant "1"])), True)] equalityAxioms :: [Formula] equalityAxioms = [(fa (var "x") (pr "=" [var "x", var "x"])), (fa (var "x") (fa (var "y") (imp (pr "=" [var "x", var "y"]) (pr "=" [var "y", var "x"])))), (fa (var "x") (fa (var "y") (fa (var "z") (imp (con (pr "=" [var "x", var "y"]) (pr "=" [var "y", var "z"])) (pr "=" [var "x", var "z"])))))] groupWithEquals = [(fa (var "x") (te (var "y") (con (pr "=" [func "*" [var "x", var "y"], constant "1"]) (pr "=" [func "*" [var "y", var "x"], constant "1"])))), (fa (var "x") (fa (var "y") (fa (var "z") (pr "=" [func "*" [var "x", func "*" [var "y", var "z"]], func "*" [func "*" [var "x", var "y"], var "z"]])))), (fa (var "x") (con (pr "=" [func "*" [var "x", constant "1"], var "x"]) (pr "=" [func "*" [constant "1", var "x"], constant "x"])))] ++ equalityAxioms