did a bunch of stuff

10 files changed, 328 insertions, 0 deletions

diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..2c9b805
--- /dev/null
+++ b/LICENSE
@@ -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.
diff --git a/README.md b/README.md
index e69de29..dbc30f6 100644
--- a/README.md
+++ b/README.md
@@ -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