wball/proof-checker
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Compare commits

base: wball:420a2418c3722fddd9534a709e199ca91bf1452a
Branches Tags
wball:main
..
compare: wball:9bf17c66fd0475f6cdea1a8b8c86f1c08bd43360
Branches Tags
wball:main

No commits in common. "420a2418c3722fddd9534a709e199ca91bf1452a" and "9bf17c66fd0475f6cdea1a8b8c86f1c08bd43360" have entirely different histories.
420a2418c3 ... 9bf17c66fd

10 changed files with 2 additions and 349 deletions
Show stats Expand all files Collapse all files

3
.gitignore vendored
View file

@ -1,3 +0,0 @@
**/*.du
**/*.ud
lib/github.com/*

3
README.md
View file

@ -1,2 +1,3 @@
# proof-checker
Proof checker based on first order logic. The eventual goal is to be as readable and natural as possible.
testing blah blah
wow it's working!

17
lib/forgejo.ballcloud.cc/wball/proof-checker/FORMULA.sig
View file

@ -1,17 +0,0 @@
signature FORMULA =
sig
datatype t =
Named of string
| Relation of string * Term.t list
| Equal of Term.t * Term.t
| Bottom
| Neg of t
| Conj of t * t
| Disj of t * t
| Impl of t * t
| Iff of t * t
| Forall of t
| Exists of t
val eq: t * t -> bool
end

35
lib/forgejo.ballcloud.cc/wball/proof-checker/Formula.sml
View file

@ -1,35 +0,0 @@
structure Formula: FORMULA =
struct
datatype t =
Named of string
| Relation of string * Term.t list
| Equal of Term.t * Term.t
| Bottom
| Neg of t
| Conj of t * t
| Disj of t * t
| Impl of t * t
| Iff of t * t
| Forall of t
| Exists of t
fun eq (Named s1, Named s2) = s1 = s2
| eq (Relation (r, ts), Relation (p, ss)) =
(r = p andalso List.all Term.eq (ListPair.zip (ts, ss))
handle unequalLengths => false)
| eq (Equal (t, s), Equal (t', s')) =
Term.eq (t, t') andalso Term.eq (s, s')
| eq (Bottom, Bottom) = true
| eq (Neg phi, Neg psi) = eq (phi, psi)
| eq (Conj (phi, psi), Conj (phi', psi')) =
eq (phi, phi') andalso eq (psi, psi')
| eq (Disj (phi, psi), Disj (phi', psi')) =
eq (phi, phi') andalso eq (psi, psi')
| eq (Impl (phi, psi), Impl (phi', psi')) =
eq (phi, phi') andalso eq (psi, psi')
| eq (Iff (phi, psi), Iff (phi', psi')) =
eq (phi, phi') andalso eq (psi, psi')
| eq (Forall phi, Forall psi) = eq (phi, psi)
| eq (Exists phi, Exists psi) = eq (phi, psi)
| eq _ = false
end

28
lib/forgejo.ballcloud.cc/wball/proof-checker/PROOF.sig
View file

@ -1,28 +0,0 @@
signature PROOF =
sig
datatype label =
Axiom
| AndI
| AndE
| OrI
| OrE
| ArrI
| ArrE
| NegI
| NegE
| RAA
| IffI
| IffE
| EqI
| EqE
| ForAllI
| ForAllE
| ExistsI
| ExistsE
exception ProofError of int
datatype t = Proof of {children: t list, label: label, formula: Formula.t}
val valid: t * Formula.t list -> bool
end

225
lib/forgejo.ballcloud.cc/wball/proof-checker/Proof.sml
View file

@ -1,225 +0,0 @@
structure Proof: PROOF =
struct
datatype label =
Axiom
| AndI
| AndE
| OrI
| OrE
| ArrI
| ArrE
| NegI
| NegE
| RAA
| IffI
| IffE
| EqI
| EqE
| ForAllI
| ForAllE
| ExistsI
| ExistsE
exception ProofError of int
datatype t = Proof of {children: t list, label: label, formula: Formula.t}
local open Formula
in
infix eq
fun valid
( Proof
{ children =
kids as
[Proof {formula = phi, ...}, Proof {formula = psi, ...}]
, label = AndI
, formula = Conj (phi', psi')
}
, a
) =
phi eq phi' andalso psi eq psi'
andalso List.all (fn k => valid (k, a)) kids
| valid
( Proof
{ children = [kid as Proof {formula = Conj (phi, psi), ...}]
, label = AndE
, formula = chi
}
, a
) =
chi eq phi orelse chi eq psi andalso valid (kid, a)
| valid (Proof {children = [], label = Axiom, formula = phi}, a) =
let
fun mem (phi, []) = false
| mem (phi, x :: xs) =
phi eq x orelse mem (phi, xs)
in
mem (phi, a)
end
| valid
( Proof
{ children = [kid as Proof {formula = phi, ...}]
, label = OrI
, formula = Disj (psi, chi)
}
, a
) =
(phi eq psi orelse phi eq chi) andalso valid (kid, a)
| valid
( Proof
{ children =
[ left as Proof {formula = Disj (phi, psi), ...}
, mid as Proof {formula = chi, ...}
, right as Proof {formula = chi', ...}
]
, label = OrE
, formula = chi''
}
, a
) =
chi eq chi' andalso chi' eq chi'' andalso valid (left, a)
andalso valid (mid, phi :: a) andalso valid (right, psi :: a)
| valid
( Proof
{ children = [kid as Proof {formula = psi, ...}]
, label = ArrI
, formula = Impl (phi, psi')
}
, a
) =
psi eq psi' andalso valid (kid, phi :: a)
| valid
( Proof
{ children =
[ left as Proof {formula = Impl (phi, psi), ...}
, right as Proof {formula = phi', ...}
]
, label = ArrE
, formula = psi'
}
, a
) =
phi eq phi' andalso psi eq psi' andalso valid (left, a)
andalso valid (right, a)
| valid
( Proof
{ children = [kid as Proof {formula = Bottom, ...}]
, label = NegI
, formula = Neg phi
}
, a
) =
valid (kid, phi :: a)
| valid
( Proof
{ children =
[ left as Proof {formula = Neg phi, ...}
, right as Proof {formula = phi', ...}
]
, label = NegE
, formula = Bottom
}
, a
) =
phi eq phi' andalso valid (left, a) andalso valid (right, a)
| valid
( Proof
{ children = [kid as Proof {formula = Bottom, ...}]
, label = RAA
, formula = phi
}
, a
) =
valid (kid, Neg phi :: a)
| valid
( Proof
{ children =
[ left as Proof {formula = Impl (phi, psi), ...}
, right as Proof {formula = Impl (psi', phi'), ...}
]
, label = IffI
, formula = Iff (phi'', psi'')
}
, a
) =
phi eq phi' andalso phi' eq phi'' andalso psi eq psi'
andalso psi' eq psi'' andalso valid (left, a) andalso valid (right, a)
| valid
( Proof
{ children = [kid as Proof {formula = Iff (phi, psi), ...}]
, label = IffE
, formula = Impl (p, q)
}
, a
) =
((phi eq p andalso psi eq q) orelse (phi eq q andalso psi eq p))
andalso valid (kid, a)
| valid (Proof {children = [], label = EqI, formula = Equal (t, t')}, a) =
Term.eq (t, t')
(* | valid *)
(* ( Proof *)
(* { children = *)
(* [ left as Proof {formula = Equal (t, s), ...} *)
(* , right as Proof {formula = phi, ...} *)
(* ] *)
(* , label = EqE *)
(* , formula = psi *)
(* } *)
(* , a *)
(* ) = *)
(* valid (left, a) andalso valid (right, a) *)
(* andalso Formula.checkSubst (t, s) (phi, psi) *)
(* | valid *)
(* ( Proof *)
(* { children = [kid as Proof {formula = Forall (x, phi), ...}] *)
(* , label = ForAllE *)
(* , formula = psi *)
(* } *)
(* , a *)
(* ) = *)
(* valid (kid, a) *)
(* andalso *)
(* (case Formula.matchVariable x (phi, psi) of *)
(* _ => true handle MatchFailure => false) *)
(* | valid *)
(* ( Proof *)
(* { children = [kid as Proof {formula = phi, ...}] *)
(* , label = ExistsI *)
(* , formula = Exist (x, psi) *)
(* } *)
(* , a *)
(* ) = *)
(* valid (kid, a) *)
(* andalso *)
(* (case Formula.matchVariable x (psi, phi) of *)
(* _ => true handle MatchFailure => false) *)
(* | valid *)
(* ( Proof *)
(* { children = [kid as Proof {formula = phi, ...}] *)
(* , label = ForAllI *)
(* , formula = Forall (x, psi) *)
(* } *)
(* , a *)
(* ) = *)
(* valid (kid, a) *)
(* andalso *)
(* (case Formula.matchVariable x (psi, phi) of *)
(* SOME (t as Term.Var x') => *)
(* Var.eq (x, x') andalso not (List.exists (Formula.occurs t) a) *)
(* | _ => false handle MatchFailure => false) *)
(* | valid *)
(* ( Proof *)
(* { children = *)
(* [ left as Proof {formula = Exist (x, phi), ...} *)
(* , right as Proof {formula = chi, ...} *)
(* ] *)
(* , label = ExistsE *)
(* , formula = chi' *)
(* } *)
(* , a *)
(* ) = *)
(* valid (left, a) andalso valid (right, phi :: a) *)
(* andalso not (List.exists (Formula.occurs (Term.Var x)) a) *)
(* | valid _ = false *)
end
end

10
lib/forgejo.ballcloud.cc/wball/proof-checker/TERM.sig
View file

@ -1,10 +0,0 @@
signature TERM =
sig
datatype t =
Var of int (* de Bruijn index *)
| Const of string
| Free of string
| Function of string * t list
val eq: t * t -> bool
end

16
lib/forgejo.ballcloud.cc/wball/proof-checker/Term.sml
View file

@ -1,16 +0,0 @@
structure Term: TERM =
struct
datatype t =
Var of int
| Const of string
| Free of string
| Function of string * t list
fun eq (Var x1, Var x2) = x1 = x2
| eq (Const s1, Const s2) = s1 = s2
| eq (Free s1, Free s2) = s1 = s2
| eq (Function (f1, args1), Function (f2, args2)) =
(f1 = f2 andalso List.all eq (ListPair.zip (args1, args2))
handle unequalLengths => false)
| eq _ = false
end

9
lib/forgejo.ballcloud.cc/wball/proof-checker/proof-checker.mlb
View file

@ -1,9 +0,0 @@
$(SML_LIB)/basis/basis.mlb
../../../github.com/diku-dk/sml-parse/parse.mlb
../../../github.com/diku-dk/sml-parse/simple_token.mlb
TERM.sig
Term.sml
FORMULA.sig
Formula.sml
PROOF.sig
Proof.sml

5
sml.pkg
View file

@ -1,5 +0,0 @@
package forgejo.ballcloud.cc/wball/proof-checker
require {
github.com/diku-dk/sml-parse 0.1.5 #5693148ec0e4cbba1a1664170d9814f3b63267d9
}