diff options
Diffstat (limited to 'bin')
| -rw-r--r-- | bin/dune | 4 | ||||
| -rw-r--r-- | bin/main.ml | 22 |
2 files changed, 26 insertions, 0 deletions
diff --git a/bin/dune b/bin/dune new file mode 100644 index 0000000..5e8e55c --- /dev/null +++ b/bin/dune @@ -0,0 +1,4 @@ +(executable + (public_name power_prover) + (name main) + (libraries power_prover)) diff --git a/bin/main.ml b/bin/main.ml new file mode 100644 index 0000000..eed1a7a --- /dev/null +++ b/bin/main.ml @@ -0,0 +1,22 @@ +open Power_prover.Datatypes + +let show_example p i = + print_endline ("Proposition p: " ^ (string_of_prop p)); + print_endline ("p in NNF: " ^ (string_of_prop (to_nnf p))); + print_endline ("Interpretation i: " ^ (string_of_interpr i)); + print_endline ("p under i: " ^ (string_of_prop (interpret p i)) ^ "\n");; + +let p1 = Not(Not(Not(And(Lit "a", Lit "b"))));; +let p2 = Iff(Not(Implies(Or(Lit "a", Lit "b"), And(Lit "b", Lit "c"))), True);; +let i1 = [("a", false); ("b", true); ("c", false)];; +let i2 = [("a", false); ("b", false)];; +let i3 = [("c", true)];; + +let () = + show_example p1 i1; + show_example p1 i2; + show_example p1 i3; + + show_example p2 i1; + show_example p2 i2; + show_example p2 i3;; |