-
Notifications
You must be signed in to change notification settings - Fork 1
Format Alethe
The Alethe is a proof format inspired from the SMT-LIB input format, essentially meant for SMT solvers. Terms and formulas adopt the SMT-LIB format. Rules include resolution, various rules to support usual SMT operations, and sub-proofs.
The syntax is described in the external document here.
The semantics is described in the external document here.
Right now the specification is speculative: rather than being cast in stone, it will improve as solvers, proof reconstructions, and tools develop. Our approach is pragmatic. We refine the format and especially the rules as we gather experience.
In the following example, assumptions are first introduced (line 1–2); a subproof renames bound variables (line 4–8); the proof finishes with instantiaton and resolution steps (line 10–15).
(assume h2 (forall ((z1 U)) (forall ((z2 U)) (p z2))))
...
(anchor :step t9 :args ((:= z2 vr4)))
(step t9.t1 (cl (= z2 vr4)) :rule refl)
(step t9.t2 (cl (= (p z2) (p vr4))) :rule cong :premises (t9.t1))
(step t9 (cl (= (forall ((z2 U)) (p z2)) (forall ((vr4 U)) (p vr4))))
:rule bind)
...
(step t14 (cl (forall ((vr5 U)) (p vr5)))
:rule th_resolution :premises (t11 t12 t13))
(step t15 (cl (or (not (forall ((vr5 U)) (p vr5))) (p a)))
:rule forall_inst :args ((:= vr5 a)))
(step t16 (cl (not (forall ((vr5 U)) (p vr5))) (p a))
:rule or :premises (t15))
(step t17 (cl) :rule resolution :premises (t16 h1 t14))
The full documentation of the Alethe proof format can be found here.
The source of the format is maintained in this git repository.