blob: 7d8c0f938b23eff5b95400350c3aeb2e4aee7522 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
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
|
