diff options
| -rw-r--r-- | LICENSE | 21 | ||||
| -rw-r--r-- | README.md | 26 | ||||
| -rw-r--r-- | bin/dune | 4 | ||||
| -rw-r--r-- | bin/main.ml | 22 | ||||
| -rw-r--r-- | chadprover.opam | 24 | ||||
| -rw-r--r-- | dune-project | 14 | ||||
| -rw-r--r-- | lib/datatypes.ml | 213 | ||||
| -rw-r--r-- | lib/dune | 2 | ||||
| -rw-r--r-- | test/dune | 2 | ||||
| -rw-r--r-- | test/test_chadprover.ml | 0 |
10 files changed, 328 insertions, 0 deletions
@@ -0,0 +1,21 @@ +MIT License + +Copyright (c) 2024 Kai Vennemann + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. @@ -0,0 +1,26 @@ +# Chadprover + +## Overview + +Experimentation with automated proofs. + + +## Useful Commands + +- `dune build` to build the project +- `dune test` to run tests +- `dune exec power_prover` to execute the program + + +## Project Log + +### Dune Setup + +- `dune init proj power_prover` to create project directory (we rename the base dir as *PowerProver*) + + +## Resources + +- https://dune.readthedocs.io/en/latest/quick-start.html +- https://ocaml.org/docs/compiling-ocaml-projects +- https://aantron.github.io/dream/ 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;; diff --git a/chadprover.opam b/chadprover.opam new file mode 100644 index 0000000..9664991 --- /dev/null +++ b/chadprover.opam @@ -0,0 +1,24 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +synopsis: "Experimentation with automated proofs" +authors: ["Filip Rabiega"] +license: "MIT" +depends: [ + "ocaml" + "dune" {>= "3.13"} + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] diff --git a/dune-project b/dune-project new file mode 100644 index 0000000..8fc8069 --- /dev/null +++ b/dune-project @@ -0,0 +1,14 @@ +(lang dune 3.13) + +(name chadprover) + +(generate_opam_files true) + +(authors "Filip Rabiega") + +(license MIT) + +(package + (name chadprover) + (synopsis "Experimentation with automated proofs") + (depends ocaml dune)) diff --git a/lib/datatypes.ml b/lib/datatypes.ml new file mode 100644 index 0000000..37c61b6 --- /dev/null +++ b/lib/datatypes.ml @@ -0,0 +1,213 @@ +(* -------------------------------------------------------------------------------------------------------------------- *) +(* ----------------------------------- Data types useful for our theorem prover(s) ------------------------------------ *) +(* -------------------------------------------------------------------------------------------------------------------- *) + +type proposition = (* logical proposition *) + | True + | False + | Lit of string + | Not of proposition + | And of proposition * proposition + | Or of proposition * proposition + | Implies of proposition * proposition + | Iff of proposition * proposition;; + +type interpretation = (string * bool) list;; (* interpretation *) + +type substitution = (string * proposition) list;; (* allows us to substitute any proposition for any atomic literal *) + + +(* -------------------------------------------------------------------------------------------------------------------- *) +(* ----------------------------------------- Utility functions for debugging ------------------------------------------ *) +(* -------------------------------------------------------------------------------------------------------------------- *) + +let rec string_of_prop = function + | True -> "True" + | False -> "False" + | Lit symbol -> symbol + | Not p -> "¬" ^ (string_of_prop p) + | And (p1, p2) -> "(" ^ (string_of_prop p1) ^ " ∧ " ^ (string_of_prop p2) ^ ")" + | Or (p1, p2) -> "(" ^ (string_of_prop p1) ^ " ∨ " ^ (string_of_prop p2) ^ ")" + | Implies (p1, p2) -> "(" ^ (string_of_prop p1) ^ " → " ^ (string_of_prop p2) ^ ")" + | Iff (p1, p2) -> "(" ^ (string_of_prop p1) ^ " ↔ " ^ (string_of_prop p2) ^ ")";; + + let string_of_sub sub = + let rec stringify = function + | [] -> "" + | (s, value) :: [] -> "(" ^ s ^ ": " ^ (string_of_prop value) ^ ")" + | (s, value) :: tl -> "(" ^ s ^ ": " ^ (string_of_prop value) ^ "), " ^ (stringify tl) + in "[" ^ (stringify sub) ^ "]";; + +let string_of_interpr (i : interpretation) = + let rec stringify = function + | [] -> "" + | (s, value) :: [] -> "(" ^ s ^ ": " ^ (string_of_bool value) ^ ")" + | (s, value) :: tl -> "(" ^ s ^ ": " ^ (string_of_bool value) ^ "), " ^ (stringify tl) + in "[" ^ (stringify i) ^ "]";; + +let print_prop prop = print_endline (string_of_prop prop);; + + +(* -------------------------------------------------------------------------------------------------------------------- *) +(* ------------------------------ Utility functions for dealing with our new data types ------------------------------- *) +(* -------------------------------------------------------------------------------------------------------------------- *) + +(* Converts an interpretation to a substitution *) +let rec sub_of_interpr = function + | [] -> [] + | (s, b) :: tl -> (s, if b then True else False) :: (sub_of_interpr tl);; + +(* Removes instances of True or False literals via simplification *) +let rec simplify_true_false = function + | True -> True + | False -> False + | Lit symbol -> Lit symbol + | Not p -> + (match simplify_true_false p with + | True -> False + | False -> True + | Not p' -> p' + | p' -> Not(p')) + | And (p1, p2) -> + (match simplify_true_false p1, simplify_true_false p2 with + | False, _ -> False + | _, False -> False + | True, p2' -> p2' + | p1', True -> p1' + | p1', p2' -> And(p1', p2')) + | Or (p1, p2) -> + (match simplify_true_false p1, simplify_true_false p2 with + | True, _ -> True + | _, True -> True + | False, p2' -> p2' + | p1', False -> p1' + | p1', p2' -> Or(p1', p2')) + | Implies (p1, p2) -> + (match simplify_true_false p1, simplify_true_false p2 with + | False, _ -> True + | True, p2' -> p2' + | p1', p2' -> Implies(p1', p2')) + | Iff (p1, p2) -> + (match simplify_true_false p1, simplify_true_false p2 with + | True, p2' -> p2' + | p1', True -> p1' + | False, p2' -> simplify_true_false (Not(p2')) + | p1', False -> simplify_true_false (Not(p1')) + | p1', p2' -> Iff(p1', p2'));; + +(* Finds a symbol in a list of substitutions and returns the value to substitute for that symbol *) +let rec replace sub symbol = + match sub with + | [] -> Lit symbol + | (s, value) :: sub -> if s = symbol then value else replace sub symbol;; + +(* Substitutes propositions for symbols as specified by the sub argument *) +let rec substitute (prop : proposition) (sub : substitution) = + match prop with + | True -> True + | False -> False + | Lit s -> replace sub s + | Not p -> Not (substitute p sub) + | And(p1, p2) -> And(substitute p1 sub, substitute p2 sub) + | Or(p1, p2) -> Or(substitute p1 sub, substitute p2 sub) + | Implies(p1, p2) -> Implies(substitute p1 sub, substitute p2 sub) + | Iff(p1, p2) -> And(substitute p1 sub, substitute p2 sub);; + +(* Converts a proposition to negation normal form *) +let to_nnf prop = + let rec to_nnf = function + | True -> True + | False -> False + | Lit symbol -> Lit symbol + | Not p -> + (match to_nnf p with + | And(p1, p2) -> Or(to_nnf (Not(p1)), to_nnf (Not(p2))) + | Or(p1, p2) -> And(to_nnf (Not(p1)), to_nnf (Not(p2))) + | p' -> simplify_true_false (Not p')) + | And(p1, p2) -> And(to_nnf p1, to_nnf p2) + | Or(p1, p2) -> Or(to_nnf p1, to_nnf p2) + | Implies(p1, p2) -> to_nnf (Or(Not(p1), p2)) + | Iff(p1, p2) -> to_nnf (And(Implies(p1, p2), Implies(p2, p1))) + in + simplify_true_false (to_nnf prop);; + +(* Applies an interpretation to a proposition and returns the resulting proposition *) +let interpret prop i = simplify_true_false (substitute prop (sub_of_interpr i));; + +(* Tests whether a proposition holds under a given interpretation *) +let test_interpretation prop i = + match interpret prop i with + | True -> Some true + | False -> Some false + | _ -> None;; (* return None if cannot be determined *) + + +(* -------------------------------------------------------------------------------------------------------------------- *) +(* --------------------------------- Sequent Calculus (TODO: move this to dif file) ----------------------------------- *) +(* -------------------------------------------------------------------------------------------------------------------- *) + +type seq = Seq of proposition list * proposition list;; (* sequent *) + +type stree = (* tree of sequents *) + | Taut (* tautology of the form A, Gamma => A, Delta *) + | Br of stree * stree + +let string_of_seq (Seq (p1, p2)) = + let rec string_of_prop_list = function + | [] -> "" + | p :: ps -> (string_of_prop p) ^ ", " ^ (string_of_prop_list ps) + in + (string_of_prop_list p1) ^ "⇒" ^ (string_of_prop_list p2);; + +(* let rec reduce_seq s = + let rec not_lhs (Seq(p1s, p2s)) = + match p1s with + | [] -> Seq(p1s, p2s), None, false + | p::ps -> + (match p with + | Not(p') -> Seq(ps, p'::p2s), None, true + | _ -> let Seq(ps', p2s), _, found = not_lhs (Seq(ps, p2s)) in Seq(p::ps', p2s), None, found) + in + let rec not_rhs (Seq(p1s, p2s)) = + match p2s with + | [] -> Seq(p1s, p2s), None, false + | p::ps -> + (match p with + | Not(p') -> Seq(p'::p1s, ps), None, true + | _ -> let Seq(p1s, ps'), _, found = not_rhs (Seq(p1s, ps)) in Seq(p1s, p::ps'), None, found) + in + let rec and_lhs (Seq(p1s, p2s)) = + match p1s with + | [] -> Seq(p1s, p2s), None, false + | p::ps -> + (match p with + | And(p1, p2) -> Seq(p1::p2::ps, p2s), None, true + | _ -> let Seq(p1s, ps'), _, found = and_lhs (Seq(p1s, ps)) in Seq(p1s, p::ps'), None, found) + in + let rec and_rhs (Seq(p1s, p2s)) = + match p2s with + | [] -> Seq(p1s, p2s), None, false + | p::ps -> + (match p with + | And(p1, p2) -> Seq(p1s, p1::ps), Some (Seq(p1s, p2::ps)), true + | _ -> + (match and_rhs (Seq(p1s, ps)) with + | Seq(p1s, ps'), None, found -> Seq(p1s, p2s), None, false + | Seq(p1s, ps'), Some (Seq(p1s', ps'')), found -> Seq(p1s, p::ps'), Some (Seq(p1s', p::ps'')), true)) + in + match s with + | Seq *) + + (* + Steps (repeat in this order): + - reduce AND on LHS + - reduce OR on RHS + - reduce NOT on LHS + - reduce NOT on RHS + - reduce -> (RHS) + - reduce <-> (both) + - reduce OR (LHS) + - reduce AND (RHS) + - reduce -> (LHS) + *) +
\ No newline at end of file diff --git a/lib/dune b/lib/dune new file mode 100644 index 0000000..5612af0 --- /dev/null +++ b/lib/dune @@ -0,0 +1,2 @@ +(library + (name power_prover)) diff --git a/test/dune b/test/dune new file mode 100644 index 0000000..96dc350 --- /dev/null +++ b/test/dune @@ -0,0 +1,2 @@ +(test + (name test_chadprover)) diff --git a/test/test_chadprover.ml b/test/test_chadprover.ml new file mode 100644 index 0000000..e69de29 --- /dev/null +++ b/test/test_chadprover.ml |