diff options
| author | filip <“filip.rabiega@gmail.com”> | 2024-08-16 14:11:00 +0200 |
|---|---|---|
| committer | filip <“filip.rabiega@gmail.com”> | 2024-08-16 14:11:00 +0200 |
| commit | 69de932f9116b30adfd689d38e35ace63aef0e2d (patch) | |
| tree | f7e8621889d313e70186ef255fcf04fe0d55d4c3 /lib/exports.ml | |
| parent | 2e893fd0df7dae8c4ae843d4a23acb098dd97aff (diff) | |
| download | chadprover-master.tar.gz chadprover-master.tar.bz2 chadprover-master.zip | |
Diffstat (limited to 'lib/exports.ml')
| -rw-r--r-- | lib/exports.ml | 12 |
1 files changed, 12 insertions, 0 deletions
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 *) |