diff options
| -rw-r--r-- | README.md | 182 | ||||
| -rw-r--r-- | api/dune | 4 | ||||
| -rw-r--r-- | api/handlers.ml | 81 | ||||
| -rw-r--r-- | api/routes.ml | 21 | ||||
| -rw-r--r-- | api/startapp.ml | 26 | ||||
| -rw-r--r-- | bin/dune | 4 | ||||
| -rw-r--r-- | bin/main.ml | 18 | ||||
| -rw-r--r-- | chadprover.opam | 2 | ||||
| -rw-r--r-- | dune-project | 2 | ||||
| -rw-r--r-- | lib/datatypes.ml | 213 | ||||
| -rw-r--r-- | lib/dune | 4 | ||||
| -rw-r--r-- | lib/exports.ml | 12 | ||||
| -rw-r--r-- | lib/input_sanitization/input_sanitizer.ml | 6 | ||||
| -rw-r--r-- | lib/lib_utils.ml | 112 | ||||
| -rw-r--r-- | lib/satisfiability/satisfiable.ml | 74 | ||||
| -rw-r--r-- | lib/sequent_calculus/headers.ml | 5 | ||||
| -rw-r--r-- | lib/sequent_calculus/sequent_proof.ml | 41 | ||||
| -rw-r--r-- | lib/sequent_calculus/sequent_rules.ml | 64 | ||||
| -rw-r--r-- | lib/sequent_calculus/sequents.ml | 72 | ||||
| -rw-r--r-- | lib/to_string.ml | 24 | ||||
| -rw-r--r-- | lib/types.ml | 9 | ||||
| -rw-r--r-- | test/dune | 3 |
22 files changed, 634 insertions, 345 deletions
@@ -1,31 +1,201 @@ -# PowerProver +# Chadprover ## Overview -Experimentation with automated proofs. +An automated theorem-prover for propositional logic. This will be updated for first-order logic. The prover is exposed as an API using the Dream web framework. + +Steps: +1. Lex the raw input (a string representing the formula to prove) to generate a list of tokens. +2. Parse the token list to generate a syntax tree. +3. Check validity? (expensive operation) +4. Run sequent calculus computation on the negation of the formula. +5. Return list of sequents that prove the formula. + +## Lexing + +We first lex the input, obtaining the following possible tokens: + +``` +type tok = + | TRUE + | FALSE + | LIT of string + | NOT + | AND + | OR + | IMPLIES + | IFF + | LEFT_PAREN + | RIGHT_PAREN + | SKIP +``` + +## Parsing + +First, we decided on an appropriate grammar for parsing the token list. + +### Approach 1: Naive Grammar + +#### Simple CFG + +``` +S ::= E $ +E ::= TRUE + | FALSE + | LIT s + | NOT E + | E AND E + | E OR E + | E IMPLIES E + | E IFF E + | LEFT_PAREN E RIGHT_PAREN +``` + +#### Issues +- we need to encode precedence +- above grammar is ambiguous + - consider `NOT E OR E`, which can be parenthesized as `(NOT E) OR E` vs. `NOT (E OR E)` + +### Approach 2: LL(1) Grammar + +#### CFG redefined as LL(1) grammar + +``` +S ::= E $ +E ::= F E' +E' ::= IFF F E' | eps +F ::= G F' +F' ::= IMPLIES G F' | eps +G ::= H G' +G' ::= OR H G' | eps +H ::= I H' +H' ::= AND I H' | eps +I ::= NOT I | LEFT_PAREN E RIGHT_PAREN | TRUE | FALSE | LIT s +``` + +#### FIRST Sets + +``` +FIRST(S) = FIRST(E) + = FIRST(F) + = FIRST(G) + = FIRST(H) + = FIRST(I) + = {TRUE, FALSE, LIT s, NOT, LEFT_PAREN} +FIRST(E') = {IFF, eps} +FIRST(F') = {IMPLIES, eps} +FIRST(G') = {OR, eps} +FIRST(H') = {AND, eps} +``` + +#### FOLLOW Sets + +``` +FOLLOW(E) = {$, RIGHT_PAREN} +FOLLOW(E') = FOLLOW(E) = {$, RIGHT_PAREN} +FOLLOW(F) = FIRST(E') U FOLLOW(E') U FOLLOW(E) = {IFF, $, RIGHT_PAREN} +FOLLOW(F') = FOLLOW(F) = {IFF, $, RIGHT_PAREN} +FOLLOW(G) = FIRST(F') U FOLLOW(F') U FOLLOW(F) = {IMPLIES, IFF, $, RIGHT_PAREN} +FOLLOW(G') = FOLLOW(G) = {IMPLIES, IFF, $, RIGHT_PAREN} +FOLLOW(H) = FIRST(G') U FOLLOW(G') U FOLLOW(G) = {OR, IMPLIES, IFF, $, RIGHT_PAREN} +FOLLOW(H') = FOLLOW(H) = {OR, IMPLIES, IFF, $, RIGHT_PAREN} +FOLLOW(I) = FIRST(H') U FOLLOW(H') U FOLLOW(H) = {AND, OR, IMPLIES, IFF, $, RIGHT_PAREN} +``` + +#### Notes + +- this approach can work, but the grammar is quite convoluted +- LL parsers are relatively straightforward to implement, however, so we opt for this approach (for now) + +### Approach 3: LR Grammar + +#### LR(1) Grammar + +``` +S ::= E $ +E ::= E IFF F | F +F ::= F IMPLIES G | G +G ::= G OR H | H +H ::= H AND I | I +I ::= NOT I | LEFT_PAREN E RIGHT_PAREN | TRUE | FALSE | LIT s +``` + +#### FIRST Sets + +``` +FIRST(S) = FIRST(E) + = FIRST(F) + = FIRST(G) + = FIRST(H) + = FIRST(I) + = {TRUE, FALSE, LIT s, NOT, LEFT_PAREN} +``` + +#### FOLLOW Sets + +``` +TODO +``` + +#### Notes + +- this is probably the best approach with the simplest grammar +- we might switch to an LR parser in the future ## Useful Commands - `dune build` to build the project - `dune test` to run tests -- `dune exec power_prover` to execute the program +- `dune exec chadprover` to execute the program ## Project Log ### Dune Setup -- `dune init proj power_prover` to create project directory (we rename the base dir as *PowerProver*) +- `dune init proj chadprover` to create project directory (we rename the base dir as *Chadprover*) - `dune build` to build the project - `dune test` to run tests -- `dune exec power_prover` to execute the program +- `dune exec chadprover` to execute the program ### Dream Setup - `opam install dream` -- add *dream* to libraries in */bin/dune*: `(libraries power_prover dream)` +- add *dream* to libraries in */bin/dune*: `(libraries chadprover dream)` - add *dream* to package dependencies in */dune-project*: ` (depends ocaml dune dream)` +- add Lwt preprocessing to */bin/dune*: `(preprocess (pps lwt_ppx))` + - this tells dune to preprocess the code with an AST rewriter that can transform Lwt promises (e.g. `let%lwt = ...`) +- same with `ppx_yojson_conv` (Jane Street's library that converts between JSON and OCaml data types) + +### Issues + +- avoid giving a file the same name as its directory; Dune treats both files and directories as modules, so it can't distinguish between them if they have the same name + + +## To Do + +### Short-Term + +- input sanitizer (no inputs longer than set number of vars, no $ signs) +- use OCaml modules +- get API up and running +- read into Lwt library + +### Ideas + +- brute force solver +- prolog solver +- sequent calculus solver (with intermediate steps) + - tableau calculus + - free variable tableau calculus +- propositional and first-order logic +- other L&P parts? +- Hoare logic? + +### Fixes + +- none for now ## Resources diff --git a/api/dune b/api/dune new file mode 100644 index 0000000..9e9e824 --- /dev/null +++ b/api/dune @@ -0,0 +1,4 @@ +(library + (name api) + (libraries chadprover dream) + (preprocess (pps lwt_ppx ppx_yojson_conv))) diff --git a/api/handlers.ml b/api/handlers.ml new file mode 100644 index 0000000..2b8ac5b --- /dev/null +++ b/api/handlers.ml @@ -0,0 +1,81 @@ +(* Handlers for the different endpoints *) + +open Ppx_yojson_conv_lib.Yojson_conv.Primitives +open Chadprover.Exports + +type post_request_data = { + data : string; +} [@@deriving yojson] + +type interpretation = { + assignment : (string * bool) list option; +} [@@deriving yojson] + +let get_data d = d.data + +let health_endpoint _ = + {|{"status": "pass"}|} + |> Dream.json + +let validate_formula_endpoint request = + let%lwt body = Dream.body request in + + let input = + body + |> Yojson.Safe.from_string + |> post_request_data_of_yojson + |> get_data + in + + try + input + |> parse_input + |> Chadprover.To_string.string_of_prop + |> fun s -> "{\"is_formula\": true, \"formula\": \"" ^ s ^ "\"}" + |> Dream.json + + with _ -> (* TODO: 400 Bad Request, error message *) + "{\"is_formula\": false, \"formula\": \"" ^ input ^ "\"}" + |> Dream.json + +let satisfy_endpoint request = + let%lwt body = Dream.body request in + + let input = + body + |> Yojson.Safe.from_string + |> post_request_data_of_yojson + |> get_data + |> parse_input + |> find_satisfying_interpretation + in + + { assignment = input; } + |> yojson_of_interpretation + |> Yojson.Safe.to_string + |> Dream.json + +let sequent_proof_endpoint request = + let%lwt body = Dream.body request in + + let seq_proof = + body + |> Yojson.Safe.from_string + |> post_request_data_of_yojson + |> get_data + |> parse_input + |> get_sequent_calculus_proof + in + + let json_string = + begin + match seq_proof with + | None -> {|{"is_provable": "false"}|} + | Some tree -> + let s = Chadprover.To_string.json_string_of_stree tree in + {|{"is_provable": "true", "sequent_proof": |} ^ s ^ "}" + end + in + + json_string + |> Dream.json diff --git a/api/routes.ml b/api/routes.ml new file mode 100644 index 0000000..74b78ae --- /dev/null +++ b/api/routes.ml @@ -0,0 +1,21 @@ +(* Define the routes for our api *) + +open Handlers + +let routes = [ + + Dream.get "/health" + health_endpoint; + + Dream.post "/validate_formula" + validate_formula_endpoint; + + Dream.post "/satisfy" + satisfy_endpoint; + + Dream.post "/sequent_proof" + sequent_proof_endpoint; + + (* /tableau_calculus_proof *) + +] diff --git a/api/startapp.ml b/api/startapp.ml new file mode 100644 index 0000000..3b459d5 --- /dev/null +++ b/api/startapp.ml @@ -0,0 +1,26 @@ + +(* Middleware to enable CORS for testing purposes *) +let cors_middleware handler request = + let handlers = + [ + "Allow", "OPTIONS, GET, HEAD, POST"; + "Access-Control-Allow-Origin", "*"; + "Access-Control-Allow-Methods", "OPTIONS, GET, HEAD, POST"; + "Access-Control-Allow-Headers", "Content-Type"; + "Access-Control-Max-Age", "86400" + ] + in + + let%lwt res = handler request in + handlers + |> List.map (fun (key, value) -> Dream.add_header res key value) + |> ignore; + Lwt.return res + + (* Create and start the app *) +let startapp () = + Dream.run + @@ Dream.logger + (* @@ Dream.origin_referrer_check *) + @@ cors_middleware (* TODO: remove *) + @@ Dream.router Routes.routes @@ -1,4 +1,4 @@ (executable - (public_name power_prover) + (public_name chadprover) (name main) - (libraries power_prover dream)) + (libraries chadprover api)) diff --git a/bin/main.ml b/bin/main.ml index 19dd333..10a6bc3 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -1,4 +1,16 @@ +(* Entry point for this web application *) + +(* open Chadprover.Types *) +open Chadprover.To_string +(* open Chadprover.Lib_utils *) +open Chadprover.Lexing.Lexer +open Chadprover.Parsing.Parser +(* open Chadprover.Satisfiability.Satisfiable *) + let () = - Dream.run (fun _ -> - Dream.html "Sup yall!" - ) + let lex_result = lex "(p > (q > (p > p)))" in (* "a & b & c = z > x & y | c" *) + let parse_result = parse lex_result in + let proof = Chadprover.Sequent_calculus.Sequent_proof.prove_sequent (Seq([], [parse_result])) in + print string_of_stree proof + +let () = Api.Startapp.startapp () diff --git a/chadprover.opam b/chadprover.opam index 9664991..ed52311 100644 --- a/chadprover.opam +++ b/chadprover.opam @@ -6,6 +6,8 @@ license: "MIT" depends: [ "ocaml" "dune" {>= "3.13"} + "dream" + "ppx_yojson_conv" "odoc" {with-doc} ] build: [ diff --git a/dune-project b/dune-project index 8fc8069..6440d84 100644 --- a/dune-project +++ b/dune-project @@ -11,4 +11,4 @@ (package (name chadprover) (synopsis "Experimentation with automated proofs") - (depends ocaml dune)) + (depends ocaml dune dream ppx_yojson_conv)) diff --git a/lib/datatypes.ml b/lib/datatypes.ml deleted file mode 100644 index 37c61b6..0000000 --- a/lib/datatypes.ml +++ /dev/null @@ -1,213 +0,0 @@ -(* -------------------------------------------------------------------------------------------------------------------- *) -(* ----------------------------------- 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 @@ -1,2 +1,4 @@ +(include_subdirs qualified) + (library - (name power_prover)) + (name chadprover)) diff --git a/lib/exports.ml b/lib/exports.ml new file mode 100644 index 0000000..f9baf73 --- /dev/null +++ b/lib/exports.ml @@ -0,0 +1,12 @@ +(* Functions we want to expose for usage within the api *) + +(* Read string input and convert to proposition *) +let parse_input = Input_sanitization.Input_sanitizer.process + +(* Find a truth assignment satisfying the input proposition or return None *) +let find_satisfying_interpretation = Satisfiability.Satisfiable.satisfy + +(* Find a sequent calculus proof or return None if proposition not provable *) +let get_sequent_calculus_proof = Sequent_calculus.Sequent_proof.prove + +let get_tableau_calculus_proof = () (* TODO *) diff --git a/lib/input_sanitization/input_sanitizer.ml b/lib/input_sanitization/input_sanitizer.ml new file mode 100644 index 0000000..f5c483d --- /dev/null +++ b/lib/input_sanitization/input_sanitizer.ml @@ -0,0 +1,6 @@ +(* Sanitize the inputs *) + +(* TODO: handle exceptions *) +let process (input : string) : Types.proposition = + input |> Lexing.Lexer.lex |> Parsing.Parser.parse + diff --git a/lib/lib_utils.ml b/lib/lib_utils.ml index e9a67b8..5dcbfd7 100644 --- a/lib/lib_utils.ml +++ b/lib/lib_utils.ml @@ -1,59 +1,82 @@ -(* Utility functions for dealing with our new data types *) +(* Utility functions *) open 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);; + | (s, b) :: tl -> (s, if b then True else False) :: (sub_of_interpr tl) -(* Removes instances of True or False literals via simplification *) +(* Removes instances of True or False literals via simplification as well as repeated Nots *) 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')) + begin + match simplify_true_false p with + | True -> False + | False -> True + | Not p' -> p' + | p' -> Not(p') + end | 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')) + begin + 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') + end | 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')) + begin + 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') + end | Implies (p1, p2) -> - (match simplify_true_false p1, simplify_true_false p2 with - | False, _ -> True - | True, p2' -> p2' - | p1', p2' -> Implies(p1', p2')) + begin + match simplify_true_false p1, simplify_true_false p2 with + | False, _ -> True + | True, p2' -> p2' + | p1', p2' -> Implies(p1', p2') + end | 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'));; + begin + match simplify_true_false p1, simplify_true_false p2 with + | True, p2' -> p2' + | p1', True -> p1' + | False, p2' -> + begin (* need to simplify Not(p2'), which depends on the form of p2' *) + match p2' with + | True -> False + | False -> True + | Not p -> p + | p -> Not(p) + end + | p1', False -> + begin (* need to simplify Not(p1') *) + match p1' with + | True -> False + | False -> True + | Not p -> p + | p -> Not(p) + end + | p1', p2' -> Iff(p1', p2') + end (* 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;; + | (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) = +let rec substitute (prop : proposition) (sub : substitution) : proposition = match prop with | True -> True | False -> False @@ -62,7 +85,7 @@ let rec substitute (prop : proposition) (sub : substitution) = | 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);; + | Iff(p1, p2) -> Iff(substitute p1 sub, substitute p2 sub) (* Converts a proposition to negation normal form *) let to_nnf prop = @@ -71,23 +94,30 @@ let to_nnf prop = | 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')) + begin + match p with + | True -> False + | False -> True + | Lit s -> Not(Lit s) + | Not p' -> to_nnf p' + | And(p1, p2) -> Or(to_nnf (Not(p1)), to_nnf (Not(p2))) (* De Morgan's Laws *) + | Or(p1, p2) -> And(to_nnf (Not(p1)), to_nnf (Not(p2))) + | Implies(p1, p2) -> And(to_nnf p1, to_nnf (Not(p2))) (* not (A -> B) = A and not B*) + | Iff(p1, p2) -> Or(And(to_nnf p1, to_nnf (Not(p2))), And(to_nnf (Not(p1)), to_nnf p2)) + end | 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);; + to_nnf (simplify_true_false 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));; +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 *) + | _ -> None (* return None if cannot be determined *) diff --git a/lib/satisfiability/satisfiable.ml b/lib/satisfiability/satisfiable.ml new file mode 100644 index 0000000..6eccc27 --- /dev/null +++ b/lib/satisfiability/satisfiable.ml @@ -0,0 +1,74 @@ +(* Find a satisfying interpretation via brute force *) + +open Types +open Lib_utils + +(* lazy list *) +type 'a seq = Nil | Cons of 'a * (unit -> 'a seq) + +let head = function + | Nil -> None + | Cons(x, _) -> Some x + +let tail = function + | Nil -> None + | Cons(_, tl) -> Some tl + +let rec get k s = + match k, s with + | 0, _ -> [] + | _, Nil -> [] + | k, Cons(x, f) -> x :: get (k - 1) (f ()) + +(* Find all the literals in a formula *) +let extract_symbols (prop : proposition) = + let rec search prop acc = + match prop with + | True -> acc + | False -> acc + | Lit s -> Lit s :: acc + | Not p -> search p acc + | And(p1, p2) -> search p1 (search p2 acc) + | Or(p1, p2) -> search p1 (search p2 acc) + | Implies(p1, p2) -> search p1 (search p2 acc) + | Iff(p1, p2) -> search p1 (search p2 acc) + in + search prop [] + +(* Generate all possible truth assignments for a list of symbols *) +let rec generate_truth_vals symbols = + let rec prepend_all x llist = (* prepend x to each item in the lazy list *) + match llist with + | Nil -> Nil + | Cons(xs, fn) -> Cons(x::xs, fun () -> prepend_all x (fn ())) + in + let rec interleave s1 s2 = + match s1, s2 with + | _, Nil -> s1 + | Nil, _ -> s2 + | Cons(x1, f1), _ -> Cons(x1, fun () -> interleave s2 (f1 ())) + in + match symbols with + | [] -> Cons ([], fun () -> Nil) + | Lit s :: tl -> + let tl_vals = generate_truth_vals tl in + let s_true = prepend_all (s, true) tl_vals in + let s_false = prepend_all (s, false) tl_vals in + interleave s_true s_false + | _ -> failwith "discovered a bug" + +(* brute force search for a satisfying interpretation *) +let satisfy prop = + let symbols = extract_symbols prop in + let truth_vals = generate_truth_vals symbols in + let rec try_next truth_vals = + match truth_vals with + | Nil -> None + | Cons(i, f) -> + begin + match test_interpretation prop i with + | Some true -> Some i + | _ -> try_next (f ()) + end + in + try_next truth_vals diff --git a/lib/sequent_calculus/headers.ml b/lib/sequent_calculus/headers.ml new file mode 100644 index 0000000..0bef07a --- /dev/null +++ b/lib/sequent_calculus/headers.ml @@ -0,0 +1,5 @@ +(* Sequent calculus: types and exceptions *) + +(* exceptions that can occur when attempting a sequent proof *) +exception RuleNotApplicable +exception NotProvable of string diff --git a/lib/sequent_calculus/sequent_proof.ml b/lib/sequent_calculus/sequent_proof.ml new file mode 100644 index 0000000..7d8c0f9 --- /dev/null +++ b/lib/sequent_calculus/sequent_proof.ml @@ -0,0 +1,41 @@ +(* Sequent Calculus *) + +open Types +open Headers +open Sequent_rules + +(* returns true if arg is the basic tautological sequent *) +let rec is_basic_sequent (Seq(l1, l2)) = + match l1 with + | [] -> false + | p :: ps -> List.mem p l2 || is_basic_sequent (Seq (ps, l2)) + +(* gives list of sequents that need to be proved for this to be true *) +let get_dependencies (s : seq) : seq list = + let rec apply_each fns s = (* apply each fn to s and return first result *) + match fns with + | [] -> raise (NotProvable "Couldn't find proof") + | fn :: fns -> + try + fn s + with + | RuleNotApplicable -> apply_each fns s + in + if is_basic_sequent s then + [] + else + apply_each rule_precedence_list s + +(* generates a proof for a sequent in stree form or throws an exception *) +(* TODO: deal with <-> case *) +let rec prove_sequent (s : seq) : stree = + let dependencies = get_dependencies s in + let proofs = List.map prove_sequent dependencies in + Concl(s, proofs) + +(* Prove a proposition via the sequent calculus or return None if not provable *) +let prove (p : proposition): stree option = + try + Some (prove_sequent (Seq ([], [p]))) + with NotProvable _ -> + None diff --git a/lib/sequent_calculus/sequent_rules.ml b/lib/sequent_calculus/sequent_rules.ml new file mode 100644 index 0000000..68f2b63 --- /dev/null +++ b/lib/sequent_calculus/sequent_rules.ml @@ -0,0 +1,64 @@ +(* Logic for applying sequent calculus rules *) + +open Types +open Headers + +(* apply NOT rule for LHS if possible *) +let rec not_lhs = function + | Seq([], _) -> raise RuleNotApplicable + | Seq(Not(p1) :: p1s, p2s) -> [Seq(p1s, p1 :: p2s)] + | Seq(_ :: p1s, p2s) -> not_lhs (Seq(p1s, p2s)) + +(* apply NOT rule for RHS if possible *) +let rec not_rhs = function + | Seq(_, []) -> raise RuleNotApplicable + | Seq(p1s, Not(p2) :: p2s) -> [Seq(p2 :: p1s, p2s)] + | Seq(p1s, _ :: p2s) -> not_rhs (Seq(p1s, p2s)) + +(* apply AND rule for LHS if possible *) +let rec and_lhs = function + | Seq([], _) -> raise RuleNotApplicable + | Seq(And(p1, p1') :: p1s, p2s) -> [Seq(p1 :: p1' :: p1s, p2s)] + | Seq(_ :: p1s, p2s) -> and_lhs (Seq(p1s, p2s)) + +(* apply AND rule for RHS if possible *) +let rec and_rhs = function + | Seq(_, []) -> raise RuleNotApplicable + | Seq(p1s, And(p2, p2') :: p2s) -> [Seq(p1s, p2 :: p2s); Seq(p1s, p2' :: p2s)] + | Seq(p1s, _ :: p2s) -> and_rhs (Seq(p1s, p2s)) + +(* apply OR rule for LHS if possible *) +let rec or_lhs = function + | Seq([], _) -> raise RuleNotApplicable + | Seq(Or(p1, p1') :: p1s, p2s) -> [Seq(p1 :: p1s, p2s); Seq(p1' :: p1s, p2s)] + | Seq(_ :: p1s, p2s) -> or_lhs (Seq(p1s, p2s)) + +(* apply OR rule for RHS if possible *) +let rec or_rhs = function + | Seq(_, []) -> raise RuleNotApplicable + | Seq(p1s, Or(p2, p2') :: p2s) -> [Seq(p1s, p2 :: p2' :: p2s)] + | Seq(p1s, _ :: p2s) -> or_rhs (Seq(p1s, p2s)) + +(* apply -> rule for LHS if possible *) +let rec implies_lhs = function + | Seq([], _) -> raise RuleNotApplicable + | Seq(Implies(p1, p1') :: p1s, p2s) -> [Seq(p1s, p1 :: p2s); Seq(p1' :: p1s, p2s)] + | Seq(_ :: p1s, p2s) -> implies_lhs (Seq(p1s, p2s)) + +(* apply -> rule for RHS if possible *) +let rec implies_rhs = function + | Seq(_, []) -> raise RuleNotApplicable + | Seq(p1s, Implies(p2, p2') :: p2s) -> [Seq(p2 :: p1s, p2' :: p2s)] + | Seq(p1s, _ :: p2s) -> implies_rhs (Seq(p1s, p2s)) + +(* precedence rules for applying rules *) +let rule_precedence_list = [ + and_lhs; (* reduce AND on LHS *) + or_rhs; (* reduce OR on RHS *) + not_lhs; (* reduce NOT on LHS *) + not_rhs; (* reduce NOT on RHS *) + implies_rhs; (* reduce -> on RHS *) + or_lhs; (* reduce OR on LHS *) + and_rhs; (* reduce AND on RHS *) + implies_lhs (* reduce -> on LHS *) +] diff --git a/lib/sequent_calculus/sequents.ml b/lib/sequent_calculus/sequents.ml deleted file mode 100644 index 0b4a33a..0000000 --- a/lib/sequent_calculus/sequents.ml +++ /dev/null @@ -1,72 +0,0 @@ - -(* Sequent Calculus *) - -open Types -open To_string - - -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/to_string.ml b/lib/to_string.ml index 30e909b..5d74adf 100644 --- a/lib/to_string.ml +++ b/lib/to_string.ml @@ -1,3 +1,5 @@ +(* Various to_string and print functions *) + open Types let rec string_of_prop = function @@ -8,23 +10,24 @@ let rec string_of_prop = function | 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) ^ ")";; + | 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) ^ "]";; + 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) ^ "]";; + in "[" ^ (stringify i) ^ "]" -let print_prop prop = print_endline (string_of_prop prop);; +let print string_of_x x = x |> string_of_x |> print_endline +let print_prop prop = print string_of_prop prop let string_of_tok = function | TRUE -> "TRUE" @@ -42,3 +45,16 @@ let string_of_tok = function let rec string_of_tokens = function | [] -> "" | t :: ts -> "[" ^ string_of_tok t ^ "] " ^ string_of_tokens ts + +let string_of_seq (Seq (p1s, p2s)) = + let p1_string = String.concat ", " (List.map string_of_prop p1s) in + let p2_string = String.concat ", " (List.map string_of_prop p2s) in + p1_string ^ " ⇒ " ^ p2_string + +let rec string_of_stree = function + | Concl(s, []) -> "[" ^ string_of_seq s ^ "]" + | Concl(s, trees) -> "Seq(" ^ string_of_seq s ^ "| " ^ (String.concat "; " (List.map string_of_stree trees)) ^ ")" + +let rec json_string_of_stree = function + | Concl(s, []) -> "[\"" ^ string_of_seq s ^ "\", []]" + | Concl(s, trees) -> "[\"" ^ string_of_seq s ^ "\", [" ^ (String.concat ", " (List.map json_string_of_stree trees)) ^ "]]" diff --git a/lib/types.ml b/lib/types.ml index bf6a34d..a069cbd 100644 --- a/lib/types.ml +++ b/lib/types.ml @@ -12,7 +12,7 @@ type proposition = | Iff of proposition * proposition (* interpretation of propositional symbols *) -type interpretation = (string * bool) list +type interpretation = (string * bool) list (* note: we're using OCaml booleans here *) (* allows us to substitute any proposition for any atomic literal *) type substitution = (string * proposition) list @@ -30,3 +30,10 @@ type tok = | LEFT_PAREN | RIGHT_PAREN | SKIP + +(* sequent *) +type seq = Seq of proposition list * proposition list + +(* tree of sequents where Conclusion(s, l) represents a sequent s and a list l of + * strees that together prove s *) +type stree = Concl of seq * stree list @@ -1,2 +1,3 @@ (test - (name test_chadprover)) + (name test_lexing) ; TODO: change back to test_chadprover + (libraries chadprover)) |